2차 논리

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

2차 논리의 문장 $\exists \phi \phi$가 쓰여진 그라피티 (노이쾰른)

정의

문법

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항 관계 $\leq$를 갖는다.

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년에 출판된 《개념 표기법》에서 오늘날의 2차 논리와 유사한 논리 체계를 도입하였다.^:295 그러나 프레게는 1차 논리와 고차 논리를 구분하지 않았다. 이후 찰스 샌더스 퍼스가 1차 논리와 2차 논리를 구분하였으며, "2차 논리"라는 용어를 도입하였다.^:296

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

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

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

참고 문헌

• Rossberg, M. (2004). 〈First-order logic, second-order logic, and completeness〉 (PDF). Hendricks, Vincent; Neuhaus, Fabian; Scheffler, Uwe; Pedersen, Stig Andur; Wansing, Heinrich. 《First-order logic revisited》. Logische Philosophie (영어) 12. λογος-Verlag. 303–322쪽. ISBN 978-3-8325-0475-5. 
• Shapiro, Stewart (2001년 8월). 〈Classical logic II: higher order logic〉. Goble, Lou. 《The Blackwell Guide to Philosophical Logic》 (영어). Blackwell. 33–54쪽. doi:10.1111/b.9780631206934.2001.00005.x. ISBN 978-0-631-20693-4. 
• Lambek, Joachim; Scott, P. J. (1986). 《Introduction to higher order categorical logic》 (영어). Cambridge University Press. ISBN 978-0-521-35653-4. 
• Benzmüller, Christoph; Miller, Dale (2014). 〈Automation of higher-order logic〉 (PDF). Gabbay, Dov M.; Siekmann, Jörg H.; Woods, John. 《Handbook of the history of logic, volume 9: computational logic》 (영어). Elsevier. 215–254쪽. doi:10.1016/B978-0-444-51624-4.50005-8. ISBN 978-0-08-093067-1. 
• Moore, Gregory H. (1988). 〈The emergence of first-order logic〉 (PDF). Aspray, William; Kitcher, Philip. 《History and Philosophy of Modern Mathematics》. Minnesota Studies in the Philosophy of Science (영어) 11. University of Minnesota Press. 95–135쪽. JSTOR 10.5749/j.cttttp0k.7. 
• Eklund, Matti (1996년 12월). “On how logic became first-order” (PDF). 《Nordic Journal of Philosophical Logic》 (영어) 1 (2): 147–167. 

외부 링크

• Enderton, Herbert B. (2009년 3월 4일). “Second-order and higher-order logic”. 《The Stanford Encyclopedia of Philosophy》 (영어). 
• Uzquiano, Gabriel (2014년 9월 3일). “Quantifiers and quantification”. 《The Stanford Encyclopedia of Philosophy》 (영어). 
• “Second-order logic”. 《nLab》 (영어). 
• “Higher-order logic”. 《nLab》 (영어).