Peter Smith의 IGT2를 읽던 도중 effectively axiomatized가 이해가 안 됩니다ㅠ
Effectively axiomatized Theory면 T has a proof system that it is an effectively decidable whether an array of wffs conforms to the proof building rules라고 하므로 T's theroems are decidable이라고 하는 것은 괜찮은가요?
Effectively axiomatized Theory면 T has a proof system that it is an effectively decidable whether an array of wffs conforms to the proof building rules라고 하므로 T's theroems are decidable이라고 하는 것은 괜찮은가요?
글고 보편양화사랑 존재양화사 키보드로 입력하는 법 좀 알려주세여ㅠㅠㅠ
ㄷ key + 한자 key
Theorem 자체가 증명된 참인 명제인데 undecidable theorem이라는 말이 의미가 있어요? 증명이론은 잘 몰라서..
컴퓨터 프로그램으로 만들 수 있는지 따지는 거니까, 적어도 컴퓨터쟁이들한테는 중요하죠.
컴퓨터과학자들에게 한정하더라도 애당초 결정가능성은 임의의 wff에 관한 거 아니에요? theorem이면 이미 증명 가능한 건데(증명되어야 정리이므로)
그러니까 어떤 wff를 컴퓨터한테 주고 그게 Theory에 속하는지 답하게 하는 거죠 ㅎㅎ 예를 들어 주어진 문장이 Presburger Arithmetic의 이론인지 결정하는 프로그램을 테스트하는 코드는 여기서 보실 수 있습니다:
https://github.com/KiJeong-Lim/ppap/blob/master/src/Jasmine/Solver/Presburger/Test.hs
넵 그건 그냥 decidability의 뜻이고... 여기 질문에서는 T's theorems are decidable이라고 할 수 있냐고 하길래 물어본 거예요! 결정가능성이 어떤 의미이고 왜 중요한지는 아는데, T is decidable system이라는 말이 아니라 T's "theorems are" decidable이라는 말이 이상해 보여서요.
다시 보니까 제가 완전히 착각했었네요 ㅠㅠ 시비 걸어서 죄송합니다 ...
제 부족한 언어능력이 발목을 잡는군요 죄송합니다
T is decidable을 의도한 질문이었나보군요!
Enumerability Theorem 2.4.24 For any effective language L and any L-theory T, (i) if T is decidably axiomatizable, then T is effectively enumerable; (ii) if T is decidabley axiomatizable and complete, then T is decidable. 출처: Peter G. Hinman저 Fundamentals of Mathematical Logic
궁금한게 있는데요 axiomatized theory에서 enumerable한게 알파벳 순서대로 나열했을 때 그 theory에 속하는지 안 속하는지를 La를 통해 알 수 있어서 그런거잖아요
그럼 모든 wff에가 그것이 axiomatized theory여서 알파벳 순서대로 계속 나열하고 proof system에 올바른지 확인할 수 있으므로 decidable한 거 아닌가요
근데 이렇게 생각하면 effectively axiomatized theory 중 sufficiently strong하고 consistent하고 decidable한게 없다는 거랑 모순 아닌가요 도대체 어디에서 잘못 이해한건지 모르겠어요
그렇게 나열해도 종료하지 않을 수도 있잖아요. T가 complete하면 그렇게 나열할 때 그 명제 혹은 그 명제의 부정이 무조건 나오겠죠? 그래서 decidable해요.
그러니까 T가 decidably axiomatizable하다면, T를 주르륵 나열할 수는 있는데, 원하는 결론이 그 리스트의 원소인지를 결정할 수가 없는 거죠. 여기서 '결정'이란 유한 시간 안에 답을 무조건 내놓는 알고리즘이 있어야 한다는 뜻입니다.
요약하자면, T에 속하는 원소를 나열하기만 하는 프로그램만 가지고 있을 때에는: 주어진 문장이 T에 속할 경우 유한 시간 안에 무조건 yes를 내놓지만, 그렇지 않을 때에는 유한 시간 안에 무조건 no를 내놓는 프로그램을 만들 수 없다는 게 요지에요. 그러나 T가 complete하기도 하다면, 주어진 문장이나 그 부정이 무조건 리스트에 걸리기 때문에 유한 시간 안에 답하는 프로그램이 나와요.
감사합니다ㅠㅠ