1차 논리

**1차 논리**(一次論理, )는 원소에만 한정 기호를 가할 수 있고, 술어에는 한정 기호를 가할 수 없는 술어 논리이다. 명제 논리와 달리 변수에 대하여 한정 기호를 사용할 수 있으나, 2차 논리와 달리 변수들의 집합에 대하여 한정 기호를 사용할 수 없다. 1차 논리의 경우, (2차 논리와 달리) 괴델의 완전성 정리 · 콤팩트성 정리 · 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립한다.

이외에 **1차 술어 논리**, **1계 논리** 등으로도 불린다. 간단히 **술어 논리**(predicate logic)라 하면 1차 논리를 가리키는 경우가 많다.

## 정의
1차 논리는 다음의 요소들로 이루어진다.
* 특정 문자열들의 집합을 **[[논리식]]**의 집합이라고 한다. 논리식이 만족시켜야 하는 문법은 재귀적으로 정의된다.
* 특정 논리식 집합으로부터 다른 논리식을 **추론**할 수 있다. 이에 대한 규칙은 힐베르트 체계 및 다른 여러 방식으로 명시될 수 있다.
* 1차 논리 언어의 **의미론**이란 그 언어의 문장들에 대하여 참인지 여부를 일관적으로 부여하는 구조이다. 이는 보통 모형으로 주어진다.

### 문법
다음과 같은 데이터가 주어졌다고 하자. (여기서 \mathbb N은 자연수, 즉 음이 아닌 정수의 집합이다.)
* 집합 I 및 함수 m\colon I\to\mathbb N, i\mapsto m_i. I는 유한 집합이거나 무한 집합일 수 있다. 이를 **연산**(演算, )의 집합이라고 한다.
* 집합 J 및 함수 n\colon J\to\mathbb N, j\mapsto n_j. J는 유한 집합이거나 무한 집합일 수 있다. 이를 **관계**(關係, )의 집합이라고 한다.

그렇다면, (I,m,J,n)으로 정의되는 **1차 논리 언어** \mathcal L_{I,J}\subseteq\Sigma^*는 특정한 문자열들의 집합이다. 이 문자열을 구성하는 문자 집합
:\Sigma=\{\mathsf x_n\}_{n\in\mathbb N}\sqcup\{\forall,=,\implies,\lnot\}\sqcup\{\mathsf f_i\}_{i\in I}\sqcup\{\mathsf R_j\}_{j\in J}
은 구체적으로 다음과 같다.
* 가산 무한 개의 변수들 \mathsf x_0,\mathsf x_1,\mathsf x_2,\dots
** 가산 무한 개의 변수들만으로 충분한 이유는 모든 논리식의 길이가 유한하기 때문이다. 무한 논리의 경우 더 많은 변수들을 추가할 수 있다.
* 명제 논리의 연산 \implies (함의) 및 \lnot (부정).
** 그 대신 다른 기호들을 사용할 수도 있다. 예를 들어, 논리합 \lor 또는 논리곱 \land 등이 있다.
* 등호 =
* **전칭 기호**(全稱記號, ) \forall.
** 그 대신 **존재 기호**(存在記號, ) \exists를 사용할 수도 있다. 사실, 임의의 변수 x에 대하여 \forall x\phi\iff \lnot\exists x\lnot\phi이며 \exists x\phi\iff \lnot\forall x\lnot\phi이므로, 이들은 서로 동치이다.
* 각 i\in I에 대하여, 기호 \mathsf f_i. 이를 m_i항 **연산**이라고 하며, m_i를 \mathsf f_i의 **[[항수 (수학)|항수]]**(項數, )라고 한다. 0항 연산을 **상수**()라고 한다.
* 각 j\in J에 대하여, 기호 \mathsf R_j. 이를 n_j항 **관계**라고 하며, n_j를 \mathsf R_j의 **항수**(項數, )라고 한다. 1항 관계를 **술어**()라고 한다.  (항수가 0인 관계는 고전 명제 논리에서는 참 또는 거짓이 되므로 자명하다.)
* 이 밖에도, 괄호 () 및 반점 , 등은 엄밀히 말해 불필요하지만, 가독성을 돕기 위해 첨가한다. 예를 들어, \mathsf f_i\mathsf x_0\mathsf x_2 대신 \mathsf f_i(\mathsf x_0,\mathsf x_2)로 쓴다.
이 기호들 가운데, \{\mathsf f_i\}_{i\in I} 및 \{\mathsf R_j\}_{j\in J}를 제외한 기호들을 **논리 기호**()라고 한다.

