본문 바로가기
Topos Uranos
한국어

네 가지 연역 기법

요약

앞 수업의 우카시에비치 체계는 세 공리 도식과 단 하나의 규칙인 전건 긍정식으로 이루어진다. 이렇게 수단이 적으므로 모든 연역은 공리에서부터 세워야 하며, 논리식 (φ→φ)(\varphi \rightarrow \varphi)조차 다섯 행이 필요하다. 이 수업은 한 번만 증명하고 이후 거듭 쓰는 네 가지 기법을 더한다. 함의를 잇는 가언 삼단논법, 전건의 순서를 바꿀 수 있게 하는 전제 교환, 잇달아 놓인 두 부정을 붙이거나 떼게 하는 이중 부정, 그리고 세 가지 형태를 가지며 함의의 두 항을 부정하여 함의를 뒤집게 하는 대우이다. 각 기법은 세 공리, 전건 긍정식, 앞 수업의 메타정리로 한 행씩 완전하게 증명되며, 세 가지 모습으로 얻어진다. 전제로부터의 연역으로, 정리로, 그리고 어떤 전제 집합 아래에서도 적용되는 규칙으로이다. 이중 부정을 증명한 뒤, 이 수업은 둘째 기본 규칙인 이중 부정 대체로 체계를 완성한다. 이 규칙은 논리식의 어느 자리에서나 두 부정을 붙이거나 떼게 하며, 세 공리가 닿지 않는 부정논리합의 내부에서도 그렇게 한다. 또 이 규칙을 왜 공준으로 세워야 하는지 설명하고, 연역의 성질이 보존됨을 확인하며, 연역 정리를 새 경우로 보완하고, 그 첫 귀결들을 얻는다.

학습 목표

  1. {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta 꼴의 결과를 연역 정리로 정리로 바꾸고, 단조성과 절단으로 어떤 전제 집합 Γ\Gamma 아래에서도 적용되는 규칙으로 바꾼다.
  2. 가언 삼단논법과 전제 교환을, A1과 A2에서 출발하는 직접 연역으로도, 연역 정리를 이용한 연역에 관한 추론으로도 증명하고, 이를 써서 함의를 잇고 순서를 바꾼다.
  3. 이중 부정의 두 방향을 A1부터 A3까지와 전건 긍정식으로 증명하고, 이를 적용하여 연역 안에서 잇달아 놓인 두 부정을 붙이거나 뗀다.
  4. 이중 부정 대체 규칙을 진술하고, 기본 언어의 기호열에서 부분식의 출현을, 약어가 감추는 출현까지 포함하여 찾아내며, 이 규칙을 연역에 적용한다.
  5. 이중 부정 대체를 왜 공준으로 세워야 하는지 표지로 설명하고, 연역의 성질과 연역 정리가 확장된 체계에서도 성립함을 증명한다.
  6. 대우를 세 가지 형태로 증명하고, 부정이 들어 있는 함의를 앞에 두고 알맞은 형태를 고른다.
  7. 네 가지 기법과 새 규칙을 공리, 전건 긍정식, 연역 정리와 결합하여 자명하지 않은 연역을 세우고, 각 행을 해당 약어로 정당화한다.

출발점의 도구

형식 연역 체계 수업에서 우카시에비치 체계를 정했다. 그 언어는 원과 원판의 언어이며, 명제 논리의 언어 수업의 공식 약어로 쓴다. 그 공리는 다음 세 도식의 모든 대입례이고(여기서 φ\varphi, ψ\psi, χ\chi는 임의의 논리식이다), 그 유일한 규칙은 전건 긍정식이다.

  • A1: (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)).
  • A2: ((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))).
  • A3: ((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi)).
  • MP: φ\varphi와 (φ→ψ)(\varphi \rightarrow \psi)에서 ψ\psi가 연역된다.

