이 수업은 수학 전체가 사용하는 두 동치의 묶음으로 연역 단원을 마무리한다. 하나는 부정이 연언이나 선언을 어떻게 통과하는지 말해 주는 드모르간 법칙이고, 다른 하나는 연언이 선언에 대해, 그리고 선언이 연언에 대해 어떻게 분배되는지 말해 주는 분배 법칙이다. 이 법칙들을 증명하기 전에, 그것들이 의존하는 구별 하나를 밝혀 둔다. 같은 기호열을 가리키는 두 식은 같은 논리식이므로 그대로 서로 바꿔 놓을 수 있다. 반면 단지 동치일 뿐인 두 논리식은 다른 논리식 안에서 동치 대체에 의해서만, 층마다 바꿔 놓을 수 있다. 이 주의를 바탕으로 두 드모르간 법칙과 그 변형들(그중에는 함의의 부정이 있다), 그리고 두 분배 법칙을 각각 두 방향으로 연역에 의해 증명한다. 문제들은 이것들을 이용해 멱등 법칙, 흡수 법칙, 결합 법칙, 간단한 표준형, 그리고 드모르간 법칙과 대우를 결합한 연역을 얻는다.
학습 목표
기호열의 항등식, 곧 약어를 어디서든 그 펼침으로 바꾸게 해 주는 것과, 증명 가능한 동치, 곧 동치 대체를 통해서만 논리식 안에서의 바꿈을 허용하는 것을 구별하고, 연역에서 동치를 사슬로 잇는다.
두 드모르간 법칙과 그 변형들을 함의의 부정까지 포함하여 연역으로 증명하고, 그 안에서 이중 부정 대체 규칙이 하는 역할을 알아본다.
선언에 대한 연언의 분배 법칙과 연언에 대한 선언의 분배 법칙을 두 방향으로 증명하고, 각 경우에 알맞은 경우에 따른 증명을 고른다.
한 걸음씩 정당화한 동치의 사슬로 논리식을 간단한 표준형으로 변형하고, 멱등 법칙, 흡수 법칙, 결합 법칙을 연역으로 얻는다.
드모르간 법칙을 대우, 그리고 연결사의 도입 규칙 및 제거 규칙과 결합하는, 전제가 있는 연역을 구성한다.
이 단원의 앞선 수업들은 하나 위에 다른 하나를 쌓아 연역의 도구를 세웠다. 공리 체계와 전건 긍정식, 네 가지 기본 기법과 이중 부정 대체, 연결사의 대칭성과 고전 논리의 기법이다. 이 수업은 새 규칙을 하나도 더하지 않고, 그것들을 함께 일하게 한다. 그렇다면 이 수업의 흥미는 다른 강좌에서 이미 알고 있을지도 모르는 진술 자체보다 그것을 얻는 방식에 있다. 각 행은 공리, 전제, 정의, 두 기본 규칙 중 하나, 또는 이미 증명된 결과로 정당화되어야 하며, 어떤 행도 “자명해 보이는” 것에 기대서는 안 된다.
사용하는 것과 그 연결 방식
형식 연역 체계 수업에서는 우카시에비치의 공리 A1, A2, A3, 전건 긍정식(MP)과 그 전제가 있는 형태, 반사성(Refl: φ∈Γ이면 Γ⊢φ), 단조성(Mon), 절단(Cut: Γ⊢φi가 각 i에 대해 성립하고 Γ∪{φ1,…,φn}⊢ψ이면 Γ⊢ψ), 연역 정리(DT), 그리고 증명 가능한 동치(φ⊣⊢ψ는 {φ}⊢ψ이고 {ψ}⊢φ라는 뜻이다)와 그 성질을 가져온다. 증명 가능한 동치는 반사적이고 대칭적이며 추이적이고, φ⊣⊢ψ이면 Γ⊢φ일 때 그리고 그때에만 Γ⊢ψ이다. 네 가지 연역 기법 수업에서는 이중 부정(DN: φ⊣⊢¬¬φ), 대우(CP), 특히 (φ→ψ)⊣⊢(¬ψ→¬φ), 그리고 이 강좌 체계의 두 번째 기본 규칙인 이중 부정 대체(RDN)를 가져오며, 이 규칙이 있어도 연역 정리는 계속 성립한다. χ′이 χ에서 부분식 θ의 한 출현을 ¬¬θ로, 또는 ¬¬θ의 한 출현을 θ로 바꾸어 얻어진다면, χ에서 χ′이 추론된다. 이렇게 행 i에서 얻은 행은 RDN(i)로 정당화한다. 그 직접적인 귀결로는 (φ↓ψ)⊣⊢(¬¬φ↓ψ), (φ↓ψ)⊣⊢(φ↓¬¬ψ), 그리고 일반적으로 χ⊣⊢χ′(χ′이 χ에서 RDN으로 얻어질 때)이 있다. 따라서 RDN(i)는 χ⊣⊢φ 형태의 행에도 적용되어 φ 안의 이중 부정을 바꾸는 데 쓰인다. 연결사의 대칭성 수업에서는 동치 대체(Repl)와 대칭성(Sym)을 가져오며, 그중에는 (φ∨ψ)⊣⊢(ψ∨φ)와 (φ∧ψ)⊣⊢(ψ∧φ)가 있다.
고전 논리의 기법 수업에서는 다음 규칙들을 가져오는데, 모두 전제 집합 Γ와 함께 쓰인다. 선언 도입(∨I): Γ⊢φ이면 Γ⊢(φ∨ψ)이고 Γ⊢(ψ∨φ)이다. 선언 제거(∨E, 선언 삼단논법): Γ⊢(φ∨ψ)이고 Γ⊢¬φ이면 Γ⊢ψ이다. 연언 도입(∧I): Γ⊢φ이고 Γ⊢ψ이면 Γ⊢(φ∧ψ)이다. 연언 제거(∧E): Γ⊢(φ∧ψ)이면 Γ⊢φ이고 Γ⊢ψ이다. 배중률(EM): ⊢(φ∨¬φ). 그리고 경우에 따른 증명(경우)의 두 형태: Γ∪{φ}⊢χ이고 Γ∪{¬φ}⊢χ이면 Γ⊢χ이며, Γ∪{φ}⊢χ, Γ∪{ψ}⊢χ이고 Γ⊢(φ∨ψ)이면 Γ⊢χ이다. 연역에서 첫째 형태는 두 행을 들어 경우(i,j)로, 둘째 형태는 세 행을 들어 경우(i,j,k)로 인용하며, 순서는 진술의 순서, 곧 두 경우와 마지막에 선언이다. 그 수업은 또한 이미 증명된 모든 규칙이 문맥 Γ 안에서 성립한다는 것을 일깨워 주며, 여기서도 이중 부정과 대우를 그렇게 쓴다.
기호열의 이름과 동치인 논리식
명제 논리의 언어 수업에서 보았듯이, ↓ 이외의 연결사는 공식적이고 유일한 정의를 가진 약어이다: ¬φ:=(φ↓φ), (φ∨ψ):=¬(φ↓ψ), (φ∧ψ):=¬(¬φ∨¬ψ), (φ→ψ):=(¬φ∨ψ), (φ↔ψ):=((φ→ψ)∧(ψ→φ)), (φ⊻ψ):=¬(φ↔ψ). 정의는 논리식에 대해 아무것도 주장하지 않는다. 이미 있던 기호열에 둘째 이름을 줄 뿐이다. 따라서 두 식이 같은 기호열을 가리키면, 더 큰 논리식의 안에서도, 어디서든 하나를 다른 하나 대신 놓을 수 있다. 쓰이는 것은 같은 원과 원판의 나열이기 때문이다. 그래서 ¬(φ∧ψ)와 ¬¬(¬φ∨¬ψ)는 같은 기호열이다. 뒤의 것은 앞의 것 안에 연언의 펼침을 써 넣으면 얻어진다. 연역에서는 이 이름 바꿈을 “Def”로 정당화하고, 그 뒤에 펼치거나 접는 연결사를 붙인다.
그런데 증명 가능한 동치는 항등식이 아니다. φ⊣⊢¬¬φ라는 것은 각각에서 다른 하나가 연역된다는 뜻이지, 같은 기호열이라는 뜻이 아니다. ¬¬φ는 φ보다 훨씬 길다. 따라서 φ⊣⊢φ′임을 아는 것만으로는 더 큰 논리식 안에서 φ′을 φ 대신 쓰는 것이 허용되지 않는다. “양변을 부정하는” 것도 허용되지 않는다. φ⊣⊢φ′으로부터 ¬φ⊣⊢¬φ′이 따른다는 것은 하나의 정리, 곧 동치 대체이며, 그 증명은 대우를 사용한다. 자명한 조작이 아니다. 체계가 논리식의 어느 곳에서든 대체를 직접 허용하는 경우는 단 하나뿐이다. θ를 ¬¬θ로 바꾸거나 그 반대로 바꾸는 경우이며, 이것이 RDN 규칙이다. 그리고 연역 체계 수업은 표지를 이용해, 이 경우조차 공리와 전건 긍정식으로부터 연역되지 않음을 보였으므로, 이것을 공준으로 세워야 했다. 이런 주의는 현학이 아니다. 바로 이것이 증명을 기호 조작과 구별해 주며, 기호 조작은 다른 연결사에, 또는 다른 체계에서 적용되면 거짓에 이를 수 있다.
두 결과가 무엇이 허용되는지를 정확히 정한다. 첫째는 형식 연역 체계 수업의, 증명 가능한 동치의 성질에 관한 명제이다. Γ⊢φ이고 φ⊣⊢φ′이면 Γ⊢φ′이므로, 증명 가능한 동치는 한 행의 논리식 전체에 적용할 수 있다. 또한 증명 가능한 동치는 반사적이고 대칭적이며 추이적이므로, 동치들은 사슬로 이어지고(χ⊣⊢φ이고 φ⊣⊢φ′이면 χ⊣⊢φ′), 같은 기호열을 가리키는 두 식은 반사성에 의해 증명 가능하게 동치이다. 둘째는 다음 보조정리로, 인용하기 편하도록 동치 대체를 선언과 연언으로 확장한 것을 모아 놓은 것이다. 대칭성 수업은 이 대체를 부정, 함의, 부정논리합에 대해 증명하고, 예제 하나에서 이 두 연결사로 확장한다.
보조정리선언과 연언에서의 대체
φ⊣⊢φ′이면, 모든 논리식 ψ에 대해 (φ∨ψ)⊣⊢(φ′∨ψ), (ψ∨φ)⊣⊢(ψ∨φ′), (φ∧ψ)⊣⊢(φ′∧ψ), 그리고 (ψ∧φ)⊣⊢(ψ∧φ′)이다.
증명
1
(φ∨ψ)=¬(φ↓ψ)
선언은 정의에 의해 부정논리합의 부정이다.
2
(φ↓ψ)⊣⊢(φ′↓ψ)
부정논리합에 대한 동치 대체가 안쪽 층의 동치를 준다.
3
(φ∨ψ)⊣⊢(φ′∨ψ)
부정에 대한 동치 대체가 그것을 바깥쪽 층 ¬(φ↓ψ)⊣⊢¬(φ′↓ψ)로 옮기며, 이것이 선언이다. 같은 방식으로 (ψ↓φ)⊣⊢(ψ↓φ′)으로 오른쪽의 대체를 얻는다.
4
(φ∧ψ)=¬(¬φ∨¬ψ),¬φ⊣⊢¬φ′
연언은 부정들의 선언의 부정이다. 부정에 대한 대체가 먼저 ¬φ⊣⊢¬φ′을 준다.
5
¬(¬φ∨¬ψ)⊣⊢¬(¬φ′∨¬ψ),(φ∧ψ)⊣⊢(φ′∧ψ)
선언에 대해 이미 증명한 부분을 ¬φ와 ¬φ′에 적용하면 (¬φ∨¬ψ)⊣⊢(¬φ′∨¬ψ)를 얻고, 다시 부정에 대한 대체가 동치를 연언으로 옮긴다. 오른쪽도 같은 방식으로 추론한다.
앞으로 “Repl”은 동치 대체를, 이 보조정리의 형태까지 포함하여 그 어떤 형태로든 가리키며, 층마다 여러 번 잇따라 적용하여 어떤 깊이에 있는 부분식에도 이를 수 있다. 한 행이 행 i에서 이미 증명된 동치를 논리식 전체에, 또는 Repl로 그 부분 중 하나에 적용하여 얻어질 때, 그 행은 그 동치의 이름과 행 번호로 정당화한다: DN(i), “Repl, DM(i)”. 이름 바꿈은 어떤 동치도 적용하지 않고 같은 기호열을 다시 쓸 뿐이며, 같은 방식으로 “Def”로 정당화하고, 그 뒤에 펼치거나 접는 연결사를 붙인다: Def ∧(i). 형식 연역 체계 수업의 명제는, 행 i가 Γ⊢φ를 주장하든 점점 이어지는 동치 χ⊣⊢φ를 주장하든, 그런 행이 정당화되어 있음을 보장한다.