형식 증명 원래 조온나 어렵나요?

[더블초코냥(218.232)]

저만 Coq이 어렵나요??

명제 논리의 완전성을 증명하고 싶은데,

maximally consistent set을 못 잡겠어요 ...

혹시 완전성 증명해보시거나 Coq 잘 아시는 분 계신가요?

[익명(211.197)]

1차논리 완전성 증명은 꽤 난이도가 있지만 명제논리는 그리 어렵지 않을 텐데... 구체적으로 어떤 부분이 막힘?

[더블초코냥(218.232)]

일단 자연수에서 명제논리식으로 가는 전사함수를 못 잡겠어요. 기껏 전사함수를 만들었더니, Coq가 재귀가 잘못되었다고 거절했어요.

[익명(182.216)]

에러 메시지가 뭐라고 뜸? Cannot guess decreasing argument... 같은 거면 termination check 문제임.

[더블초코냥(218.232)]

subterm만 가지고 재귀하라고 했어요

[익명(182.216)]

그리고 특정 증명체계를 꼭 써야 하는게 아니라면 sequent calculus의 완전성을 증명하는게 아마 훨씬 쉬울 듯.

[더블초코냥(218.232)]

오 그런가요?? 조언 감사합니다. 겐첸의 자연연역에 대해서는 건전성이랑 약완전성까지 증명해서 완전성까지 보이고 싶었어요 ㅎㅎ

[익명(182.216)]

ㅇㅇ subterm 도 같은 문제임. Coq의 모든 함수는 유한시간 안에 종료해야 하는데, subterm 이 아닌 인자로 재귀를 하면 컴파일러가 termination 을 자동으로 확인할 수가 없음.

[더블초코냥(218.232)]

수동으로 확인하는 법은 없나요??

[더블초코냥(218.232)]

제가 수동으로 해서 coq한테 알려줘서 쓸 수 있는 법은 없나요?

[익명(182.216)]

수동으로 유한종료를 증명해서 컴파일러를 도와주는 방법이 있긴 한데 증명기마다 문법이 조금씩 다르고 내가 Coq 유저가 아니라서... 웬만하면 그냥 subterm만 사용하도록 함수 정의를 바꾸는 게 가장 편함.

[더블초코냥(218.232)]

그렇군요 ㅠㅠ 아무튼 정말 감사합니다. 복 많이 받으세요.