SecondOrder

2차 논리 언어(second-order language)

비논리 상수 집합(개별 상수, 함수 기호, 술어 기호) \(\operatorname{C}\) 에 대하여 \(\operatorname{L1C}\) 를 1차 논리 언어라고 하자.

• 언어 \(\operatorname{L1C}\) 에서 시작하여 양의 정수 \(n\) 과 \(i\) 에 대한 함수 변수 \(\mathbf{g}_{i}^{n}\) 과 술어 변수 \(\mathbf{R} _{i}^{n}\) 을 추가한다.

\(\left< u \right>_n\) 을 개별 변수 \(u_1, \dots, u_n\) 의 임의의 열로 정의하고, \(\forall \left< u \right>_n\) 을 \((\forall u_1)\dots (\forall u_n)\) 로 정의하자. \(\left< t \right>_n\) 을 항의 열 \(t_1, \dots, t_n\) 으로 정의하자.

• 항의 집합에 함수 변수 \(\mathbf{g} ^{n}\) 에 대한 항 \(\mathbf{g} ^{n}(\left< t \right>_n)\) 을 추가한다.
• 식의 집합에 새롭게 확장된 항의 집합의 임의의 열 \(\left< t \right>_n\) 과 \(\operatorname{C}\) 의 임의의 술어 기호 \(A _{i}^{n}\) 과 임의의 \(n\)항 술어 변수 \(\mathbf{R} ^{n}\) 에 대한 원자식 \(A _{i}^{n}(\left< t \right>_n)\) 과 \(\mathbf{R}^{n}(\left< t \right>_n)\) 을 추가한다.
• 식의 집합에 함수와 술어 변수에 대한 양화 \((\forall \mathbf{g}^{n})B\) 와 \((\forall \mathbf{R}^{n})B\) 를 추가한다.

위와 같은 방식으로 얻어진 언어를 2차 논리 언어 \(\operatorname{L2C}\) 라고 한다. \(\operatorname{L2C}\) 를 완전 2차 논리 언어(full second-order logic language)라고 한다.

동등성 기호의 정의

다음과 같이 정의한다.

• \(t = u\) 를 \((\forall \mathbf{R}^{1})(\mathbf{R}^{1}t \iff \mathbf{R}^{1}u)\) 라고 정의한다.

• \(\mathbf{g}^{n} = \mathbf{h}^{n}\) 을 \(\forall \left< x \right>_{n}\left( \mathbf{g}^{n}\left( \left< x \right>_n \right) = \mathbf{h}^{n}\left( \left< x \right>_n \right) \right)\) 라고 정의한다.

• \(\mathbf{R}^{n} = \mathbf{S}^{n}\) 를 \(\forall \left< x \right>_n \left( \mathbf{R}^{n}\left( \left< x \right>_n \right) \iff \mathbf{S}^{n}\left( \left< x \right>_n \right) \right)\) 라고 정의한다.

표준 해석(standard interpretation)

언어 \(\operatorname{L2C}\) 와 영역 \(D\) 를 갖는 1차 논리 해석을 잡자. 1차 논리에서 만족을 정의할 때 \(D\) 의 원소로 이루어진 모든 가산 무한열 집합 \(\Sigma\) 를 잡았다. 2차 논리에서는 \(\Sigma\) 대신 다음과 같이 정의되는 함수 \(s\) 의 집합 \(\Sigma_{2}^{}\) 를 사용한다.

• \(D\) 의 원소를 각 개별 변수에 할당한다.
• 각 함수 변수 \(\mathbf{g}^{n}\) 에 \(D\) 의 어떤 \(n\)항 연산 \(s(\mathbf{g}^{n})\) 를 할당한다. \(s(\mathbf{g}^{n})\) 는 함수 \(D ^{n}\to D\) 이다.
• 각 술어 변수 \(\mathbf{R}^{n}\) 에 \(D\) 의 어떤 \(n\)항 관계 \(s(\mathbf{R}^{n})\) 를 할당한다. \(\mathbf{R}^{n}\) 은 곱집합 \(D ^{n}\) 의 부분집합이다.

