린(Lean) 정리 증명기로 안셀무스의 신 존재 증명 형식화하기

P와 동치도, P의 부정도 아닌 Q를 이론 T로부터 증명하는 일은 P가 T의 정리가 아님에 대한 증명이 아닙니다. 따라서, 하셔야 하는 것은 해당 명제가 안셀름의 전제들의 정리가 ‘아님을’ 보이는 일이어야지, 해당 명제를 함축 않는 다른 명제가 정리임을 보이는 일이어서는 안 된다는 말씀인 겁니다. (부기하신 부분은 기호논리학에서 “.”이 하는 역할과 같아 이해하고 있습니다.)

1개의 좋아요