1차 논리

**1차 논리**(一次論理, first-order logic)는 원소에만 한정 기호를 가할 수 있고, 술어에는 한정 기호를 가할 수 없는 술어 논리이다.언어=en 명제 논리와 달리 변수에 대하여 한정 기호를 사용할 수 있으나, 2차 논리와 달리 변수들의 집합에 대하여 한정 기호를 사용할 수 없다. 1차 논리의 경우, (2차 논리와 달리) 괴델의 완전성 정리 · 콤팩트성 정리 · 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립한다. 이외에 **1차 술어 논리**, **1계 논리** 등으로도 불린다. 간단히 **술어 논리**(predicate logic)라 하면 1차 논리를 가리키는 경우가 많다.
# 정의
1차 논리는 다음의 요소들로 이루어진다. * 특정 문자열들의 집합을 **논리식**의 집합이라고 한다. 논리식이 만족시켜야 하는 문법은 재귀적으로 정의된다. * 특정 논리식 집합으로부터 다른 논리식을 **추론**할 수 있다. 이에 대한 규칙은 힐베르트 체계 및 다른 여러 방식으로 명시될 수 있다. * 1차 논리 언어의 **의미론**이란 그 언어의 문장들에 대하여 참인지 여부를 일관적으로 부여하는 구조이다. 이는 보통 모형으로 주어진다.
## 문법
다음과 같은 데이터가 주어졌다고 하자. (여기서 \mathbb N은 자연수, 즉 음이 아닌 정수의 집합이다.) * 집합 I 및 함수 m\colon I\to\mathbb N, i\mapsto m_i. I는 유한 집합이거나 무한 집합일 수 있다. 이를 **연산**(演算, operation)의 집합이라고 한다. * 집합 J 및 함수 n\colon J\to\mathbb N, j\mapsto n_j. J는 유한 집합이거나 무한 집합일 수 있다. 이를 **관계**(關係, relation)의 집합이라고 한다. 그렇다면, (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 등이 있다. * 등호 = * **전칭 기호**(全稱記號, universal quantifier) \forall. ** 그 대신 **존재 기호**(存在記號, existential quantifier) \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의 **항수**(項數, arity)라고 한다. 0항 연산을 **상수**(constant)라고 한다. * 각 j\in J에 대하여, 기호 \mathsf R_j. 이를 n_j항 **관계**라고 하며, n_j를 \mathsf R_j의 **항수**(項數, arity)라고 한다. 1항 관계를 **술어**(predicate)라고 한다. (항수가 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}를 제외한 기호들을 **논리 기호**(logical symbol)라고 한다. 1차 논리의 **항**(項, term)은 다음 문법을 따른다. * 모든 변수는 항이다. * 임의의 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차 논리의 **논리식**((well-formed) formula)은 다음 문법을 따르는, 위 기호들의 문자열이다. * 임의의 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의 **자유 변수**(free variable)라고 하며, 그렇지 않다면 x를 \phi의 **종속 변수**(bound variable)라고 한다. 자유 변수를 갖지 않는 (즉, 그 속에 등장하는 모든 변수가 종속 변수인) 논리식을 **문장**(文章, sentence)이라고 한다.
## 공리와 추론 규칙
1차 논리의 증명 이론은 다양한 방식으로 공리화할 수 있다. 예를 들어 다비트 힐베르트의 힐베르트 체계(Hilbert system)나, 게르하르트 겐첸의 시퀀트 계산이나 자연 연역 등을 사용할 수 있다. 1차 논리를 힐베르트 체계를 사용하여 공리화하면, 다음과 같다. 우선, 편의상 다음과 같은 기호만을 사용한다고 하자. * 명제 논리에서, 오직 함의 \implies와 부정 \lnot만을 사용한다고 하자. (논리합이나 논리곱과 같은 다른 명제 논리 기호는 이 둘로 나타낼 수 있다.) * 술어 논리에서, 오직 전칭 기호 \forall만을 사용한다고 하자. (존재 기호 \exists는 \forall만으로 나타낼 수 있다.) 이 경우, 다음과 같은 공리 기본꼴(axiom schema)들을 정의한다. 이 공리 기본꼴들에서 사용된 기호들은 다음과 같다. * \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차 언어**(monadic first-order language)라고 한다.
## 린드스트룀 정리
**린드스트룀 정리**(Lindström’s theorem)에 따르면, 1차 술어 논리는 (가산) 콤팩트성 정리와 하향 뢰벤하임-스콜렘 정리를 만족시키는 가장 강력한 논리 체계이다.언어=en
# 예

## 집합론
체르멜로-프렝켈 집합론의 언어는 하나의 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년에 출판된 《개념 표기법》언어=de에서 사용한 논리는 (현대적 용어로는) 2차 논리였다.295101–102 이후 1885년에 찰스 샌더스 퍼스는 1차 논리와 2차 논리를 구분하였다.언어=en언어=en296언어=en99 퍼스는 1차 논리를 "1차 내포 논리"(first-intensional logic)로, 2차 논리를 "2차 내포 논리"(second-intensional logic)로 일컬었다.99–100 이후 에른스트 체르멜로는 2차 논리를 사용하여 집합론을 개발하였다. 토랄프 스콜렘은 1922년에 체르멜로의 집합론을 1차 논리로 재정의하였다.언어=de123–124언어=en153–156url-status=447 이는 오늘날 사용되는 체르멜로-프렝켈 집합론의 기반이 되었다. 제2차 세계 대전 이후 1차 논리는 (2차 논리나 유형 이론 등을 대신하여) 통상적으로 사용되는 수학의 기반이 되었다.448