Loading AI tools
위키백과, 무료 백과사전
1차 논리(一次論理, 영어: first-order logic)는 원소에만 한정 기호를 가할 수 있고, 술어에는 한정 기호를 가할 수 없는 술어 논리이다.[1] 명제 논리와 달리 변수에 대하여 한정 기호를 사용할 수 있으나, 2차 논리와 달리 변수들의 집합에 대하여 한정 기호를 사용할 수 없다. 1차 논리의 경우, (2차 논리와 달리) 괴델의 완전성 정리 · 콤팩트성 정리 · 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립한다.
이외에 1차 술어 논리, 1계 논리 등으로도 불린다. 간단히 술어 논리(predicate logic)라 하면 1차 논리를 가리키는 경우가 많다.
1차 논리는 다음의 요소들로 이루어진다.
다음과 같은 데이터가 주어졌다고 하자. (여기서 은 자연수, 즉 음이 아닌 정수의 집합이다.)
그렇다면, 으로 정의되는 1차 논리 언어 는 특정한 문자열들의 집합이다. 이 문자열을 구성하는 문자 집합
은 구체적으로 다음과 같다.
이 기호들 가운데, 및 를 제외한 기호들을 논리 기호(영어: logical symbol)라고 한다.
1차 논리의 항(項, 영어: term)은 다음 문법을 따른다.
1차 논리의 논리식(영어: (well-formed) formula)은 다음 문법을 따르는, 위 기호들의 문자열이다.
여기서 논리식 및 그 속에 등장하는 변수 에 대하여, 만약 가 를 포함하지 않는다면, 를 의 자유 변수(영어: free variable)라고 하며, 그렇지 않다면 를 의 종속 변수(영어: bound variable)라고 한다.
자유 변수를 갖지 않는 (즉, 그 속에 등장하는 모든 변수가 종속 변수인) 논리식을 문장(文章, 영어: sentence)이라고 한다.
1차 논리의 증명 이론은 다양한 방식으로 공리화할 수 있다. 예를 들어 다비트 힐베르트의 힐베르트 체계(영어: Hilbert system)나, 게르하르트 겐첸의 시퀀트 계산(영어: sequent calculus)이나 자연 연역(영어: natural deduction) 등을 사용할 수 있다.
1차 논리를 힐베르트 체계를 사용하여 공리화하면, 다음과 같다. 우선, 편의상 다음과 같은 기호만을 사용한다고 하자.
이 경우, 다음과 같은 공리 기본꼴(영어: axiom schema)들을 정의한다. 이 공리 기본꼴들에서 사용된 기호들은 다음과 같다.
즉, 공리 기본꼴에서 위의 기호들을 실제의 논리식·항·변수로 치환하면 공리들을 얻는다.
우선, 추론 규칙으로 전건 긍정의 형식
과 일반화
가 있다. 이 밖에, 다음과 같은 명제 논리의 공리 기본꼴들이 사용된다.
1차 술어 논리의 경우, 다음과 같은 추가 공리 기본꼴들이 사용된다.
위 공리 기본꼴들에서, 는 논리식 에 등장하는 자유 변수 를 항 로 대체하여 얻는 논리식을 뜻한다. 예를 들어, 체의 언어에서
이다. 이때, 논리식 내부의 ‘’에서 가 치환되지 않는 이유는 이 부분에서는 가 종속 변수이기 때문이다.
1차 논리의 의미론은 보통 모형으로 주어진다. 주어진 연산 집합 와 관계 집합 을 갖는 1차 논리 언어 가 주어졌다고 하자. 그렇다면, 이 언어의 모형은 집합 및 각 항 연산 에 대하여 의 해석 및 각 항 관계 에 대하여 그 해석 으로 구성된다. 이를 통해, 의 문장 와 의 모형 에 대하여, 가 에서 참인지 또는 거짓인지 여부를 정의할 수 있다. 가 에서 참이라는 것은
로 표기한다.
보다 일반적으로, 의 논리식 가 자유 변수 를 갖는다고 하자. 그렇다면, 의 모형 및 그 속의 개의 원소
가 주어졌을 때,가 에서 에 대하여 참인지 또는 거짓인지 여부를 정의할 수 있다. 이는
로 표기한다.
1차 논리의 경우 콤팩트성 정리와 뢰벤하임-스콜렘 정리가 성립한다.
비논리 기호를 포함하지 않는 1차 논리 문장들의 집합을 라고 하자. 그 가운데, 모든 모형에서 참인 문장들의 부분 집합
을 생각하자. 또한, 속에서, 위의 힐베르트 체계를 통해 증명할 수 있는 문장들의 집합을
그렇다면, 다음이 성립한다.
보다 일반적으로, 임의의 가산 연산 집합 와 관계 집합 를 갖는 1차 논리 언어 속에서, 문장들의 집합을 라고 하자. 그 가운데, 모든 모형에서 참인 문장들의 부분 집합
을 생각하자.
린드스트룀 정리(영어: Lindström’s theorem)에 따르면, 1차 술어 논리는 (가산) 콤팩트성 정리와 하향 뢰벤하임-스콜렘 정리를 만족시키는 가장 강력한 논리 체계이다.[2]
체르멜로-프렝켈 집합론의 언어는 하나의 2항 관계 만을 포함하며, 아무런 연산을 갖지 않는다. 집합론에서 사용되는 대부분의 명제들은 이 언어로 나타낼 수 있다.
체의 1차 논리 언어
는 두 개의 이항 연산과 하나의 1항 연산 및 두 개의 상수(0항 연산)을 포함하며, 등호 밖의 관계를 갖지 않는다. 보통 는 와 같이 표기한다.
순서체의 1차 논리 언어
는 두 개의 이항 연산과 하나의 1항 연산 및 두 개의 상수(0항 연산)을 포함하며, 하나의 2항 관계를 갖는다. 보통 는 와 같이 표기한다.
범주의 1차 논리 언어는 다음과 같이, 하나의 3항 관계
와 두 개의 1항 연산
으로 나타낼 수 있다. 변수들은 사상을 나타내며, 대상들은 항등 사상으로 나타내어진다. 편의상 다음과 같은 술어를 정의하자.
이는 가 항등 사상(즉, 대상)임을 뜻한다. 그렇다면, 범주의 1차 논리 이론은 다음과 같은 공리들로 구성된다.
고틀로프 프레게가 1879년에 출판된 《개념 표기법》[3]에서 사용한 논리는 (현대적 용어로는) 2차 논리였다.[4]:295[5]:101–102 이후 1885년에 찰스 샌더스 퍼스는 1차 논리와 2차 논리를 구분하였다.[6][4]:296[5]:99 퍼스는 1차 논리를 "1차 내포 논리"(영어: first-intensional logic)로, 2차 논리를 "2차 내포 논리"(영어: second-intensional logic)로 일컬었다.[5]:99–100
이후 에른스트 체르멜로는 2차 논리를 사용하여 집합론을 개발하였다. 토랄프 스콜렘은 1922년에 체르멜로의 집합론을 1차 논리로 재정의하였다.[7][5]:123–124[8]:153–156[9]:447 이는 오늘날 사용되는 체르멜로-프렝켈 집합론의 기반이 되었다.
제2차 세계 대전 이후 1차 논리는 (2차 논리나 유형 이론 등을 대신하여) 통상적으로 사용되는 수학의 기반이 되었다.[9]:448
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.