모든 걸 뚫을 수 있는 창과 모든 걸 막을 수 있는 방패
만약에 그 창과 방패를 결합시켜 "창방패"라는 물건을 새로이 발명한다면, 그 창과 방패를 결합시킨 "창방패"는
동시에 존재할 수 없는 속성,"모든 걸 뚫을 수 있는" 창의 속성과 "모든 걸 막을 수 있는" 방패의 속성을 둘 다 가지고 있기에 모순인 것인가.
아니면,
실제로 모든 걸 뚫을 수 있으면서 막을 수 있기에 모순이 아닌 것인가.
그런 '창방패'가 존재하면 모순을 이끌어 낼 수 있습니다. 아래 린 4 코드의 마지막 정리를 봐 주세요.
/-- A class of objects with two predicates, `IsSpear` and `IsShield`, and a relation, `CanPierce`,
defined as follows:
* `IsSpear x`: `x` is a spear.
* `IsShield x`: `x` is a shield.
* `CanPierce x y`: `x` can pierce `y`. -/
class SpearShield (Object : Type u) where
IsSpear : Object → Prop
IsShield : Object → Prop
CanPierce : Object → Object → Prop
namespace SpearShield
variable {Object : Type u} [SpearShield Object]
/-- For all objects `x` and `y`, `x` blocks `y` if and only if `y` cannot pierce `x`. -/
def Block (x y : Object) : Prop := ¬CanPierce y x
-- Assign infix notations to the predicates `CanPierce` and `Block`.
infix:55 " can pierce " => CanPierce
infix:55 " blocks " => Block
/-- No object is both a spear and a shield capable of both piercing and blocking any object. -/
theorem not_exists_isSpear_and_isShield_and_canPierce_and_block : ¬∃ (x : Object), IsSpear x ∧
IsShield x ∧ (∀ (y : Object), x can pierce y) ∧ ∀ (y : Object), x blocks y := by
intro h
let ⟨x, _, _, hpx, hbx⟩ := h
have hxpx : x can pierce x := hpx x
have hxbx : x blocks x := hbx x
exact hxbx hxpx
end SpearShield
더 많은 분이 린이나 다른 증명 보조기를 다루실 수 있다면, 그분들은 자신의 논증을 직접 형식화하고 검토하실 수 있을 것입니다. 이는 모두에게 이롭다고 생각해요.
2개의 좋아요
‘모든 걸 뚫는’이라는 표현이 사실은 애매합니다. 이것이 무제약적 의미에서 모든 것을 의미한다면, 사실은 모든 걸 뚫는 창 같은 것은 존재할 수 없습니다. 어떤 창도 자기 스스로를 뚫을 수는 없으니까요. 따라서 창의 판매자는 다음과 같이 ‘모든 걸 뚫는 창이다’가 정의되어야 한다고 호소할 수 있습니다 (F: 창이다; Pxy: x가 y를 뚫는다):
(Fx∧∀y(x≠y⊃Pxy))
한편 ‘모든 걸 막는 방패이다’는 다음처럼 정의되는 것이 자연스럽습니다 (G: 방패이다):
(Gx∧¬∃y(Pyx))
그렇다면 ‘자비롭게 해석된 창방패가 존재한다’는 다음의 식이 됩니다:
∃x(Fx∧Gx∧∀y(x≠y⊃Pxy)∧¬∃y(Pyx))
요것이 논리적 모순이기 위해 필요한 건 ‘∀y(x≠y⊃Pxy)∧¬∃y(Pyx)’의 모순입니다. 하지만 그렇지 않은데요, 가령 다음의 논리적 모형이 존재합니다:
F={a}
G={a}
Pxy=∅
다만, 흥미롭게도 그와 같은 창방패는 둘 이상 존재할 수 없습니다. 이 경우 어떤 a, b에 대해
- ∀y(a≠y⊃Pay)∧¬∃y(Pya)
이고 - ∀y(b≠y⊃Pby)∧¬∃y(Pyb)
인데, 우리는 이로부터 빠르게 모순을 이끌어낼 수 있습니다.
- Pab (1, ∧제거, ∀예화, 동일성, MP)
- ¬Pab (2, ∧제거, ∀-∃ 쌍대성, ∀예화)
4개의 좋아요
다른 모든 것을 뚫을 수 있고, 다른 모든 것을 막을 수 있는 창방패가 존재하는 모형이 있다는 말씀이죠? 이런 해석이 더 자비롭다는 데 저도 동의합니다. 시간이 나면 @car_nap 님의 형식화도 린으로 재서술해 볼게요.
그건 그렇고, 제가 린으로 프로그래밍을 할 수 있게 되면, 린으로 작성한 증명을 피치 형식(Fitch-style)으로 내보내는 프로그램을 작성하고 싶네요. 이러면 다른 분들이 린 증명을 이해하기가 '그나마' 더 수월해질 테니까요.