본문 바로가기
Topos Uranos
한국어

고전 논리의 기법

요약

수학에서 추론하는 사람은 연언과 선언을 도입하고 제거하며, 배중률에 호소하고, 모순된 것을 버리고, 경우를 나누고, 귀류법을 쓰지만, 거의 언제나 자신이 그렇게 한다는 것을 의식하지 못한다. 이 수업은 그 모든 기법이 이 강좌의 연역 체계의 파생 규칙임을 증명하며, 그것들이 실제로 쓰이는 형태로, 곧 연역 내내 유지되는 전제 집합 Γ\Gamma와 함께 증명한다. 먼저 이미 증명된 모든 규칙이 맥락 Γ\Gamma 안에서 성립함을 상기하고, 이어서 선언과 연언의 도입과 제거, 배중률과 무모순율, 폭발 원리, 두 형태의 귀류법, 그리고 경우에 따른 증명을, 처음에는 논리식과 그 부정으로, 다음에는 임의의 선언으로 증명한다. 문제들은 이 기법들을 퍼스의 법칙이나 양도논법 같은 고전적 법칙에 적용하고, 그것들을 전제 없이 증명하는 것만으로는 왜 충분하지 않은지 보여 준다.

학습 목표

  1. Γ⊢φ\Gamma \vdash \varphi 꼴의 행에 앞서 증명한 규칙과 동치를 적용하고, 그 단계를 단조성과 절단으로 정당화한다.
  2. 선언과 연언의 도입 규칙과 제거 규칙을 전제와 함께 증명하고, 공식 약어는 허용되는 곳에서만 펼친다.
  3. 배중률과 무모순율을 연역하고, 각 단계에서 무엇이 정의이고 무엇이 정리인지 구별한다.
  4. 폭발 원리, 두 형태의 귀류법, 경우에 따른 증명을 전제와 함께 증명하고, 전제 없는 판본으로는 왜 충분하지 않은지 설명한다.
  5. 이 기법들을 결합하여 고전적 법칙(퍼스의 법칙, 이출 법칙, 양도논법)의 연역을 구성하고, 논리식의 연역 가능성을 전제 집합의 모순성과 관련짓는다.

맥락 안의 규칙

형식 연역 체계 수업에서 우카시에비치 체계를 정했다. 곧 공리 도식 A1, A2, A3, 전건 긍정식(MP) 규칙, 그리고 전제 집합 Γ\Gamma로부터의 연역이라는 개념과 그 첫 성질들로, 반사성(Refl: φ∈Γ\varphi \in \Gamma이면 Γ⊢φ\Gamma \vdash \varphi), 단조성(Mon: Γ⊆Δ\Gamma \subseteq \Delta이고 Γ⊢φ\Gamma \vdash \varphi이면 Δ⊢φ\Delta \vdash \varphi), 절단(Cut), 연역 사이의 전건 긍정식(Γ⊢φ\Gamma \vdash \varphi이고 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)이면 Γ⊢ψ\Gamma \vdash \psi이며, 이것도 MP로 인용한다), 연역 정리(DT: Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi이면 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi))와 그 역(CDT)이다. 네 가지 연역 기법 수업과 연결사의 대칭성 수업은 가언 삼단논법(HS), 전제 교환(IP), 이중 부정(DN), 세 형태의 대우(CP), 동치 대체(Repl), 대칭성(Sym), 그리고 선언과 연언의 동치 형식을 덧붙였다. 그중 앞의 수업은 이중 부정을 증명한 뒤 이 강좌의 체계에 둘째 기본 규칙인 이중 부정 대체(RDN)를 더했다. χ′\chi'이 χ\chi에서 부분식 θ\theta의 한 출현을 ¬¬θ\neg\neg\theta로, 또는 ¬¬θ\neg\neg\theta의 한 출현을 θ\theta로 바꾸어 얻어지면, χ\chi에서 χ′\chi'을 추론한다. 이후 ⊢\vdash 기호는 이 체계(A1에서 A3까지, MP, RDN)를 가리키며, 그 안에서는 반사성, 단조성, 절단, 연역 정리와 그 역이 여전히 성립한다. 이 수업의 기법들은 그 체계의 파생 규칙이지만, 그 증명 가운데 어느 것도 RDN을 직접 인용하지 않는다. 이 규칙은 동치 형식과 동치 대체를 통해 작용하며, 대칭성 수업이 그것들을 이 규칙으로 증명했다.

