본문 바로가기
Topos Uranos
한국어

연결사의 대칭성

요약

이 수업은 인자의 순서가 부정논리합, 선언, 연언, 쌍조건, 배타적 선언에서 연역되는 것을 바꾸지 않음을 증명한다. 이 강좌의 공식 약어 아래에서는 이 대칭성들이 자명하지 않다. 부정논리합은 기본 연결사이고, 우카시에비치의 공리는 부정과 함의에 대해서만 말하며, 이중 부정 대체 규칙(RDN)은 이중 부정을 붙이거나 뗄 뿐이기 때문이다. 그래서 이 수업은 먼저 세 가지 도구를 세운다. 첫째는 증명 가능한 동치가 등식처럼 행동한다는 것이다. 둘째인 기본 보조정리는 부정논리합을 공리의 언어로 옮긴다. RDN 규칙과 이중 부정 덕분에 (φ↓ψ)(\varphi \downarrow \psi)는 ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi)와 동치이다. 셋째인 동치 대체는 RDN 규칙이 있어도 불필요해지지 않으며, 부정 아래에서, 함의의 양쪽에서, 그리고 부정논리합의 양쪽에서 논리식을 그것과 동치인 임의의 논리식으로 바꾸게 해 준다(θ\theta를 ¬¬θ\neg\neg\theta로 바꾸는 것만이 아니다). 이 도구들로 선언과 연언의 동치 형식(다른 책들은 이것을 정의로 삼는다)을 동치로 증명하고, 다섯 대칭성을 양방향으로, 정의가 정하는 순서에 따라 증명한다. 먼저 부정논리합을, 그리고 그로부터 차례로 나머지를 증명한다.

학습 목표

  1. 공식 약어를 펼쳐서, 두 표현이 같은 논리식을 가리키는지, 아니면 동치임을 보이는 데 연역이 필요한 서로 다른 논리식을 가리키는지 판정한다.
  2. 이중 부정 대체 규칙(RDN)과 이중 부정으로 기본 보조정리 (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)를 증명하고, 약어가 숨기고 있는 이중 부정의 위치를 찾아낸다.
  3. 동치 대체를 적용하여 동치를 부정, 함의, 부정논리합의 내부로 옮기고, 그것을 θ\theta와 ¬¬θ\neg\neg\theta를 맞바꿀 뿐인 RDN 규칙과 구별하며, 동치의 사슬에서 증명 가능한 동치를 등식처럼 사용한다.
  4. 이미 증명한 결과들을 이어 붙여, 선언과 연언의 동치 형식과 다섯 대칭성을 양방향으로 증명한다.
  5. 논리식의 복잡도에 관한 귀납법으로 동치 대체를 임의의 논리식으로 확장한다.

사용하는 것과 증명해야 하는 것

형식 연역 체계에 관한 수업은 우카시에비치 체계를 정했다. 곧 공리 A1, A2, A3과 전건 긍정식이다. 그 수업은 또한 반사성(Refl: φ∈Γ\varphi \in \Gamma이면 Γ⊢φ\Gamma \vdash \varphi), 단조성(Mon), 절단(Cut: Γ⊢φi\Gamma \vdash \varphi_{i}가 각 ii에 대해 성립하고 Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi이면 Γ⊢ψ\Gamma \vdash \psi), 연역 정리(DT)와 그 역(CDT), 그리고 증명 가능한 동치 φ⊣⊢ψ\varphi \dashv\vdash \psi를 세웠다. 이것은 {φ}⊢ψ\{\varphi\} \vdash \psi이고 {ψ}⊢φ\{\psi\} \vdash \varphi라는 뜻이다. 또한 공리와 전건 긍정식이 보존하는 표지를 써서, 그 체계가 부정논리합에 관한 어떤 논리식들을 연역하지 못함을 보였다. 네 가지 연역 기법에 관한 수업은 가언 삼단논법(HS: {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)), 전제 교환(IP), 이중 부정(DN: φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, 그 두 정리 ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi)와 ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)를 포함한다), 그리고 세 형태의 대우(CP)를 더했다.

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

이중 부정을 증명한 뒤, 같은 수업은 둘째 기본 규칙인 이중 부정 대체(RDN)로 이 강좌의 체계를 완성했다. χ′\chi'이 χ\chi에서 부분식 θ\theta의 한 출현을 ¬¬θ\neg\neg\theta로 바꾸거나, 부분식 ¬¬θ\neg\neg\theta의 한 출현을 θ\theta로 바꾸어 얻어지면, χ\chi에서 χ′\chi'을 추론한다. 이렇게 행 ii에서 얻은 행은 RDN(i)(i)로 정당화한다. 그 지점부터 ⊢\vdash는 이 강좌의 체계(A1부터 A3까지, 전건 긍정식, RDN)를 가리키며, 그 체계에서도 Refl, Mon, Cut, DT, CDT는 계속 성립한다. 이 규칙은 기본 언어의 기호열에 작용하므로, 약어가 숨기는 출현에도, 그리고 부정논리합의 두 인자 가운데 어느 쪽에도 미친다. 그 직접적인 귀결로 다음이 있다.

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