1차 논리의 **항**(項, )은 다음 문법을 따른다.
* 모든 변수는 항이다.
* 임의의 i\in I와 m_i개의 항 t_1,t_2,\dots,t_{m_i}에 대하여, \mathsf f_i(t_1,t_2,\dots,t_{m_i})은 항이다.  (상수의 경우, 즉 m_i=0일 때, 보통 괄호 \mathsf f_i()를 생략하여 \mathsf f_i로 쓴다.)

1차 논리의 **논리식**()은 다음 문법을 따르는, 위 기호들의 문자열이다.
* 임의의 j\in J와 n_j개의 항 t_1,\dots,t_{n_j}에 대하여, \mathsf R_j(t_1,\dots,t_{n_j})은 논리식이다.
* 두 항 t_1, t_2에 대하여, t_1=t_2는 논리식이다.
* 논리식 \phi와 \chi에 대하여, \lnot\phi와 \phi\implies\chi는 논리식이다.
* 논리식 \phi에 등장하는 변수 x_i가 자유 변수라면, \forall x\phi는 논리식이다.
여기서 논리식 \phi 및 그 속에 등장하는 변수 x에 대하여, 만약 \phi가 \forall x를 포함하지 않는다면, x를 \phi의 **자유 변수**()라고 하며, 그렇지 않다면 x를 \phi의 **종속 변수**()라고 한다.

자유 변수를 갖지 않는 (즉, 그 속에 등장하는 모든 변수가 종속 변수인) 논리식을 **문장**(文章, )이라고 한다.

### 공리와 추론 규칙
1차 논리의 증명 이론은 다양한 방식으로 공리화할 수 있다. 예를 들어 다비트 힐베르트의 힐베르트 체계()나, 게르하르트 겐첸의 시퀀트 계산이나 자연 연역 등을 사용할 수 있다.

1차 논리를 힐베르트 체계를 사용하여 공리화하면, 다음과 같다. 우선, 편의상 다음과 같은 기호만을 사용한다고 하자.
* 명제 논리에서, 오직 함의 \implies와 부정 \lnot만을 사용한다고 하자. (논리합이나 논리곱과 같은 다른 명제 논리 기호는 이 둘로 나타낼 수 있다.)
* 술어 논리에서, 오직 전칭 기호 \forall만을 사용한다고 하자. (존재 기호 \exists는 \forall만으로 나타낼 수 있다.)

이 경우, 다음과 같은 공리 기본꼴()들을 정의한다. 이 공리 기본꼴들에서 사용된 기호들은 다음과 같다.
* \phi, \chi, \psi는 임의의 논리식을 뜻한다.
* t, u는 임의의 항을 뜻한다.
* x는 임의의 변수를 뜻한다.
즉, 공리 기본꼴에서 위의 기호들을 실제의 논리식·항·변수로 치환하면 공리들을 얻는다.

우선, 추론 규칙으로 전건 긍정의 형식
:㈀ \begin{matrix}
\phi\implies\chi\\
\phi\\
\hline
\chi
\end{matrix}
과 일반화
:㈁ \begin{matrix}
\phi\\
\hline
\forall x\phi
\end{matrix}
::추론 규칙 ㈁에서, x는 \phi의 자유 변수이어야 한다.
가 있다. 이 밖에, 다음과 같은 명제 논리의 공리 기본꼴들이 사용된다.
:㈂ \phi \implies \left( \chi \implies \phi \right) 
:㈃ \left( \phi \implies \left( \chi \implies \psi \right) \right) \implies \left( \left( \phi \implies \chi \right) \implies  \left( \phi \implies \psi \right) \right)
:㈄ \left ( \lnot \phi \implies \lnot \chi \right) \implies \left( \chi\implies \phi \right) 
1차 술어 논리의 경우, 다음과 같은 추가 공리 기본꼴들이 사용된다.
:㈅  \forall x\phi\implies\phi[t/x]
:㈆ \forall x\left(\phi\implies\chi\right) \implies \left( \forall x\phi \implies \forall x\chi\right)
:㈇ x = x
:㈈ \left(t=u\right) \implies \left( \phi[t/x] \implies \phi[u/x] \right)
::공리 기본꼴 ㈈에서, x는 논리식 \phi의 자유 변수이어야 한다.
위 공리 기본꼴들에서, \phi[t/x]는 논리식 \phi에 등장하는 자유 변수 x를 항 t로 대체하여 얻는 논리식을 뜻한다. 예를 들어, 체의 언어에서
:\text{“}\lnot(x=2)\land\left(\forall xx=y)\right)\lor x=3\text{”}[(1+1)/x]
=\text{“}\lnot\left((1+1)=2\right)\land\left(\forall xx=y)\right)\lor 1+1=3\text{”}
이다. 이때, 논리식 내부의 ‘\forall xx=y’에서 x가 치환되지 않는 이유는 이 부분에서는 x가 종속 변수이기 때문이다.