그러나 수학에서는 아무도 전제 없이 추론하지 않는다. 사람들은 몇몇 공리에서, 정리의 가정에서, 그리고 어떤 경우를 따지기 위해 가정한 것에서 출발하여 추론한다. 그렇다면 추론 기법은 행에서 행으로 이어지는 전제 집합 Γ\Gamma와 함께 진술될 때에만 쓸모가 있다. 따라서 이 수업의 각 규칙은 임의의 Γ\Gamma에 대해 진술되고 증명된다. 전제가 없는 경우는 특수한 경우 Γ=∅\Gamma = \emptyset이며, 그 반대가 아니다.

증명은 연역에 관한 연역이다. 각 행은 무언가가 어떤 집합에서 연역 가능하다는 것, 곧 Γ⊢φ\Gamma \vdash \varphi임을 주장하며, 그 근거는 앞선 행들을 가리킨다. 그 안에서 “전제”는 규칙의 진술이 가정하는 행을 나타내고, 공리(A1, A3)나 이미 증명된 정리(예컨대 Id, 곧 정리 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi))의 이름은 Γ⊢φ\Gamma \vdash \varphi 꼴의 행을 나타내며, 거기서 φ\varphi는 그 도식이나 그 정리의 대입례로서 어떤 집합에서든 연역 가능하다.

네 가지 연역 기법 수업은 단조성과 절단으로 “결과에서 규칙으로” 보조정리를 증명했고, 이 보조정리가 이러한 작업 방식을 가능하게 한다. {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta이고, Γ⊢αi\Gamma \vdash \alpha_{i}가 각 ii에 대해 성립하면, Γ⊢β\Gamma \vdash \beta이다. n=1n = 1일 때, 동치 α⊣⊢α′\alpha \dashv\vdash \alpha'의 각 방향에 적용하면, 이 보조정리는 Γ⊢α\Gamma \vdash \alpha일 때 그리고 그때에만 Γ⊢α′\Gamma \vdash \alpha'임을 말한다. 따라서 이미 증명된 모든 규칙과 이미 증명된 모든 동치는 전제가 있는 연역의 행들에 적용된다. 어떤 행이 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)이면, 대우에 의해 그 아래에 Γ⊢(¬ψ→¬φ)\Gamma \vdash (\neg\psi \rightarrow \neg\varphi)의 행을 덧붙이고 “CP”와 행 번호로 정당화할 수 있다. 대칭성 수업의 두 동치 형식은 끊임없이 쓰일 것이므로, “Eq”로 쓴다.

(φ∨ψ)⊣⊢(¬φ→ψ)(φ∧ψ)⊣⊢¬(φ→¬ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) \qquad (\varphi \wedge \psi) \dashv\vdash \neg(\varphi \rightarrow \neg\psi)

이 두 동치 가운데 첫째가 정의가 아니라는 점을 강조해 둔다. 둘째는 대칭성 수업에서 보였듯이 기호열의 항등식이지만, 첫째와 함께 “Eq”로 인용한다. 정의상 (φ∨ψ)(\varphi \vee \psi) 자체는 ¬(φ↓ψ)\neg(\varphi \downarrow \psi)이고 (¬φ→ψ)(\neg\varphi \rightarrow \psi) 자체는 (¬¬φ∨ψ)(\neg\neg\varphi \vee \psi)이며, 이 둘은 서로 다른 기호열이다. 하나를 “함의의 정의에 의해” 다른 하나로 읽는 것이 바로 이 수업이 피하는 오류이다. 반면 “Def”는 같은 기호열을 다른 이름으로 쓰는 데에, 예컨대 (φ→ψ)(\varphi \rightarrow \psi)를 (¬φ∨ψ)(\neg\varphi \vee \psi)로 읽을 때에 쓴다.