본문 바로가기
Topos Uranos
한국어

형식 연역 체계

요약

이 수업은 앞 단원의 언어를 증명의 도구로 바꾼다. 형식 연역 체계가 무엇인지(하나의 언어, 몇 개의 공리 도식, 몇 개의 추론 규칙)를 정의하고, 이 강좌가 다루는 두 체계 가운데 첫 번째인 우카시에비치 체계를 소개한다. 이 체계는 세 개의 공리 도식과 유일한 규칙인 전건 긍정식(modus ponens)으로 이루어진다. 전제 집합으로부터의 연역, 정리, 그리고 관계 Γ⊢φ\Gamma \vdash \varphi를 정확히 정의하고, ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)를 다섯 행으로 연역하며, 연역의 구조적 성질인 반사성, 단조성, 연역 사이의 전건 긍정식, 절단, 유한성을 증명한다. 이어서 행의 수에 관한 강한 귀납법으로 연역 정리와 그 역을 증명하는데, 이 둘은 연역에 관한 연역으로 추론할 수 있게 해 준다. 그리고 증명 가능한 동치를 정의한다. 끝으로, 진리값에 기대지 않고, 부정논리합을 유일한 연결사로 갖는 언어에서 이 체계의 한계를 확립한다. 논리식에 관한 재귀로 계산되는 00과 11의 표지는 우카시에비치 공리와 전건 긍정식에 의해 보존되며, 연역되어야 할 어떤 논리식들이 연역되지 않는다는 것, 나아가 (v1↓v2)(v_{1} \downarrow v_{2})에서 (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2})로 넘어가는 것조차 불가능하다는 것을 증명한다. 여기서 두 번째 규칙, 곧 이중 부정 대체가 필요해지며, 다음 수업은 이 규칙으로 체계를 완성한다.

학습 목표

  1. 공리 도식 A1, A2, A3의 대입례를 알아보고, 논리식의 나열이 전제 집합으로부터의 연역인지 판정한다.
  2. 우카시에비치 체계에서 공리, 전제, 전건 긍정식으로 연역을 구성하고, 반사성, 단조성, 절단, 연역 정리와 그 역으로 연역에 관한 연역을 구성한다.
  3. 연역의 구조적 성질과 연역 정리를 행의 수에 관한 강한 귀납법으로 증명한다.
  4. 증명 가능한 동치를 확립하고, 증명 가능한 동치가 반사적, 대칭적, 추이적이라는 사실을 사용한다.
  5. 공리와 전건 긍정식이 보존하는 표지를 이용해 어떤 논리식이 연역 가능하지 않음을 증명하고, 이를 통해 연결사가 하나뿐인 언어에서 우카시에비치 체계의 한계와 두 번째 규칙이 필요한 이유를 설명한다.

형식 연역 체계란 무엇인가

앞 단원은 하나의 언어를 구성했다. 곧 원과 원판으로 된 어떤 기호열이 논리식인지를 정했을 뿐, 그 이상은 하지 않았다. 그러나 언어는 그 자체로는 아무것도 주장하지 않고 아무것도 증명하지 않는다. 증명하려면 그 밖에도 출발점과 나아가는 방식이 필요하다. 따라서 형식 연역 체계는 세 가지 구성 요소로 이루어진다. 논리식을 정하는 형식 언어, 증명 없이 받아들이는 논리식인 공리의 집합, 그리고 이미 쓴 다른 논리식들로부터 어떤 논리식을 쓸 수 있는지를 말해 주는 추론 규칙의 집합이다. 결정적인 것은 이 세 가지가 모두 순수하게 구문론적이라는 점이다. 어떤 논리식이 공리인지, 또는 어떤 규칙이 올바르게 적용되었는지를 확인하려면 기호열을 보기만 하면 되고, 그것이 무엇을 뜻하는지 물을 필요가 없다. 그렇다면 형식 체계에서의 증명은 기호 하나하나 기계적으로 검사할 수 있으며, 그 모든 가치는 바로 이 가능성에 있다.

처음부터 짚어 둘 것은, 여기서 공리가 이 낱말의 옛 용법에서처럼 “자명한 진리”가 아니라 출발점으로 선택된 논리식이라는 점이다. 그 선택이 적절한지(공리가 의미론이 밝혀 줄 어떤 의미에서 참인지, 그리고 연역되어야 할 모든 것을 연역하기에 충분한지)는 체계에 관한 물음이며, 직관이 아니라 체계에 관한 정리로 답한다. 메타이론 단원이 이 물음에 답하며, 이 수업의 마지막 절은 이 물음이 쓸데없지 않음을 보여 준다.

공리 도식과 대입례

명제 논리의 체계들은 공리가 무한히 많기 때문에 그것을 하나씩 진술하지 않고 도식으로 진술한다. 도식이란 (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi))처럼 메타변항으로 쓴 메타언어의 표현이다. 도식은 논리식이 아니라 틀이다. 도식의 대입례란 각 메타변항에 어떤 논리식을 균일하게 대입하여 얻는 논리식이다. 곧 같은 메타변항의 모든 출현에는 같은 논리식이 대입되지만, 서로 다른 메타변항이 같은 논리식을 받아도 되고 서로 다른 논리식을 받아도 된다.

예시도식의 대입례

φ:=v1\varphi := v_{1}, ψ:=¬v2\psi := \neg v_{2}로 두면 도식 (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi))는 대입례 (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1}))을 준다. φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}), ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2})로 두면 ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2})))를 준다. 두 메타변항이 같은 논리식을 받는 것을 막는 것은 아무것도 없기 때문이다. 이와 달리 (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3}))은 이 도식의 대입례가 아니다. φ\varphi의 첫 번째 출현과 마지막 출현이 서로 다른 논리식을 받게 되어 대입이 균일하지 않기 때문이다. 각 대입례는 약어를 펼치면 원과 원판으로 된 기호열이다. 반면에 도식은 메타언어 안에만 존재한다.