2차 논리

2차 논리의 문장 \exists\phi\phi가 쓰여진 그라피티 ([[노이쾰른)]] 수리논리학에서, **2차 논리**(二次論理, second-order logic)는 임의의 다항 관계 및 다항 연산에 대한 변수 및 이에 대한 전칭·존재 기호를 사용할 수 있는 논리이다. 1차 논리에서 변수는 사용하는 모형의 원소만을 지칭하지만, 2차 논리에서는 모형 속의 임의의 부분 집합에 대하여 언급할 수 있다. 이에 따라 2차 논리는 1차 논리보다 더 다양한 개념들에 대하여 논할 수 있다. 그러나 2차 논리는 1차 논리와 달리 완전한 증명 체계를 갖지 못하며, 콤팩트성 정리나 뢰벤하임-스콜렘 정리와 같은 중요한 성질들이 성립하지 않는다.
# 정의

## 문법
2차 논리의 문법은 다음과 같은 기호들로 구성된다. 2차 논리의 **변수**(variable)들은 다음과 같은 가산 무한 개의 **종류**(sort)에 속한다. * 각 자연수 n\in\mathbb N에 대하여, n항 연산 변수 f_0^n,f_1^n,f_2^n,\dots. ** 특히, n=0일 때, f_0^0,f_1^0,\dots는 1차 논리의 변수에 해당한다. ** 사실, n>0인 연산 변수들은 생략할 수 있다.63 예를 들어, \forall f_i^n(\cdots)는 \forall R_i^{n+1}\left((\forall x_0,x_0',x_1,x_2,\dots,x_n\colon R_i^{n+1}(x_0,x_1,\dots,x_n)\land R_i^{n+1}(x_0',x_1,\dots,x_n)\implies x_0=x_0')\implies(\cdots)\right)와 같이 풀어 쓸 수 있다. * 각 자연수 n\in\mathbb N에 대하여, n항 관계 변수 R_0^n,R_1^n,R_2^n,\dots. ** 특히, n=1일 때, R_0^1,R_1^1,\dots는 1차 논리 변수들의 집합에 해당한다. 변수 밖에도 다음과 같은 논리 기호들이 사용된다. (이들은 1차 논리와 같다.) * 전칭 기호 \forall와 존재 기호 \exists * 등호 = * 명제 논리 기호 \land (논리곱), \lor (논리합), \lnot (부정) 등 * 괄호 () 및 반점 , 등 * 주어진 n항 연산 \mathsf f 및 n항 관계 \mathsf R. 예를 들어, 집합론의 언어는 하나의 2항 관계 \in를 갖는다. 다른 예로, 순서체의 언어는 2항 연산 +와 \cdot, 1항 연산 -, 0항 연산 0과 1, 그리고 2항 관계 \le를 갖는다. 2차 논리의 **항**(term)은 다음 문법을 따라야 한다. * n항 연산 변수 f_i^n과 n개의 항 t_1,t_2,\dots,t_n에 대하여, f_i^n(t_1,t_2,\dots,t_n)은 항이다. (편의상 n=0일 때 괄호 f_i^0()를 생략하여 f_i^0로 쓴다.) * n항 연산 \mathsf f와 n개의 항 t_1,t_2,\dots,t_n에 대하여, \mathsf f(t_1,t_2,\dots,t_n)은 항이다. (편의상 n=0일 때 괄호 \mathsf f()를 생략하여 \mathsf f로 쓴다.) 2차 논리의 **논리식**((well formed) formula)은 다음 문법을 따라야 한다. * n항 관계 변수 R_i^n과 n개의 항 t_1,t_2,\dots,t_n에 대하여, R_i^n(t_1,t_2,\dots,t_n)는 논리식이다. * n항 관계 \mathsf R와 n개의 항 t_1,t_2,\dots,t_n에 대하여, \mathsf R(t_1,t_2,\dots,t_n)는 논리식이다. * 두 항 t_1, t_2에 대하여, t_1=t_2는 논리식이다. * 논리식 \phi와 \phi에 등장하는 n항 자유 연산 변수 f_i^n에 대하여, \forall f_i^n\phi와 \exists f_i^n\phi는 논리식이다. * 논리식 \phi와 \phi에 등장하는 n항 자유 관계 변수 R_i^n에 대하여, \forall R_i^n\phi와 \exists R_i^n\phi는 논리식이다. * 두 논리식 \phi와 \chi에 대하여, \phi\land\chi와 \phi\lor\chi 및 \phi에 대하여, \lnot\phi는 논리식이다. 여기서, 논리식 \phi에 등장하는 연산 변수 또는 관계 변수 x가 **자유 변수**(free variable)라는 것은 \phi에 \forall x나 \exists x가 포함되지 않는 것을 의미한다.
## 의미론
2차 논리의 의미론은 흔히 2차 논리의 모형으로 주어진다. 이 경우, 모형 \langle X,\dots\rangle가 주어졌을 때, n항 연산 변수는 X 위의 모든 (외적 관점에서의) 연산 X^{X^n}의 값을 가질 수 있으며, n항 관계 변수는 X 위의 모든 (외적 관점에서의) 관계 \mathcal P(X^n)의 값을 가질 수 있다. 특히, 1항 관계 변수는 X의 모든 부분 집합의 값을 가질 수 있다. 반면, 1차 논리 모형에서는 (집합론의 언어를 사용할 경우, 추이적 모형의 경우) 1차 논리 언어로 정의 가능한 X의 부분 집합만을 다룰 수 있다. 2차 논리의 경우, 위와 같은 표준적인 의미론 대신 **헹킨 의미론**(Henkin semantics)을 사용할 수 있다. 헹킨 의미론에서는 각 변수 종류(sort)가 다른 정의역(domain)을 가질 수 있다. 헹킨 의미론을 사용할 경우 2차 논리는 사실상 1차 논리와 같아진다. 간혹 헹킨 의미론과 구별하기 위하여 전자를 **표준 의미론**(standard semantics)이라고 하기도 한다.
# 성질
2차 논리의 **증명 체계**(proof system)는 (순수한 논리 기호만 포함하는, 즉 변수 및 =,\forall,\exists,\lor,\land,\lnot만을 포함하는) 2차 논리 명제에 대하여 증명을 제시하거나 또는 제시하지 않는 함수이다. 증명 체계가 증명을 제시하는 명제를 **증명 가능 명제**(provable proposition)라고 한다. 여기서 "증명"이란 (주어진 알파벳에 대한) 일련의 문자열을 뜻한다. 괴델의 불완전성 정리에 따라, 2차 논리의 증명 체계는 다음 세 조건을 동시에 만족시킬 수 없다. * (정당성 soundness) 증명 체계가 증명할 수 있는 모든 명제는 2차 논리의 모든 (표준) 모형에서 참이다. * (완전성 completeness) 증명 체계는 2차 논리의 모든 (표준) 모형에서 참인 2차 논리 명제를 증명할 수 있다. * (유효성 effectiveness) 증명들의 집합은 재귀적 집합이다. 즉, 주어진 문자열이 어떤 명제의 증명인지 여부를 항상 종료하는 알고리즘으로 판별할 수 있다. 반면, 1차 논리의 경우 위 세 조건을 만족시키는 증명 체계가 존재한다 (괴델의 완전성 정리). 2차 논리에서는 또한 콤팩트성 정리와 뢰벤하임-스콜렘 정리가 성립하지 않는다. (위 성질들은 2차 논리의 표준 의미론에 대한 것이다. 헹킨 의미론을 사용하면 이는 1차 논리와 같은 성질들을 갖는다.)
# 역사
고틀로프 프레게는 1879년에 출판된 《개념 표기법》언어=de에서 오늘날의 2차 논리와 유사한 논리 체계를 도입하였다.295 그러나 프레게는 1차 논리와 고차 논리를 구분하지 않았다. 이후 찰스 샌더스 퍼스가 1차 논리와 2차 논리를 구분하였으며, "2차 논리"라는 용어를 도입하였다.언어=en296 헹킨 의미론은 리언 앨버트 헹킨(Leon Albert Henkin, 1921~2006)이 1950년에 도입하였다.언어=en 2차 논리에 대하여 윌러드 밴 오먼 콰인은 (이솝 우화에 빗대어) “양의 탈을 쓴 집합론”(set theory in sheep’s clothing)이라고 평하였다.언어=en66, Chapter 5 즉, 2차 논리로는 집합론에 해당하는 여러 개념들(멱집합 등)을 정의할 수 있으며, 또한 적절한 증명 이론을 제시할 수 없으므로, 1차 논리와 달리 2차 ‘논리’는 사실 논리가 아니라는 것이다. 반면, 조지 불로스(George Boolos)언어=en를 비롯한 다른 수리철학자들은언어=en언어=en언어=en언어=en언어=en 콰인의 비판에 반대하여 2차 논리를 옹호하였다.