일단, 저 증명이 맞는지 틀린지부터 논하자면, 그것은 논리 체계에 의존함.


대체로 증명이라는 거 자체를 특정한 규칙을 만족하는  명제의 유한 나열로 보는데, 


여기서 특정한 규칙을 어떻게 설정하는지에 따라 달라짐. 

즉, 현대 수리논리학에서는 참-거짓 여부와 증명이라는 것을 철저히 분리된 개념으로 봄. 증명 규칙을 어떻게 설정하는지에 따라서 참-거짓과의 연관성은 강해질 수도, 약해질 수도 있음. 


그리고 다이아코네쿠스 정리를 논할 때 우선적으로 논해야 할 사항이 바로 어느 논리 체계에서 논증하는가인데, 

그 논리 체계는 직관주의 논리 체계(intuitional logic)임. 

그리고 구성주의적 집합론은, 직관주의 논리 체계 위에서만 집합론을 서술하는 거임. 

이게 왜 중요하냐면, 컴공 등의 분야에서는 주어진 logic과 그 결과들을 알고리즘으로 연결시키는 게 중요한데, 구성주의 방법으로 유도된 결론들은 그렇게 알고리즘으로 연결시키기가 훨씬 수월하기 때문임.


그냥 순수하게 구성주의적인 증명으로 무엇을 유도할 수 있는가, 무엇을 유도할 수 없는가의 관점에서 다룸.  

true라는 결론이 나왔다고 증명 가능인 게 아님. 이건 ZFC 체계도 마찬가지지만. 

그래도 Sound system이니까 false라는 결론이 나오면 증명 불가능한 건 맞지만. 



구성주의 논리에 대해서 좀 더 서술하자면, 귀류법, 대우, 배중률 혹은 그와 비슷한 것들을 추론 규칙에서 배제한 거임. 그렇다고 해당 추론 규칙이 거짓이라고 가정한 것도 아니고, 반대로 참이라고 가정하는 것도 아님. 그저 추론 규칙으로서 배재했을 뿐임. 


 

좀 더 구체적으로는 다음과 같은 구성주의 논리가 있음. 

우선

1st or higher order logic with equality에서 natural deduction system들 중 하나에 대해 서술하자면, 

다음과 같이 크게 19개의 추론 규칙을 갖고 있음. 




(사진 출처 : The Logic Book, Sixth Edition - Merrie Bergmann.pdf (farka.eu) 의 맨 마지막 Appendix)


참고로 SD 는 sentential derivative system,

PD는 predicate derivative system,

PDE는 PD with equality라고 생각하면 됨. 

I는 introduction이고,  (추가하는 거)

E는 elimination임.  (없애는 거)


그러면 여기서 ~rule 2개를 없애면 직관주의 논리가 됨. 


근데, 여기서 ~rule 중에 ~I 규칙은 남기고, ~E 규칙만 배제할 수도 있음. 그건 순전히 서술하고 싶은 사람의 마음임. 


가령, ~P or P도 유도가 일반적으로 안 되고, ~P or ~~P도 유도가 일반적으로 안 되는 논리 체계를 선호할 수도 있고,

~P or P가 유도가 일반적으로 안 되고, ~P or ~~P는 유도가 되어도 상관 없다고 생각할 수도 있음. 

근데 개인적인 추측으로는 아마 전자를 더 선호할 것 같음. 나도 intuitional logic 분야는 공부를 안 해서 잘 모름.


참고로, 위 PDE랑 SD는 직관주의 논리 체계와 달리, completeness(완전성 정리)가 성립함. 


주어진 명제들로 이루어진 집합 A에 대해, 

A로부터 참이라고 결론이 내려지는 명제는 언제나 증명 가능하다는 정리임. 명제들은 당연히 주어진 논리 체계에서의 명제들이고.  (참고로, 여기서 모든 명제들의 집합은 countable한 논리 체계를 사용함.)

그래서 sentential logic에서는 truth-table로 참, 거짓을 판별하는데 truth-table로 참이라는 결론이 나왔으면 SD에서 그 증명 방법도 존재한다고 말할 수 있음.



그리고 PDE에서 ~rule 을 없애고 P or ~P를 공리로서 채택한 PDE'이라는 증명 체계는, PDE와 동등한 증명 능력을 가진다는 게 증명이 됨. 



그러니 다이아코네스의 정리라는 것은, 저 natual deduction system에 근거해서 설명하자면, ~ Rule 2개를 제외한, 나머지 17개의 추론 규칙을 허용했을 때 ZFC 공리 체계에서는 (P or ~P)가 유도된다는 정리이고 P or ~P가 유도되면 ~ Rule 2개를 제외한 것이 의미가 없어지니 구성주의 집합론에서는 axiom of choice를 배제할 명분이 됨. 

그렇다고 이것이 직관주의 논리의 ZF 공리 체계에서 선택 공리가 거짓이라는 걸 의미하지는 않음. 


정리를 설명할 때, 추론 규칙을 무엇을 허용하는지는 종종 생략되지만, constructive set theory 같은 일반적이지 않은 논리 체계를 사용할 때에는 반드시 어떤 논리 체계에서 서술하는지를 밝혀줘야 함.