그리고 일반적으로, χ⊣⊢χ′\chi \dashv\vdash \chi'은 χ′\chi'이 χ\chi에서 RDN으로 얻어질 때마다 성립한다. 이런 꼴의 동치 행은 행 번호 없이 “RDN”으로 정당화하며, 이는 “DN”이나 “CP” 행이 이미 증명된 동치를 인용하는 것과 마찬가지이다. 거기에서처럼, 이미 증명한 정리는 연역의 한 행으로 써도 된다. 그 정리 자신의 연역을 그 자리에 끼워 넣을 수 있기 때문이다. 또한 그 수업의 “결과에서 규칙으로” 보조정리에 의해, 각 기법은 임의의 전제 집합 Γ\Gamma 아래에서 규칙으로도 적용되며, CP(i)(i)나 HS(i,j)(i, j)처럼 적용되는 행의 번호와 함께 인용한다. 연역에 관한 연역에서 “전제”는 증명하고 있는 규칙의 가정 하나를 가리킨다.

명제 논리의 언어에 관한 수업에서 정한 공식 약어가 연결사의 유일한 정의이다.

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

“Def”로 정당화한 행은 아무것도 연역하지 않는다. 같은 논리식을 다른 이름으로 쓸 뿐이며, 주석은 어떤 약어를 펼치거나 접는지를 말한다(“Def →\rightarrow”, “Def ∨\vee”). 자연어의 형식화에 관한 수업에서 본 현상을 떠올려 두는 것이 좋다. 같은 논리식이 여러 이름을 가질 수 있으므로, 연언은 기호열로서는 선언이기도 하다. 예를 들어 ¬φ\neg\varphi를 φ\varphi 대신 넣어 함의를 펼치면 다음을 얻는다.

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

그리고 φ\varphi 앞에 나타나 약어에 가려진 이중 부정이, RDN 규칙이 앞으로의 모든 내용에 관여하게 되는 이유이다.

등식으로서의 증명 가능한 동치

이 수업의 증명은 거의 모두 동치의 사슬이다. φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}, φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3}, 이런 식으로 이어진다. 사슬에서 φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n}을 결론지으려면 증명 가능한 동치가 등식처럼 행동해야 하며, 바로 그것을 세운 것이 형식 연역 체계에 관한 수업의 증명 가능한 동치의 성질에 관한 명제이다. 이 관계는 반사적(φ⊣⊢φ\varphi \dashv\vdash \varphi)이고, 대칭적(φ⊣⊢ψ\varphi \dashv\vdash \psi이면 ψ⊣⊢φ\psi \dashv\vdash \varphi)이며, 추이적(φ⊣⊢ψ\varphi \dashv\vdash \psi이고 ψ⊣⊢χ\psi \dashv\vdash \chi이면 φ⊣⊢χ\varphi \dashv\vdash \chi)이고, 증명 가능하게 동치인 두 논리식은 결론으로서 서로 바꿀 수 있다(Γ⊢φ\Gamma \vdash \varphi이고 φ⊣⊢φ′\varphi \dashv\vdash \varphi'이면 Γ⊢φ′\Gamma \vdash \varphi'이며, 이는 논리식의 모든 집합 Γ\Gamma에 대해 성립한다). 마지막 두 성질을 어떻게 증명했는지 떠올려 두는 것이 좋다. 수업 전체가 그것에 기대고 있기 때문이다. {φ}⊢φ′\{\varphi\} \vdash \varphi'에서 단조성으로 Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi'으로 넘어가고, 이것과 Γ⊢φ\Gamma \vdash \varphi에서 절단으로 Γ⊢φ′\Gamma \vdash \varphi'에 이른다. 추이성은 한쪽 방향에서는 Γ={φ}\Gamma = \{\varphi\}로, 다른 쪽 방향에서는 Γ={χ}\Gamma = \{\chi\}로 놓고 이것을 적용하면 얻어진다.

앞으로 동치의 사슬을 하나의 동치로 모으는 걸음은 “Cut”으로 정당화하며, 그것이 그 명제의 도구이다. 그런데 각 고리 φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1}은 가는 연역과 돌아오는 연역 두 가지를 모두 담고 있다. 따라서 동치의 사슬은 그 결론의 두 방향을 한꺼번에 증명하며, “연습으로” 남는 것은 아무것도 없다.