본문 바로가기
Topos Uranos
한국어

메타이론: 종합과 도전 과제

요약

이 수업은 메타이론에 바친 단원을 마무리하고, 그와 함께 강좌의 내용을 마무리한다. 이 수업은 연역의 사슬을 재구성한다. 곧 공리의 타당성에서 체계의 건전성으로, 부정논리합에 관한 두 보조정리에서 칼마르 보조정리를 거쳐 유한한 전제에 대한 완전성으로, 두 증인 보조정리에서 콤팩트성 정리로, 그리고 이를 통해 강한 완전성으로, 절 형식에서 분해의 건전성과 반박 완전성으로 이어지는 사슬이며, 각 고리마다 어떤 결과를 사용하고 어느 수업에서 증명되었는지를 밝힌다. 또한 강좌의 앞선 세 부분, 곧 언어, 연역, 의미론이 ⊢\vdash 식과 ⊨\models 식의 일치로 어떻게 수렴하는지, 그리고 각각이 이 일치에 무엇을 보태는지를 보이고, 강좌가 증명한 것, 인정한 것, 열어 둔 것을 구별한다. 마무리 평가에서는 입문 평가의 기능을 되풀이하고, 끝으로 수업의 연습 문제보다 어렵고 여러 수업의 도구를 결합해야 하는 여섯 개의 도전 과제를 제시한다.

학습 목표

  1. 단원의 결과들의 논리적 순서를 재구성하고, 각 결과가 어떤 앞선 결과에 기대며 어느 수업에서 증명되었는지를 밝히며, 콤팩트성과 강한 완전성의 순서의 이유를 설명한다.
  2. 언어, 연역, 의미론이 ⊢\vdash 식과 ⊨\models 식의 일치로 어떻게 수렴하는지, 그리고 강좌의 각 단원의 어떤 결과가 이 일치에 없어서는 안 되는지를 설명한다.
  3. 강좌가 증명한 것을 인정한 것(공리 도식, 원시 규칙, 귀납법)과 열어 둔 것(충족 가능성을 결정하는 비용과 양화사가 있는 논리)으로부터 구별한다.
  4. 표지, 칼마르 보조정리, 균일 대입, 콤팩트성, 분해를 결합하는 문제를 풀되, 각 경우에 일치의 쉬운 쪽을 이용한다.

단원에서 얻은 것

이 단원의 목표는 앞선 단원들이 같은 언어 위에 세운 두 관계, 곧 연역 가능성 Γ⊢φ\Gamma \vdash \varphi 관계와 의미론적 귀결 Γ⊨φ\Gamma \models \varphi 관계를 비교하고, 둘이 일치함을 증명하는 것이었다. 이 목표는 진술로서는 유보 없이 달성되었다. 유한하든 무한하든 임의의 전제 집합에 대해 두 관계는 같은 관계이며, 분해는 귀결을 결정하는 세 번째 방법을 주는데, 이 역시 건전하고 완전하다. 유보는 방법에 있으며, 각각은 제자리에서 언급되었다. 첫 수업의 완전성은 구성적이지만 실용적이지 않다. 그것이 만들어 내는 연역은 진리표만큼 길기 때문이다. 콤팩트성은 할당의 존재를 보장하지만 그것을 찾는 법은 가르쳐 주지 않는다. 분해는 결정하지만, 최악의 경우의 비용은 열린 문제이다. 이러한 유보를 안고서 보면, 지나온 길은 네 구간으로 이루어진 연역의 사슬로 읽을 수 있다.

건전성