## 성질
### 의미론

1차 논리의 의미론은 보통 모형으로 주어진다. 주어진 연산 집합 I와 관계 집합 J을 갖는 1차 논리 언어 \mathcal L_{I,J}가 주어졌다고 하자. 그렇다면, 이 언어의 **[[모형 (논리학)|모형]]**은 집합 X 및 각 n항 연산 i\in I에 대하여 \mathsf f_i의 **해석** \mathsf f_i^X\colon X^n\to X 및 각 n_j항 관계 \mathsf R_j에 대하여 그 **해석** \mathsf R_j^X\in\mathcal P(X^{n_j})으로 구성된다. 이를 통해, \mathcal L_{I,J}의 문장 \phi와 \mathcal L_{I,J}의 모형 M에 대하여, \phi가 M에서 참인지 또는 거짓인지 여부를 정의할 수 있다. \phi가 M에서 참이라는 것은
:M\models\phi
로 표기한다.

보다 일반적으로, \mathcal L_{I,J}의 논리식 \phi가 자유 변수 x_1,\dots,x_k를 갖는다고 하자. 그렇다면, \mathcal L_{I,J}의 모형 M 및 그 속의 k개의 원소
:(m_1,\dots,m_k)\in M^k
가 주어졌을 때,\phi가 M에서 (m_i)_{i=1}^k에 대하여 참인지 또는 거짓인지 여부를 정의할 수 있다. 이는
:M\models\phi[m_1/x_1,\dots,m_k/x_k]
로 표기한다.

1차 논리의 경우 **[[콤팩트성 정리]]**와 **[[뢰벤하임-스콜렘 정리]]**가 성립한다.

### 증명 이론
비논리 기호를 포함하지 않는 1차 논리 문장들의 집합을 \mathcal L_=^0라고 하자. 그 가운데, 모든 모형에서 참인 문장들의 부분 집합
:\mathcal T=\{\phi\in\mathcal L_=^0\colon\forall M\in\operatorname{Model}(\mathcal L_=)\colon M\models\phi\}
을 생각하자. 또한, \mathcal L_=^0 속에서, 위의 힐베르트 체계를 통해 증명할 수 있는 문장들의 집합을
:\mathcal T'=\{\phi\in\mathcal L_=^0\colon\vdash\phi\}
그렇다면, 다음이 성립한다.
* 1차 논리의 건전성 정리에 따르면, \mathcal T=\mathcal T'이다. 즉, 명제가 증명 가능한지 여부는 명제가 참인지 여부와 동치이다.
* \mathcal T는 재귀 집합이다. (이는 레오폴트 뢰벤하임이 1915년에 증명하였다.)

보다 일반적으로, 임의의 가산 연산 집합 I와 관계 집합 J를 갖는 1차 논리 언어 \mathcal L_{I,J} 속에서, 문장들의 집합을 \mathcal L_{I,J}^0\subseteq\mathcal L_{I,J}라고 하자. 그 가운데, 모든 모형에서 참인 문장들의 부분 집합
:\mathcal T=\{\phi\in\mathcal L^0_{I,J}\colon\forall M\in\operatorname{Model}(\mathcal L_{I,J})\colon M\models\phi\}
을 생각하자.
* 괴델의 완전성 정리에 따르면, \mathcal T는 재귀 열거 집합이다.
* 만약 \mathcal R에 (등호를 제외한) 2항 이상의 항수를 갖는 관계가 존재한다면, \mathcal T는 재귀 집합이 아니다.
* 만약 I=\varnothing이며, J의 모든 관계가 술어(1항 관계) 또는 등호라면, \mathcal T는 재귀 집합이다. 이러한 언어를 **1항 1차 언어**()라고 한다.

### 린드스트룀 정리
**린드스트룀 정리**()에 따르면, 1차 술어 논리는 (가산) 콤팩트성 정리와 하향 뢰벤하임-스콜렘 정리를 만족시키는 가장 강력한 논리 체계이다.