φ\varphi의, 논리식의 집합 Γ\Gamma로부터의 연역이란 φ\varphi로 끝나는 논리식의 유한한 나열로서, 그 각 논리식이 공리이거나, Γ\Gamma의 원소이거나, 앞선 두 논리식에 전건 긍정식을 적용한 결과인 것이다. 그런 나열이 있으면 Γ⊢φ\Gamma \vdash \varphi라고 쓰고, Γ\Gamma가 공집합이면 ⊢φ\vdash \varphi라고 쓰며, φ\varphi는 정리라고 한다. 같은 수업에서 여기서 쓸 메타정리들을 증명했다. 반사성(Refl: φ∈Γ\varphi \in \Gamma이면 Γ⊢φ\Gamma \vdash \varphi), 단조성(Mon: Γ⊆Δ\Gamma \subseteq \Delta이고 Γ⊢φ\Gamma \vdash \varphi이면 Δ⊢φ\Delta \vdash \varphi), 연역 사이의 전건 긍정식(Γ⊢φ\Gamma \vdash \varphi이고 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)이면 Γ⊢ψ\Gamma \vdash \psi), 절단(Cut: Γ⊢φi\Gamma \vdash \varphi_{i}가, ii가 11부터 nn까지의 각 값일 때 성립하고 Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi이면 Γ⊢ψ\Gamma \vdash \psi), 유한성(Γ⊢φ\Gamma \vdash \varphi이면 Γ\Gamma의 어떤 유한 부분집합으로 충분하다), 연역 정리(DT: Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi이면 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi))와 그 역(CDT), 그리고 정리 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)이며, 이 정리는 근거 표기에서 Id로 줄여 쓴다. 끝으로, φ⊣⊢ψ\varphi \dashv\vdash \psi(증명 가능한 동치)는 {φ}⊢ψ\{\varphi\} \vdash \psi이고 {ψ}⊢φ\{\psi\} \vdash \varphi라는 뜻이다.

¬\neg 기호와 →\rightarrow 기호는 기본 언어의 기호가 아니라 약어임을 기억해 두자. ¬φ\neg\varphi는 기호열 (φ↓φ)(\varphi \downarrow \varphi)이고, (φ→ψ)(\varphi \rightarrow \psi)는 (¬φ∨ψ)(\neg\varphi \vee \psi), 곧 ¬(¬φ↓ψ)\neg(\neg\varphi \downarrow \psi)이다. 세 공리는 부정과 함의에 대해서만 말하며, 같은 수업은 공리들과 전건 긍정식이 보존하는, 00과 11의 값을 갖는 표지를 써서 그로부터 나오는 한계를 보였다. 우카시에비치 체계에서는 (v1↓v2)(v_{1} \downarrow v_{2})에서 (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2})가 연역되지 않으며, 부정논리합은 일부가 그 체계의 손이 닿지 않는 곳에 남는다. 그러므로 이 수업은 두 단계로 나아간다. 이중 부정까지는(이중 부정을 포함하여) ⊢\vdash 기호는 우카시에비치 체계를 가리키며, 증명되는 어떤 것도 약어를 펼치는 데 의존하지 않는다. 이중 부정을 증명한 뒤, 체계에 둘째 기본 규칙인 이중 부정 대체를 더하는데, 이 규칙은 펼친 기호열에 작용한다. 그때부터 ⊢\vdash 기호는 이 강좌의 체계, 곧 우카시에비치 체계에 이 규칙을 더한 것을 가리킨다. 앞 체계의 모든 연역은 뒤 체계의 연역이기도 하므로, 그 전에 증명한 것은 아무것도 잃지 않는다.

연역의 두 방식