건전성과 완전성에 관한 수업은 먼저 용어를 정했다. 체계는 Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi 조건이 성립하면 건전하고, 그 역이 성립하면 완전하며, 완전성에는 세 단계(약한 완전성, 유한 집합에 대한 완전성, 강한 완전성)가 있다. 이 수업은 완전성을 “건전성에 의해” 얻으려는 순환 논증의 정체를 드러냈다. 그 논증은 ⊬χ\nvdash \chi 조건에서 ⊭χ\not\models \chi 조건으로 넘어가는데, 이 걸음은 사실 약한 완전성의 대우이다. 또한 이 수업은 두 성질이 서로 독립임을 보였다. 이어서 A1, A2, A3의 각 대입례가 타당함을 증명했다. 그것을 거짓으로 만드는 할당을 가정하면 함의의 거짓 행 때문에 불가능한 값에 이르기 때문이다. 그리고 건전성을 행의 수에 대한 강한 귀납법으로 증명했다. 공리의 경우, 전제의 경우, 의미론적 전건 긍정식의 경우가 있고, RDN 규칙(이중 부정 대체)에 대해서는 동치 θ≡¬¬θ\theta \eqsem \neg\neg\theta 식과 의미론적 대체 정리를 쓴다. 행에서 행으로 전해지는 성질은 타당성이 아니라 전제를 충족하는 하나의 고정된 할당에 의해 충족된다는 것이며, 그래서 건전성은 전제가 있을 때에도, 전제가 무한할 때에도 성립한다. 그로부터 충족 가능한 집합의 무모순성, 특히 체계 자체의 무모순성이 따르고, 또한 연역 단원에는 없던 방법, 곧 반례 모형으로 어떤 연역이 존재하지 않음을 증명하는 방법이 따른다.

칼마르와 유한 완전성

같은 수업은 그 역을 두 단계로 증명했다. 첫 단계는 칼마르 보조정리이다. φ\varphi 식의 변항이 모두 u1,…,unu_{1}, \ldots, u_{n} 집합 안에 있으면, {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v} 관계가 모든 할당 vv에 대해 성립한다. 여기서 ψv\psi^{v} 식은 ψ\psi 식(v(ψ)=1v(\psi) = 1 조건일 때)이거나 ¬ψ\neg\psi 식(그렇지 않을 때)이다. 체계는 각 행으로부터 그 행이 식에 대해 말하는 것을 연역한다. 복잡도에 대한 귀납에는 합성된 경우가 하나뿐이다. 곧 (α↓β)(\alpha \downarrow \beta) 식의 경우이며, 부정논리합이 유일한 원시 연결사이기 때문이다. 그 경우에는 세 하위 경우가 있고, 이들은 체계의 두 보조정리를 요구하며, 둘째 보조정리는 두 형태를 가진다. ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))) 관계는 연언 도입, 이중 부정, RDN 규칙의 두 번 적용으로 연역되고, ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) 관계와 ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)) 관계는 선언 도입으로 연역된다. 둘째 단계는 전제를 제거한다. φ\varphi 식이 항진식이면, 그것은 2n2^{n} 개의 행 각각의 전제로부터 연역되며, 경우에 따른 증명이 마지막 변항의 리터럴, 이어서 끝에서 두 번째 변항의 리터럴을 제거해 나가 ⊢φ\vdash \varphi 관계에 이른다. 이것이 약한 완전성이다. 의미론적 연역 정리와 구문론적 연역 정리의 역에 의해 완전성은 유한한 전제 집합으로 확장되었다. 따라서 유한한 전제에 대해서는 연역과 귀결이 일치하고, 증명 가능한 동치가 의미론적 동치와 일치하며, 진리표가 답해 주므로 연역 가능성은 결정 가능하다.

콤팩트성과 강한 완전성

콤팩트성 정리에 관한 수업은 칼마르 보조정리가 닿지 못하는 무한한 경우를 다루었다. 무한히 많은 전제는 하나의 함의로 옮겨 넣을 수 없기 때문이다. 이 수업은 연역을 전혀 언급하지 않고, 집합이 충족 가능할 필요충분조건은 그 유한 부분집합이 모두 충족 가능하다는 것임을 증명했다. v1,…,vnv_{1}, \ldots, v_{n} 변항들에 대한 값의 열은, 집합의 모든 유한 부분집합이 그 열을 연장하는 어떤 할당에 의해 충족될 때 좋은 열이라 한다. 두 증인 보조정리는 좋은 열이 좋은 열로 연장됨을 보장한다. 두 연장이 모두 좋지 않다면, 두 유한한 증인의 합집합이 그 열이 좋다는 것과 모순되기 때문이다. 그리고 가능할 때마다 11 값을 우선하여 얻은 할당은 각 식을 충족한다. 이는 일치 보조정리에서 따르는데, 각 식은 유한히 많은 변항만을 가지기 때문이다. 이 구성은 선택 공리를 필요로 하지 않는다. 변항에는 번호가 매겨져 있고 각 단계에 규칙이 있기 때문이다. 콤팩트성으로부터 그 동치인 형태들, 곧 충족 불가능성의 형태와 귀결의 형태가 따랐다. 뒤의 것과 유한한 전제에 대한 완전성과 단조성으로부터 강한 완전성이 따랐고, 강한 완전성과 건전성으로부터 완전한 일치가 따랐다. 곧 Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi 관계가 모든 Γ\Gamma 집합에 대해 성립하며, 집합이 무모순일 필요충분조건은 충족 가능하다는 것이다. 이 수업은 이 순서가 취향의 문제가 아님을 경고했다. 아직 얻지 못한 강한 완전성으로부터 콤팩트성을 얻는 것은 순환이 될 것이기 때문이다. 수업은 가산 그래프의 채색으로 끝났는데, 이는 무한한 문제를 유한 부분들이 충족 가능한 식의 집합으로 옮기는 것이다. 또한 식의 집합이 표현할 수 있는 것의 한계도 다루었다.