## 예
### 집합론
체르멜로-프렝켈 집합론의 언어는 하나의 2항 관계 \in 만을 포함하며, 아무런 연산을 갖지 않는다. 집합론에서 사용되는 대부분의 명제들은 이 언어로 나타낼 수 있다.

### 체와 순서체
체의 1차 논리 언어
:I=\{+,\cdot,-,0,1\}
:m_+=m_\cdot=2
:m_-=1
:m_0=m_1=0
:J=\varnothing
는 두 개의 이항 연산과 하나의 1항 연산 및 두 개의 상수(0항 연산)을 포함하며, 등호 밖의 관계를 갖지 않는다. 보통
\mathsf f_+(a,b)는 a+b와 같이 표기한다.

순서체의 1차 논리 언어
:I=\{+,\cdot,-,0,1\}
:m_+=m_\cdot=2
:m_-=1
:m_0=m_1=0
:J=\{\le\}
:n_\le=2
는 두 개의 이항 연산과 하나의 1항 연산 및 두 개의 상수(0항 연산)을 포함하며, 하나의 2항 관계를 갖는다. 보통
\mathsf R_\le(a,b)는 a\le b와 같이 표기한다.

### 범주
범주의 1차 논리 언어는 다음과 같이, 하나의 3항 관계
* \mathsf C(-,-,-) (\mathsf C(x,y,z)는 x\circ y=z임을 뜻함)
와 두 개의 1항 연산
* \operatorname{dom}(-) (사상의 정의역)
* \operatorname{codom}(-) (사상의 공역)
으로 나타낼 수 있다. 변수들은 사상을 나타내며, 대상들은 항등 사상으로 나타내어진다. 편의상 다음과 같은 술어를 정의하자.
:\mathsf{Obj}(x)\iff \operatorname{dom}(x)=\operatorname{codom}(x)=x
이는 x가 항등 사상(즉, 대상)임을 뜻한다. 그렇다면, 범주의 1차 논리 이론은 다음과 같은 공리들로 구성된다.
* \operatorname{dom}(x)=x\iff\operatorname{codom}(x)=x (항등 사상의 두 정의의 동치성)
* \mathsf{Obj}(\operatorname{dom}x) (사상의 정의역은 대상)
* \mathsf{Obj}(\operatorname{codom}x) (사상의 공역은 대상)
* \mathsf C(x,y,z)\implies\operatorname{dom} x=\operatorname{codom}y (사상 합성의 존재의 필요 조건)
* \mathsf C(x,y,z)\implies\operatorname{dom} y=\operatorname{dom} z (합성 사상의 정의역)
* \mathsf C(x,y,z)\implies\operatorname{codom}x=\operatorname{codom}z (합성 사상의 공역)
* \mathsf C(x,y,a)\land\mathsf C(a,z,c)\land\mathsf C(y,z,b)\land\mathsf C(x,b,d)\implies c=d (사상 합성의 결합 법칙)
* \mathsf{Obj}(x)\land\mathsf C(x,y,z)\implies y=z (항등 사상과의 합성)
* \mathsf{Obj}(y)\land\mathsf C(x,y,z)\implies x=z (항등 사상과의 합성)
이 이론의 모형의 개념은 **[[작은 범주]]**의 개념과 동치이다.

## 역사
고틀로프 프레게가 1879년에 출판된 《개념 표기법》에서 사용한 논리는 (현대적 용어로는) 2차 논리였다. 이후 1885년에 찰스 샌더스 퍼스는 1차 논리와 2차 논리를 구분하였다. 퍼스는 1차 논리를 "1차 내포 논리"()로, 2차 논리를 "2차 내포 논리"()로 일컬었다.

이후 에른스트 체르멜로는 2차 논리를 사용하여 집합론을 개발하였다. 토랄프 스콜렘은 1922년에 체르멜로의 집합론을 1차 논리로 재정의하였다. 이는 오늘날 사용되는 체르멜로-프렝켈 집합론의 기반이 되었다.

제2차 세계 대전 이후 1차 논리는 (2차 논리나 유형 이론 등을 대신하여) 통상적으로 사용되는 수학의 기반이 되었다.

## 같이 보기
* 논리 기호
* 로지반
* 프리넥스 표준형
* 프롤로그 (프로그래밍 언어)
* 관계대수
* 관계형 모델
* 스콜렘 표준형
* 진리표
## 각주

## 외부 링크
* 
* 
* 
* 
* 
* 
* 
* 
* 
* 

분류:술어 논리