The Coq Proof Assistant로 건전성이랑 약완전성은 보였는데요,
http://www.anupamdas.com/wp/wp-content/uploads/2018/08/el2.pdf

이 자료 보면서 완전성 증명 중인데 처음부터 막히네요 ㅇㅅㅇ;;

일단 "모든 formula들을 나열할 수 있다"부터 막막하네요.

nat에서 formula로 가는 전단사함수를 어떻게 구성해야할지 모르겠습니다.

Coq가 직관주의라서 존재함을 보이려면,

실제로 그걸 줘야하거든요.

힌트 주실 수 있나요? ㅠㅠ