분해

분해 방법에 관한 수업은 식의 집합을 절의 집합으로 바꾸었다. 절은 리터럴의 유한 집합이며, 두 가지 표현이 있다. 하나는 절 형식으로, 같은 모형을 가진다. 다른 하나는 정의적 형식으로, 합성된 각 부분 표기에 새 변항을 도입하며, 충족 가능성만을 보존하고, 2의 거듭제곱처럼이 아니라 식처럼 커진다. 절 위에서는 단 하나의 규칙이 작용한다. CC 절과 DD 절로부터, ℓ∈C\ell \in C 조건과 ℓ∗∈D\ell^{*} \in D 조건 아래에서, (C∖{ℓ})∪(D∖{ℓ∗})(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\}) 절을 얻는다. 반박은 □\Box 절에 이르는 도출이다. 건전성은 체계의 건전성처럼 도출에 대한 귀납으로, 분해식이 그 전제들의 귀결임을 이용해 증명되었고, 반박 완전성은 변항의 개수에 대한 귀납으로, 한 변항의 제거를 통해 증명되었다. 이 제거는 충족 가능성을 보존하며, 그 증명은 모형을 구성한다. 무한 집합에 대해서는 다시 콤팩트성에 의한다. 이로부터 Γ⊨φ\Gamma \models \varphi 관계가 성립할 필요충분조건은 Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} 집합의 절 형식이 반박을 가진다는 것임이 따른다. 또한 포화는 유한하다. nn 개의 변항으로는 절이 4n4^{n} 개를 넘지 않기 때문이다. 포화는 진리표 없이 충족 가능성을 결정한다. 이 수업은 최악의 경우의 비용을 아무도 모르는 충족 가능성 문제와, 빨리 결정되는 두 경우, 곧 혼 절과 두 리터럴로 된 절을 소개했다.

다음 그림은 네 구간을 하나의 사슬로 모은다. 가운데 열의 각 마디는 하나의 결과이며, 논리적 순서에 따라 번호가 매겨져 있고, 그 증명이 사용하는 앞선 고리들과 호로 이어져 있다. 주위에는 받침들, 곧 사슬이 거듭 의지하는 원리와 도구가 떠 있다. 각 받침은 그것에 기대는 고리들과는 실선으로, 그것이 확립되는 고리와는 점선으로 이어져 있으며, 앞선 단원에서 온 받침들은 둥근 테로 그려진다. 받침을 누르면 그것을 사용하는 모든 고리가 강조되고, 각 고리는 그것이 증명된 수업으로 연결된다. 건전성과 콤팩트성이, 하나는 첫째 구간에서, 다른 하나는 셋째 구간에서 확립되어 뒤따르는 구간들에 다시 나타난다는 것, 그리고 단원에서 가장 자주 찾는 받침은 할당과 일치이고, 그다음이 세 가지 형태의 귀납법, 곧 연역의 행에 대한, 식의 복잡도에 대한, 절 집합의 변항 개수에 대한 귀납법이라는 것에 주목하라.

