일계논리의 형식계는 명제논리와 마찬가지로 알파벳, 공리, 추론규칙으로 구성된다. 그러나 일계논리의 공리와 추론규칙은 명제논리보다 더 복잡하다.
일계논리의 공리와 추론규칙
일계논리에서는 결합자와 한정기호를 다음 세 개의 기호로 표현할 수 있다. \[\lnot, \,\,\, \rightarrow, \,\,\, \forall\]
일계논리의 공리는 다음과 같은 아홉 개의 공리틀로 이루어져 있다.
- (A1) \((\phi\rightarrow (\psi \rightarrow \phi))\)
- (A2) \(((\phi\rightarrow (\psi \rightarrow \theta)) \rightarrow ((\phi \rightarrow \psi)\rightarrow (\phi \rightarrow \theta)))\)
- (A3) \((((\lnot \phi) \rightarrow (\lnot \phi)) \rightarrow (\psi \rightarrow \phi))\)
- (A4) \(((\forall x)\phi \rightarrow \phi[t/x])\)
- (A5) \(x\)가 \(\phi\)에서 자유변수가 아닐 때 \(((\forall x)(\phi \rightarrow \psi)\rightarrow (\phi \rightarrow (\forall x)\psi))\)
- (E1) \(t\)가 항일 때 \((t=t)\)
- (E2) \(t,\) \(u\)가 항일 때 \(((t=u) \rightarrow (u=t))\)
- (E3) \(t,\) \(u,\) \(v\)가 항일 때 \(((t=u) \rightarrow ((u=v) \rightarrow (t=v)))\)
- (E4) \(((t=u) \rightarrow (\phi[t/x,\,t/y]\rightarrow \phi[t/x,\,u/y]))\)
위 공리에서 \(\phi[t/x]\)는 논리식 \(\phi\)에 나타나는 자유변수 \(x\)를 \(t\)로 치환하는 것을 의미한다.
첫 세 공리(A1-A3)는 명제논리의 공리와 동일하다. A4와 A5는 한정기호를 다루기 위한 것이며, E1-E4는 등호의 성질을 정의한다.
일계논리의 추론규칙은 다음 두 가지가 있다.
- (R1) Modus Ponens: \(\phi\)와 \(\phi \rightarrow \psi\)로부터 \(\psi\)를 추론한다.
- (R2) 일반화: \(x\)가 변수일 때, \(\phi\)로부터 \((\forall x)\phi\)를 추론한다.
일계논리의 건전성과 완전성
일계논리의 공리와 추론규칙을 바탕으로 일계논리에서 중요한 두 정리를 소개한다.
정리 16.1. (건전성 정리)
논리식 \(\phi\)가 정리이면 \(\phi\)는 논리적으로 유효하다. 더 일반적으로, \(\varSigma\)가 논리식의 집합이고 \(\phi\)가 논리식일 때, \(\phi\)가 \(\varSigma\)로부터 추론될 수 있으면 \(\phi\)는 \(\varSigma\)의 논리적 귀결이다.
증명 개요 건전성 정리는 공리가 모두 논리적으로 유효하고, 추론규칙이 논리적 유효성을 보존한다는 사실에 기초한다. 증명은 \(\varSigma\)로부터의 \(\phi\)의 증명 길이에 대한 수학적 귀납법을 사용한다.
기본 단계: \(\phi\)가 공리이거나 \(\varSigma\)에 속하는 경우, \(\phi\)의 논리적 유효성은 자명하다.
귀납 단계: \(\phi\)가 추론규칙을 통해 얻어진 경우, 귀납적 가정에 의해 추론에 사용된 논리식들이 논리적으로 유효하므로 \(\phi\) 역시 논리적으로 유효하다.
정리 16.2. (완전성 정리)
가산 개의 함수기호, 관계기호, 상수기호를 가진 일계논리언어 \(\mathcal{L}\)에 대해, 논리식 \(\phi\)가 논리적으로 유효하면 \(\phi\)는 정리이다. 더 일반적으로, \(\varSigma\)가 논리식의 집합이고 \(\phi\)가 논리식일 때, \(\phi\)가 \(\varSigma\)의 논리적 귀결이면 \(\phi\)는 \(\varSigma\)로부터 추론될 수 있다.
증명 개요 완전성 정리는 더 강한 결과인 "논리식의 집합 \(\varSigma\)가 무모순일 필요충분조건은 \(\varSigma\)가 모델을 가지는 것이다"를 증명함으로써 얻을 수 있다. 증명은 다음 단계로 진행된다.
- \(\mathcal{L}\)에 새로운 상수들을 추가하여 확장한다.
- \(\varSigma\)가 무모순이면 \(\varSigma\)를 포함하는 완전하고 무모순인 집합 \(\varSigma^+\)가 존재함을 보인다.
- \(\varSigma^+\)를 사용하여 모델을 구성한다.
- 이 모델이 \(\varSigma\)의 모델임을 증명한다.
이러한 방법을 통해 무모순인 논리식 집합이 모델을 가짐을 보이고, 이것을 사용하여 완전성 정리를 증명한다.
이 정리들은 일계논리의 구문론과 의미론 사이의 관계를 설명한다. 즉, 논리적으로 유효한 것과 형식적으로 증명 가능한 것이 일치한다는 것을 보여준다.