린 커뮤니티에도 이미 메시지를 올렸는데, 두 분만 제 형식화를 논평해 주셨습니다. 한 분의 논평은 유형 클래스를 잘 정의하는 방법에 관한 것이고, 다른 한 분의 논평은 앨빈 플랜팅아(Alvin Plantinga)가 정식화한 안셀무스의 존재론적 논증의 3단계에 관한 것입니다.
그런데 제가 Lean은 물론이거니와, 안셀무스식 신 존재 논증 역시 깊이 공부해질 못해서 조심스럽습니다만, 안셀무스의 영향을 받은 양상적 존재론적 논증(들)에 대한 Lean 형식화부터 시도해보는 것도 유용하지 않을까 싶습니다. 안셀무스식 논증의 '최신판'이기도 하거니와, 일단 양상논리로 형식화가 이루어졌다는 점에서 정밀하게 옮기는데 더 용이할테니까요.
어쨌든 증명보조기를 철학적 논증에 (필요한 상황에서라면) 도입하는 것도 유용한 도구가 될 수 있을 것 같네요!
P와 동치도, P의 부정도 아닌 Q를 이론 T로부터 증명하는 일은 P가 T의 정리가 아님에 대한 증명이 아닙니다. 따라서, 하셔야 하는 것은 해당 명제가 안셀름의 전제들의 정리가 ‘아님을’ 보이는 일이어야지, 해당 명제를 함축 않는 다른 명제가 정리임을 보이는 일이어서는 안 된다는 말씀인 겁니다. (부기하신 부분은 기호논리학에서 “.”이 하는 역할과 같아 이해하고 있습니다.)
In your case you just need to demonstrate that for some instantiation of your class the proposition is false. E.g. for Anselm Nat with Conceivable := fun _ => True there is provably no x such that IsMax x Conceivable.
안셀무스의 논증에 있는 전제에서 ∃ (x : Being), isGod x이라는 결론을 도출할 수 없음을 밝히려면, ∃ (x : Being), isGod x라는 진술이 거짓인 유형 세계 단계 u, 유형 Being : Type u 그리고 Anselm Being의 사례[인스턴스]를 들기만 해도 됩니다. 새로 추가한 정리는 다음과 같습니다.
local instance : Anselm ℤ where
conceivable := fun _ ↦ True
inUnderstanding := fun _ ↦ True
inReality := fun
| .ofNat _ => True
| .negSucc _ => False
lt_of_inUnderstanding_not_inReality_inReality {_ _ : ℤ} := by
repeat (first | simp | split <;> simp [not_true, not_false])
rename_i n _ m
calc
-(n + 1) < (0 : ℤ) := Int.negSucc_lt_zero n
0 ≤ ↑m := Int.zero_le_ofNat m
isMax_conceivable_inUnderstanding := by simp
exists_conceivable_and_inReality := by exists 0
private theorem not_exists_int_isGod : ¬ ∃ (a : ℤ), isGod a := by
intro hex
rcases hex with ⟨god, _hcg, hleg⟩
have god_lt_succ_god : god < god + 1 := Int.lt_succ god
have succ_god_le_god : god + 1 ≤ god := hleg (god + 1) trivial
exact not_le_of_lt god_lt_succ_god succ_god_le_god