연역을 쓰는 방식은 둘이며, 둘 다 쓴다. 첫째는 본래 의미의 연역, 곧 논리식의 나열로서 각 행이 공리, 전제 또는 전건 긍정식의 결과인 것이다. 각 행은 A1, A2, A3, 전제 또는 MP(i,j)(i, j)로 정당화하는데, 여기서 행 ii는 전건이고 행 jj는 그 전건이 정확히 행 ii인 함의이다(새 규칙을 도입한 뒤에는 RDN(i)(i)도 있다). 둘째는 연역에 관한 연역으로, 그 행은 논리식이 아니라 Γ⊢φ\Gamma \vdash \varphi 꼴의 주장이다. 각 행은 이미 증명된 메타정리로 정당화되며, 나열 전체는 첫째 방식의 연역이 존재함을, 그것을 써 내지 않고도 보장하는 메타언어의 추론이다. 이 둘째 방식의 근거는 다음과 같이 읽는다.

  • Refl: 오른쪽 논리식이 왼쪽 집합에 속한다.
  • A1, A2, A3: 오른쪽 논리식이 그 도식의 대입례이다. 공리의 대입례는 어떤 Γ\Gamma에서든 한 행짜리 연역으로 연역된다.
  • MP(i,j)(i, j): 연역 사이의 전건 긍정식을 행 ii의 Γ⊢φ\Gamma \vdash \varphi와 행 jj의 Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)에, 같은 Γ\Gamma로 적용한 것.
  • DT(i)(i)와 CDT(i)(i): 행 ii에 적용한 연역 정리 또는 그 역.
  • 이미 증명된 정리의 이름, 예컨대 Id나 DN: 오른쪽 논리식이 그 정리의 대입례이며, 어떤 Γ\Gamma에서든 단조성에 의해 연역된다. 공집합은 Γ\Gamma에 포함되기 때문이다.
  • 전제(연역에 관한 연역에서): 그 행은 증명하고 있는 규칙의 가정 가운데 하나이다.

이 수업의 모든 결과는 메타변항으로 진술되므로 임의의 논리식에 대해 성립한다. 그 증명은 하나의 도식이며, 그 안의 각 메타변항에 논리식을 대입하면 또 하나의 증명이 얻어진다. 공리 도식의 대입례는 여전히 대입례이고, 전건 긍정식의 각 적용도 여전히 그 적용이기 때문이다(새 규칙의 각 적용도 마찬가지이다). 이렇게 ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)에서 ⊢(¬ψ→¬ψ)\vdash (\neg\psi \rightarrow \neg\psi)가 나온다. ¬ψ\neg\psi를 φ\varphi 대신 쓴 것이다. 결과를 진술에 있는 것보다 복잡한 논리식에 적용하는 이 수단이 앞으로 가장 쓸모가 많다.

결과에서 규칙으로

이 수업의 기법들은 {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)처럼 고정된 전제에서 증명된다. 그러나 쓰이는 곳은 다른 전제를 가진 연역의 한가운데이며, 거기서 (φ→ψ)(\varphi \rightarrow \psi)와 (ψ→χ)(\psi \rightarrow \chi)는 전제가 아니라 이미 연역된 논리식이다. 단조성과 절단에서 곧바로 나오는 다음 보조정리가 그런 쓰임을 한 번에 영구히 허락한다.

보조정리결과에서 규칙으로

{α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta이면, 논리식의 모든 집합 Γ\Gamma에 대해 Γ⊢α1\Gamma \vdash \alpha_{1}, …\ldots, Γ⊢αn\Gamma \vdash \alpha_{n}에서 Γ⊢β\Gamma \vdash \beta가 나온다. 또한 ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))이다.

증명

  1. Γ∪{α1,…,αn}⊢β\dato{mon}{\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta}

    가정에 의해 β\beta는 논리식 αi\alpha_{i}들에서 연역된다. {α1,…,αn}\{\alpha_{1}, \ldots, \alpha_{n}\}은 Γ∪{α1,…,αn}\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\}에 포함되므로, 단조성에 의해 전제에 Γ\Gamma를 더할 수 있다.

  2. Γ⊢β\Gamma \vdash \resaltar{\beta}

    또한 각 αi\alpha_{i}가 Γ\Gamma에서 연역되면, 절단이 더한 전제들을 없앤다.

  3. ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))

    정리의 형태를 위해서는 연역 정리를 nn번 적용하여 전제를 마지막 것부터 첫 것까지 해소한다. 각 적용은 해소된 전제를 함의의 전건으로 바꾼다.

그러므로 전제에서 증명된 기법은 모두 세 가지 모습을 가진다. 결과 자체, 그 전제를 해소하여 얻는 정리, 그리고 어떤 Γ\Gamma 아래에서도 적용되는 규칙이다. 연역에 관한 연역에서 규칙은 기법의 이름과 그것을 적용하는 행의 번호로, HS(3,4)(3, 4)처럼 불러내며, 보조정리가 그 걸음이 정당함을 보장한다.