search

snu-sf-class / pl2016

14 stars 17 forks source link

과제 5에 11번 질문드립니다. #63

Closed AlexSeongJu-sr closed 8 years ago

AlexSeongJu-sr commented 8 years ago

Axiom을 써야하는데, axiom을 어떻게 넣는지 모르겠습니다. Definition으로 excluded_middle을 정의하고 apply excluded_middle. 을 사용하면 되는 거 아닌가요?

goal이 P \/ (P -> False) 인 상태에서 apply excluded_middle을 쓰니 Error: Impossible to unify "Prop" with "P \/ (P -> False)". 라고 뜹니다. 뭐가 잘못된 것인지 궁금합니다

jeehoonkang commented 8 years ago

Axiom을 쓰시면 안됩니다. 문제는 공리를 받아드릴 필요 없이 증명할 수 있는 명제입니다.