호프스태만 mu 시스템인데
공리는 mi하나고 위의 네가지 추론규칙을 사용하여 정리를 만드는 간단한 시스템입니다
근데 여기서 mu를 네가지 추론규칙을 사용하여 만들 수 있냐는 게 질문입니다
답은 시스템 안에서는 얻기 어렵지만 각각 규칙 고려하여 수학적 귀납법을 적용하면 간단하게 mu를 얻을 수 없다는 걸 알 수 있습니다.
1. 근데 사실 귀납법이 페아노공리나 이런 쪽에서 공리로 받아드리고 있는데 왜 mu시스템에 적용해도 되는지 헷갈립니다.
이게 더 헷갈리는데
명제논리에서 sigma가 무모순일때 sigma pi와 sigma not pi 둘 중 하나는 무모순임을 밝힐때 귀류법을 적용하는데
2. 명제논리안에서 귀류법이 작동하는건 알겠는데
위와 같이 명제논리에 대한 정리에서도 귀류법을 써도 되는지 모르겠어요..
뭔가 완전 잘못생각하고 있는거 같은데
관련된 자료나 이런거 있으면 알려주실수있나요
물어볼사람이 없어서 ㅠㅠ
1번은 structural induction 찾아보면 되고요. (coq식으로 설명하자면 rule에 대하여 induction을 건 거에요) 2번은 배중률을 믿으시면 당연히 되는 거고요
2번은 그냥 배중률이라는 걸 믿고있다는 전제로 간다고 생각하면 될까요? 실례지만 괜찮다고 생각되는 책있으면 추천해주실수 있나요..? 번역서면 좋지만 원서도 괜찮아요 답변 감사합니다 정말
배중률을 헷갈려하는게 좀 찾아보니까 직관주의 이런쪽은 배중률을 안 믿는다고 해서요 수리논리학은 아무래도 배중률을 무조건적으로 수용할거라고 생각하지는 않았습니다
수리논리 책 추천해드리자면, 저에게는 정주희 교수님 책이 좋았어요. 그런데 그 책도 읽다보면 오류를 만나게 돼요. 특징으로는 완전성 정리는 다루지 않지만, 추론규칙이 훨씬 예쁩니다. 구성은 6단원은 기초집합론이고 7단원이 본격적인 집합론이에요. 여기서 본격적이라는 말은 모든 게 다 집합인 세계를 다룬다는 뜻입니다. 그리고 개인적으로 2장은 안 봐도 될 것 같아요.
아... 대상논리에서 배중률을 쓰면 완전성 정리 증명하려면 배중률이 필요하더라고요, 직접해보니까요.
증명을 직접시도 해보니깐 대상논리에서 완정성정리 증명하는데 배중률이 필요해서 쓰고있다 라고 생각해도 될까요? 책추천감사해요 꼭 한번 읽어볼게요
메타논리에서 대상논리의 완전성을 증명하는 데 메타논리의 배중률이 필요하다는 말씀을 드린 것입니다.
공부가 부족해서 계속 질문드려서 죄송한데 그럼 메타논리의 추론규칙은 어떻게 정하는거죠..ㅠㅠ
저도 그게 궁금해서 혼자서 고민했는데, 그 답이 coq이라는 증명보조기라고 생각하게 되었어요.
coq가 뭔지 잘 모르지만 coq를 기반으로 생각하셨다는 거 같네요 감사합니다 저도 좀 더 생각해보겠습니다