각 \(s\) 마다 임의의 항 \(t_1, \dots, t_n\) 과 임의의 함수 변수 \(\mathbf{g}^{n}\) 에 대하여 표기 \(s(\mathbf{g}^{n}(t_1, \dots, t_n))\) 를 \(s(\mathbf{g}^{n})(s(t_1), \dots , s(t_n))\) 로 정의한다.

1차 논리의 만족의 정의를 다음과 같이 확장한다.

1. 임의의 술어 변수 \(\mathbf{R}^{n}\) 과 항의 임의의 유한열 \(\left< t \right>_n\) 에 대하여 \(s\) 가 \(\mathbf{R}^{n}(\left< t \right>_n)\) 를 만족한다는 것은 \(\left< s(t_1),\dots ,s(t_n) \right>\in s(\mathbf{R}^{n})\) 와 동치이다.
2. \(s\) 가 \((\forall \mathbf{g}^{n})B\) 를 만족한다는 것은 \(s\) 와 \(\mathbf{g}^{n}\) 에서만 다를 수도 있는 \(\Sigma_2\) 안의 모든 \(s'\) 이 \(B\) 를 만족한다는 것이다.
3. \(s\) 가 \((\forall \mathbf{R}^{n})B\) 를 만족한다는 것은 \(s\) 와 \(\mathbf{R}^{n}\) 에서만 다를 수도 있는 \(\Sigma_{2}^{}\) 안의 모든 \(s'\) 이 \(B\) 를 만족한다는 것이다.

위와 같이 정의된 해석 \(\mathcal{M}\) 을 언어 \(\operatorname{L2C}\) 의 표준 해석이라고 한다.

참(truth, 진리), 거짓(false)

식 \(B\) 가 표준해석 \(\mathcal{M}\) 에서 참이라는 것은 \(B\) 가 \(\Sigma_{2}^{}\) 의 모든 \(s\) 에 의하여 만족된다는 것이고, 이를 다음과 같이 표기한다.

\(B\) 가 \(\mathcal{M}\) 에서 거짓이라는 것은 \(B\) 를 만족하는 \(\Sigma_{2}^{}\) 의 함수 \(s\) 가 존재하지 않는다는 것이다.

표준적으로 타당하다(standardly valid), 표준적으로 만족가능한(standardly satisfiable), 표준적으로 논리적으로 함의(standardly logically implication)

식 \(B\) 가 모든 표준 해석에서 참이면 표준적으로 타당하다고 한다.

\(B\) 가 어떤 표준 해석의 \(\Sigma_{2}^{}\) 의 어떤 \(s\) 에 의하여 만족되면 표준적으로 만족가능하다고 한다.

모든 표준 해석에 대하여 \(\Gamma\) 안의 모든 식을 만족하는 \(\Sigma_{2}^{}\) 안의 모든 \(s\) 가 \(C\) 를 만족하면 식 \(C\) 를 식 집합 \(\Gamma\) 의 표준 논리적 귀결(standard logical consequence)이라고 한다.

\(C\) 가 \(\{B\}\) 의 논리적 귀결이면 식 \(B\) 가 표준적으로 논리적으로 식 \(C\) 를 함의한다고 한다.

다음의 \(\operatorname{L2}\) 문장이 표준해석에서 참인 것은 영역 \(D\) 가 유한하거나 가산무한인 것과 동치이다.

• \(\mathbf{Y}^{1} \subseteq \mathbf{X} ^{1}\): \((\forall u)(\mathbf{Y}^{1}(u) \implies \mathbf{X} ^{1}(u))\)
• \(\operatorname{NonEm}(\mathbf{X} ^{1})\): \((\exists u)(\mathbf{X} ^{1}(u))\)
• \(\operatorname{Asym}(\mathbf{R}^{2}, \mathbf{X} ^{1})\): \((\forall u)(\forall v)(\mathbf{X} ^{1}(u) \land \mathbf{X} ^{1}(v) \land \mathbf{R}^{2}(u, v) \implies \lnot \mathbf{R}^{2}(v, u))\)

• 2차 논리 식에 대한 정렬관계 \(\mathbf{R}^{2} \operatorname{We}\mathbf{X} ^{1}\) 를 다음과 같이 정의한다.

  \[ \begin{align}\begin{split} \operatorname{Asym}(&\mathbf{R}^{2}, \mathbf{X}^{1}) \land (\forall \mathbf{Y}^{1})\bigg ( \mathbf{Y}^{1}\subseteq \mathbf{X} ^{1} \land \operatorname{NonEm}(\mathbf{Y}^{1}) \\ &\implies (\exists u)\Big (\mathbf{Y}^{1}(u) \land (\forall v)\big (\mathbf{Y}^{1}(v) \land v \neq u \implies \mathbf{R}^{2}(u, v)\big )\Big )\bigg ) \\ \end{split}\end{align} \tag*{} \]

• \(\operatorname{Suc}(u,v,\mathbf{R}^{2})\): \(\mathbf{R}^{2}(v, u) \land (\forall w)\lnot \big (\mathbf{R}^{2}(v, w) \land \mathbf{R}^{2}(w, u)\big )\)

• \(\operatorname{First}(u, \mathbf{R}^{2})\): \((\forall v)(v \neq u \implies \mathbf{R}^{2}(u, v))\)

2차 논리 이론(second-order theory), 2차 논리 술어 계산(second-order predicate calculus)

1차 논리 공리과 추론 규칙에 다음과 같은 논리적 공리과 추론 규칙을 추가하여 언어 \(\operatorname{L2C}\) 에서의 2차 논리 이론을 정의한다.

• 논리적 공리

  • \(\text{(B4a)} \quad (\forall \mathbf{R}^{n})B(\mathbf{R}^{n})\implies B(\mathbf{W} ^{n}) \quad\) (\(B(\mathbf{W} ^{n})\) 는 \(B(\mathbf{R}^{n})\) 의 모든 자유인 \(\mathbf{R}^{n}\) 을 \(\mathbf{W} ^{n}\) 으로 교체한 것이고, \(\mathbf{W} ^{n}\) 은 \(B(\mathbf{R}^{n})\) 에서 \(\mathbf{R}^{n}\) 에 대하여 자유이다.)

  • \(\text{(B4b)} \quad (\forall \mathbf{g}^{n})B(\mathbf{g}^{n})\implies B(\mathbf{h} ^{n}) \quad\) (\(B(\mathbf{h} ^{n})\) 는 \(B(\mathbf{g}^{n})\) 의 모든 자유인 \(\mathbf{g}^{n}\) 을 \(\mathbf{h} ^{n}\) 으로 교체한 것이고, \(\mathbf{h} ^{n}\) 은 \(B(\mathbf{g}^{n})\) 에서 \(\mathbf{g}^{n}\) 에 대하여 자유이다.)

  • \(\text{(B5a)} \quad (\forall \mathbf{R}^{n})(B \implies C) \implies (B \implies (\forall \mathbf{R}^{n})C) \quad\) (\(\mathbf{R}^{n}\) 은 \(B\) 에서 자유가 아니다.)

  • \(\text{(B5b)} \quad (\forall \mathbf{g}^{n})(B \implies C) \implies (B \implies (\forall \mathbf{g}^{n})C) \quad\) (\(\mathbf{g}^{n}\) 은 \(B\) 에서 자유가 아니다.)

  • Comprehension Schema(\(\text{Comp}\)): \((\exists \mathbf{R}^{n})(\forall \left< x \right>_n)(\mathbf{R}^{n}(\left< x \right>_n) \iff B) \quad\) (\(B\) 의 모든 자유변수가 \(\left< x \right>_n\) 에서 나타나고, \(\mathbf{R}^{n}\) 은 \(B\) 에서 자유가 아니다.)

  • Function Definition Schema(\(\text{FunDef}\)):

    \[ \begin{align}\begin{split} (\forall \mathbf{R}^{n+1})\Big [&(\forall \left< x \right>_n) (\exists _1 y)\mathbf{R}^{n+1} (\left< x \right>_n, y) \\ & \implies (\exists \mathbf{g}^{n})(\forall \left< x \right>_n) \mathbf{R}^{n+1}\big (\left< x \right>_n, \mathbf{g}^{n}(\left< x \right>_n)\big )\Big ] \\ \end{split}\end{align} \tag*{} \]

• 추론 규칙

  • \(\text{(Gen2a)}\) \(B\) 에서 \((\forall \mathbf{R}^{n})B\) 가 도출된다.
  • \(\text{(Gen2b)}\) \(B\) 에서 \((\forall \mathbf{g}^{n})B\) 가 도출된다.

언어 \(\operatorname{L2C}\) 에서 비논리 공리를 갖지 않는 2차 논리 이론을 \(\operatorname{PC2}\) 라고 표기하고, 2차 논리 술어 계산이라고 한다.

정리 A.1 건전성(Soundness)

\(\operatorname{PC2}\) 의 정리는 표준적으로 타당하다.

정리 A.2 반복 정리(Iteration Theorem)

\(\operatorname{AR2}\) 의 모델인 표준 해석 \(\mathcal{M}\) 과 \(\mathcal{M}\) 의 영역 \(D\) 를 잡자. 임의의 집합 \(W\) 의 원소 \(c\) 와, \(W\) 의 단항 연산 \(g\) 를 잡자. 그러면 다음을 만족하는 \(D\) 위에서 정의된 함수 \(F\) 가 유일하게 존재한다.

• \(F(0) = c\)
• \((\forall x)(x \in D \implies F(x') = g(F(x)))\)

정리 A.3 \(\operatorname{AR2}\) 의 유일성

\(\operatorname{AR2}\) 의 모델인 두 표준 해석 \(\mathcal{M}\) 과 \(\mathcal{M}^{*}\) 은 동형이다.

정리 A.4

\(\mathcal{A}\) 가 형식적 산술의 비논리 상수(\(0\), \('\), \(+\), \(\cdot\), \(=\))로 구성되었다고 하자. 자연수 집합을 영역으로 갖고 비논리 상수에 대한 보통의 해석을 갖는 \(\operatorname{L2}\mathcal{A}\) 의 표준해석을 \(\mathcal{N}\) 이라고 하자.

\(\operatorname{L2}\mathcal{A}\) 의 임의의 식 \(B\) 에 대하여 \(B\) 가 \(\mathcal{N}\) 에서 참인 것은 \(\operatorname{AR2}\implies B\) 가 표준적으로 타당한 것과 동치이다.

정리 A.5

1. \(\operatorname{L2}\mathcal{A}\) 의 표준적으로 타당한 식의 집합 \(\operatorname{SV}\) 는 효과적으로 열거가능하지 않다.
2. \(\operatorname{SV}\) 는 재귀적으로 열거가능하지 않다. 즉, \(\operatorname{SV}\) 의 식의 괴델수의 집합은 재귀적으로 열거가능하지 않다.

따름정리 A.6

모든 표준적으로 타당한 식의 집합은 효과적으로(또는 재귀적으로) 열거 가능하지 않다.

따름정리 A.7

정리가 \(\operatorname{L2}\mathcal{A}\) 의 표준적으로 타당한 식이 되는 공리적 형식 체계는 존재하지 않는다.

정리 A.8 표준 의미의 불완전성(Incompleteness of Standard Semantics)

정리가 모든 표준적으로 타당한 식이 되는 공리적 형식 체계는 존재하지 않는다.