2차 논리

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

## 정의
### 문법
2차 논리의 문법은 다음과 같은 기호들로 구성된다.

2차 논리의 **변수**()들은 다음과 같은 가산 무한 개의 **종류**()에 속한다.
* 각 자연수 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인 연산 변수들은 생략할 수 있다. 예를 들어, \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차 논리의 **항**()은 다음 문법을 따라야 한다.
* 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차 논리의 **[[논리식]]**()은 다음 문법을 따라야 한다.
* 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가 **자유 변수**()라는 것은 \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차 논리의 경우, 위와 같은 표준적인 의미론 대신 **헹킨 의미론**()을 사용할 수 있다. 헹킨 의미론에서는 각 변수 종류()가 다른 정의역()을 가질 수 있다. 헹킨 의미론을 사용할 경우 2차 논리는 사실상 1차 논리와 같아진다. 간혹 헹킨 의미론과 구별하기 위하여 전자를 **표준 의미론**()이라고 하기도 한다.

## 성질
2차 논리의 **증명 체계**()는 (순수한 논리 기호만 포함하는, 즉 변수 및 =,\forall,\exists,\lor,\land,\lnot만을 포함하는) 2차 논리 명제에 대하여 증명을 제시하거나 또는 제시하지 않는 함수이다. 증명 체계가 증명을 제시하는 명제를 **증명 가능 명제**()라고 한다. 여기서 "증명"이란 (주어진 알파벳에 대한) 일련의 문자열을 뜻한다.

괴델의 불완전성 정리에 따라, 2차 논리의 증명 체계는 다음 세 조건을 동시에 만족시킬 수 없다.
* (정당성 ) 증명 체계가 증명할 수 있는 모든 명제는 2차 논리의 모든 (표준) 모형에서 참이다.
* (완전성 ) 증명 체계는 2차 논리의 모든 (표준) 모형에서 참인 2차 논리 명제를 증명할 수 있다.
* (유효성 ) 증명들의 집합은 재귀적 집합이다. 즉, 주어진 문자열이 어떤 명제의 증명인지 여부를 항상 종료하는 알고리즘으로 판별할 수 있다.
반면, 1차 논리의 경우 위 세 조건을 만족시키는 증명 체계가 존재한다 (괴델의 완전성 정리).

2차 논리에서는 또한 콤팩트성 정리와 뢰벤하임-스콜렘 정리가 성립하지 않는다.

(위 성질들은 2차 논리의 표준 의미론에 대한 것이다. 헹킨 의미론을 사용하면 이는 1차 논리와 같은 성질들을 갖는다.)

## 역사
고틀로프 프레게는 1879년에 출판된 《개념 표기법》에서 오늘날의 2차 논리와 유사한 논리 체계를 도입하였다. 그러나 프레게는 1차 논리와 고차 논리를 구분하지 않았다. 이후 찰스 샌더스 퍼스가 1차 논리와 2차 논리를 구분하였으며, "2차 논리"라는 용어를 도입하였다.

헹킨 의미론은 리언 앨버트 헹킨(, 1921~2006)이 1950년에 도입하였다.

2차 논리에 대하여 윌러드 밴 오먼 콰인은 (이솝 우화에 빗대어) “양의 탈을 쓴 집합론”()이라고 평하였다. 즉, 2차 논리로는 집합론에 해당하는 여러 개념들(멱집합 등)을 정의할 수 있으며, 또한 적절한 증명 이론을 제시할 수 없으므로, 1차 논리와 달리 2차 ‘논리’는 사실 논리가 아니라는 것이다.

반면, 조지 불로스()를 비롯한 다른 수리철학자들은 콰인의 비판에 반대하여 2차 논리를 옹호하였다.

## 같이 보기
* 1차 논리
* 고차 논리

## 참고 문헌

* 
* 
* 
* 
* 
* 

## 외부 링크
*
*
* 
* 

분류:수리논리학