사슬의 받침

  • A귀납법과 재귀. 자연수에 대한 강한 귀납법, 식의 복잡도에 대한 귀납법(유일한 합성된 경우는 (α↓β)(\alpha \downarrow \beta) 식), 그리고 재귀에 의한 정의. 첫째 단원에서 증명되었다. 이 단원에서는 증명 없이 받아들인다.
  • B강좌의 체계. A1, A2, A3, 전건 긍정식과 RDN 규칙. 반사성, 단조성, 연역 사이의 전건 긍정식, 유한성, 그리고 Γ∪{φ}⊢ψ⇔Γ⊢(φ→ψ)\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi) 성질. 둘째 단원에서 정해졌다. 이 단원에서는 증명 없이 받아들인다.
  • C유도된 기법. 이중 부정은 네 가지 연역 기법에 관한 수업에서, 연언 도입, 선언 도입, 경우에 따른 증명(Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi 관계와 Γ∪{¬ψ}⊢χ\Gamma \cup \{\neg\psi\} \vdash \chi 관계이면 Γ⊢χ\Gamma \vdash \chi 관계)은 고전 논리의 기법에 관한 수업에서 나왔다. 둘째 단원에서 증명되었다. 이 단원에서는 증명 없이 받아들인다.
  • D할당과 일치. v((α↓β))=(1−v(α))(1−v(β))v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta)) 등식. 두 할당이 V(φ)V(\varphi) 집합 위에서 일치하면 φ\varphi 식에 같은 값을 준다. 타당성은 2n2^{n} 개의 행으로 결정된다. 셋째 단원에서 증명되었다. 이 단원에서는 증명 없이 받아들인다.
  • E의미론적 귀결. 함의의 거짓 행, 단조성, Γ∪{φ}⊨ψ⇔Γ⊨(φ→ψ)\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi) 관계, Γ⊨φ\Gamma \models \varphi 관계가 성립할 필요충분조건은 Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} 집합이 충족 불가능하다는 것, 그리고 의미론적 대체 정리. 셋째 단원에서 증명되었다. 이 단원에서는 증명 없이 받아들인다.
  • F연언 형식. 값 보조정리. 모든 식은 연언 표준형과 동치이며, 이 표준형은 2n2^{n} 개의 절을 필요로 할 수 있다. 리터럴의 선언이 타당할 필요충분조건은 상보 쌍을 포함하는 것이다. 셋째 단원에서 증명되었다. 이 단원에서는 증명 없이 받아들인다.
  • G건전성. Γ⊢φ\Gamma \vdash \varphi 관계이면 Γ⊨φ\Gamma \models \varphi 관계이며, 이는 모든 집합 Γ\Gamma에 대해 성립한다. 반례 모형은 어떤 연역이 존재하지 않음을 증명한다. 확립되는 곳: 2. 건전성.
  • H콤팩트성. 식의 집합이 충족 가능할 필요충분조건은 그 유한 부분집합이 모두 충족 가능하다는 것이다. 따라서 충족 불가능한 집합은 이미 어떤 유한 부분에서 충족 불가능하다. 확립되는 곳: 11. 콤팩트성 정리.

  1. 제1구간 건전성

    • 진리표를 만들지 않고 도식의 각 대입례가 타당함을 확인한다.
    • RDN 규칙의 경우를 포함하여, 행의 수에 대한 강한 귀납법으로 건전성을 증명한다.
    • 반례 모형으로 어떤 식이 연역 가능하지 않음을 증명하고, 건전성으로부터 무모순성을 이끌어 낸다.

    1. 공리의 타당성. A1, A2, A3의 각 대입례는 타당하다. 그것을 거짓으로 만드는 할당은 함의의 거짓 행 때문에 불가능한 값을 요구하게 된다.

      받침: E (의미론적 귀결). 증명된 수업: 건전성과 완전성.

    2. 건전성. Γ⊢φ\Gamma \vdash \varphi 관계이면 Γ⊨φ\Gamma \models \varphi 관계이며, 이는 모든 Γ\Gamma 집합에 대해 성립한다. 행의 수에 대한 강한 귀납법으로, 공리의 경우, 전제의 경우, 의미론적 전건 긍정식, 그리고 RDN 규칙에는 θ≡¬¬θ\theta \eqsem \neg\neg\theta 식과 의미론적 대체를 쓴다.

      사용: 1. 공리의 타당성. 받침: A (귀납법과 재귀), B (강좌의 체계), E (의미론적 귀결). 증명된 수업: 건전성과 완전성.

    3. 무모순성과 반례 모형. 충족 가능한 집합은 모두 무모순이다. 체계는 무모순이며 ⊬v1\nvdash v_{1} 관계가 성립한다. 어떤 할당이 Γ\Gamma 집합을 충족하고 φ\varphi 식을 거짓으로 만들면 Γ⊬φ\Gamma \nvdash \varphi 관계가 성립하며, 진리표가 이를 증명한다. 타당하지 않은 것은 정리가 아니다.

      받침: G (건전성), D (할당과 일치). 증명된 수업: 건전성과 완전성.

  2. 제2구간 칼마르와 유한 완전성

    • 부정논리합에 관한 두 보조정리를, 필요하면 RDN 규칙을 써서 체계 안에서 연역한다.
    • 칼마르 보조정리를 합성된 경우가 하나뿐인 복잡도에 대한 귀납으로 증명한다.
    • 경우에 따른 증명으로 행의 전제를 제거하고, 두 연역 정리로 유한한 전제를 내려놓는다.
    • 유한한 전제 아래의 연역 가능성, 증명 가능한 동치, 무모순성을 진리표로 결정한다.

    1. 부정논리합의 도입. {¬α,¬β}⊢(α↓β)\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta) 관계와 ⊢(¬α→(¬β→(α↓β)))\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta))) 관계. 부정들의 연언은 ¬¬(¬¬α↓¬¬β)\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta) 식이다. 이중 부정이 바깥 부정을 없애고, RDN 규칙이 안쪽의 두 부정을 없앤다.

      받침: B (강좌의 체계), C (유도된 기법). 증명된 수업: 건전성과 완전성.

    2. 부정논리합의 부정. ⊢(α→¬(α↓β))\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta)) 관계와 ⊢(β→¬(α↓β))\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta)) 관계. ¬(α↓β)\neg(\alpha \downarrow \beta) 식은 (α∨β)(\alpha \vee \beta) 식이므로 선언 도입으로 충분하다.

      받침: B (강좌의 체계), C (유도된 기법). 증명된 수업: 건전성과 완전성.

    3. 칼마르 보조정리. V(φ)⊆{u1,…,un}V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\} 조건이면 {u1v,…,unv}⊢φv\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v} 관계가 모든 할당 vv에 대해 성립한다. 귀납 단계에는 경우가 하나뿐이며, 곧 (α↓β)(\alpha \downarrow \beta) 식이고, α\alpha 식과 β\beta 식의 값에 따라 세 하위 경우로 나뉜다.

      사용: 4. 부정논리합의 도입, 5. 부정논리합의 부정. 받침: A (귀납법과 재귀), D (할당과 일치), B (강좌의 체계). 증명된 수업: 건전성과 완전성.

    4. 약한 완전성. ⊨φ\models \varphi 관계이면 ⊢φ\vdash \varphi 관계이다. 칼마르 보조정리가 각 행으로부터 φ\varphi 식을 연역하고, 경우에 따른 증명이 마지막 변항부터 첫 변항까지 리터럴을 제거한다. 보조정리는 2n2^{n} 번, 경우에 따른 증명은 2n−12^{n} - 1 번 쓰인다.

      사용: 6. 칼마르 보조정리. 받침: C (유도된 기법). 증명된 수업: 건전성과 완전성.

    5. 유한한 전제에 대한 완전성. {γ1,…,γk}⊨φ⇒{γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi 관계. 의미론적 연역 정리가 항진식으로 이끌고, 약한 완전성이 그것을 연역하며, 연역 정리의 역이 전제를 되돌려 놓는다.

      사용: 7. 약한 완전성. 받침: E (의미론적 귀결), B (강좌의 체계). 증명된 수업: 건전성과 완전성.

    6. 유한한 일치와 결정. 유한한 Γ\Gamma 집합에 대해 Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi 관계와 φ⊣⊢ψ⇔φ≡ψ\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi 관계가 성립한다. 따라서 유한한 전제로부터의 연역 가능성은 진리표에 의해 결정 가능하다.

      사용: 8. 유한한 전제에 대한 완전성. 받침: G (건전성), D (할당과 일치). 증명된 수업: 건전성과 완전성.

  3. 제3구간 콤팩트성과 강한 완전성

    • 변항의 값을 하나씩 고정하여 콤팩트성을 증명하되, 좋은 열이라는 불변량과 두 증인의 논증을 이용한다.
    • 충족 가능성의 형태, 충족 불가능성의 형태, 귀결의 형태 사이를 오간다.
    • 순환 없이 콤팩트성으로부터 강한 완전성을 얻고, 그로부터 무모순성과 충족 가능성의 일치를 얻는다.
    • 무한한 대상에 관한 문제를 식의 집합으로 부호화하고 콤팩트성으로 푼다.

    1. 두 증인 보조정리. 이미 고정된 값의 열 ss 열이 좋으면(집합의 모든 유한 부분집합이 그 열을 연장하는 어떤 할당에 의해 충족되면), (s,1)(s, 1) 열 또는 (s,0)(s, 0) 열이 좋다. 둘 다 좋지 않다면, 두 유한한 증인의 합집합이 ss 열이 좋다는 것과 모순된다.

      받침: D (할당과 일치). 증명된 수업: 콤팩트성 정리.

    2. 콤팩트성 정리. Γ\Gamma 집합이 충족 가능할 필요충분조건은 그 유한 부분집합이 모두 충족 가능하다는 것이다. vn+1v_{n + 1} 변항을 11 값으로((sn,1)(s_{n}, 1) 열이 좋으면), 그렇지 않으면 00 값으로 고정하면, 얻어진 할당은 일치 보조정리에 의해 각 식을 충족한다. 변항에 번호가 매겨져 있으므로 선택 공리는 필요 없다.

      사용: 10. 두 증인 보조정리. 받침: A (귀납법과 재귀), D (할당과 일치). 증명된 수업: 콤팩트성 정리.

    3. 동치인 형태들. Γ\Gamma 집합이 충족 불가능할 필요충분조건은 그 어떤 유한 부분이 충족 불가능하다는 것이다. Γ⊨φ\Gamma \models \varphi 관계가 성립할 필요충분조건은 Γ0⊨φ\Gamma_{0} \models \varphi 관계가 어떤 유한한 Γ0⊆Γ\Gamma_{0} \subseteq \Gamma 집합에 대해 성립한다는 것이다. 그리고 이 마지막 형태는 거꾸로 정리를 함의한다.

      사용: 11. 콤팩트성 정리. 받침: E (의미론적 귀결). 증명된 수업: 콤팩트성 정리.

    4. 강한 완전성. Γ⊨φ\Gamma \models \varphi 관계이면 Γ⊢φ\Gamma \vdash \varphi 관계이며, 이는 모든 Γ\Gamma 집합에 대해 성립한다. 귀결의 형태가 유한한 Γ0\Gamma_{0} 집합을 주고, 유한한 전제에 대한 완전성이 Γ0⊢φ\Gamma_{0} \vdash \varphi 관계를 주며, 단조성이 Γ⊢φ\Gamma \vdash \varphi 관계를 준다.

      사용: 8. 유한한 전제에 대한 완전성, 12. 동치인 형태들. 받침: B (강좌의 체계). 증명된 수업: 콤팩트성 정리.

    5. 연역은 귀결이다. Γ⊢φ⇔Γ⊨φ\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi 관계가 모든 Γ\Gamma 집합에 대해 성립한다. 정리는 정확히 항진식이며, 집합이 무모순일 필요충분조건은 충족 가능하다는 것이다.

      사용: 13. 강한 완전성. 받침: G (건전성). 증명된 수업: 콤팩트성 정리.

    6. 가산 그래프의 채색. 각 꼭짓점과 각 색에 대해 xi,cx_{i,c} 변항을 두고, 각 꼭짓점이 정확히 한 색을 가지며 이웃한 꼭짓점은 서로 다른 색을 가진다는 식들을 두면, 가산 그래프는 그 유한 부분 그래프가 모두 kk 가지 색으로 채색 가능할 때 그 자신도 채색 가능하다.

      받침: H (콤팩트성), F (연언 형식). 증명된 수업: 콤팩트성 정리.

  4. 제4구간 분해

    • 식의 집합을 연언 형식이나 정의적 형식으로 절의 집합으로 나타낸다.
    • 한 단계에서 두 상보 쌍을 제거하지 않고 반박을 만든다.
    • 분해의 건전성과 반박 완전성을, 먼저 유한 집합에 대해, 이어서 콤팩트성으로 임의의 집합에 대해 증명한다.
    • 포화로 귀결을 결정하고, 빨리 결정되는 경우를 알아본다.

    1. 절 형식. 절은 리터럴의 유한 집합이며, 어떤 리터럴이 11 값을 가질 때 충족되고, □\Box 절은 충족 불가능하다. Γ\Gamma 집합의 절 형식은 같은 모형을 가지며, Γ⊨φ\Gamma \models \varphi 관계가 성립할 필요충분조건은 Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} 집합의 절 형식이 충족 불가능하다는 것이다.

      받침: F (연언 형식), E (의미론적 귀결). 증명된 수업: 분해 방법.

    2. 정의적 절 형식. 각 부분 표기에 새 변항과 그 정의 절을 두면, T(φ)T(\varphi) 집합과 φ\varphi 집합은 동등 충족 가능하고, 절은 많아야 4k+14k + 1 개이며, 각 절의 리터럴은 많아야 세 개이다. 정의적 형식은 유한한 전제 아래의 귀결을 결정한다.

      사용: 16. 절 형식. 받침: A (귀납법과 재귀), D (할당과 일치). 증명된 수업: 분해 방법.

    3. 분해의 건전성. {C,D}⊨Rℓ(C,D)\{C, D\} \models R_{\ell}(C, D) 관계는 ℓ\ell 변항의 값에 따른 경우 나누기로 보인다. 도출에 대한 강한 귀납법으로, S⊨CS \models C 관계는 모든 절 CC 절에 대해, 그것이 SS 집합으로부터 도출되기만 하면 성립한다. SS 집합이 반박을 가지면 그것은 충족 불가능하다.

      사용: 16. 절 형식. 받침: A (귀납법과 재귀). 증명된 수업: 분해 방법.

    4. 한 변항의 제거. Ep(S)E_{p}(S) 집합은 pp 리터럴도 ¬p\neg p 리터럴도 없는 절을 남기고 pp 변항에 관한 분해식을 더한 것으로, pp 변항을 포함하지 않으며 SS 집합과 동등 충족 가능하다. 그 모형으로부터 SS 집합의 모형을 얻는데, pp 변항의 값을 고르면 된다.

      사용: 18. 분해의 건전성. 받침: D (할당과 일치). 증명된 수업: 분해 방법.

    5. 유한한 반박 완전성. 유한하고 충족 불가능한 절의 집합은 모두 반박을 가진다. 변항의 개수에 대한 귀납으로, 마지막 변항을 제거하고 각 분해식의 전제들을 끼워 넣는다.

      사용: 19. 한 변항의 제거. 받침: A (귀납법과 재귀). 증명된 수업: 분해 방법.

    6. 반박 완전성. 절의 집합은 유한하든 무한하든 충족 불가능할 필요충분조건이 반박을 가진다는 것이다. 따라서 Γ⊨φ\Gamma \models \varphi 관계가 성립할 필요충분조건은 Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} 집합의 절 형식이 반박을 가진다는 것이다.

      사용: 16. 절 형식, 18. 분해의 건전성, 20. 유한한 반박 완전성. 받침: H (콤팩트성). 증명된 수업: 분해 방법.

    7. 포화는 결정한다. nn 개의 변항으로는 도출되는 절의 집합이 많아야 4n4^{n} 개의 원소를 가진다. 포화는 멈추며, 진리표 없이 충족 가능성을 결정하지만, 언제나 진리표보다 빠른 것은 아니다.

      사용: 18. 분해의 건전성, 20. 유한한 반박 완전성. 증명된 수업: 분해 방법.

강좌가 이른 곳. 사슬은 강좌의 두 얼굴이 하나의 같은 관계로 인식되고 그것을 결정하는 방법이 마련된 곳에서 끝난다. 열린 채로 남은 것은 더 이상 명제 논리에 관한 물음이 아니라, 그 비용과 양화사로의 확장에 관한 물음이다.