Two Senses of ‘Not True’ and the Intuitionistic Natural Deduction System.
‘참이 아님’의 두 가지 뜻과 직관주의 자연연역 체계
The present article argues that the standard intuitionistic natural deduction system fails to adequately capture the notion of ‘not true’ in the intuitionistic sense. Initially, it examines how historical intuitionists have employed the concept of ‘not true’ in two distinct ways, particularly emphasizing L. E. J. Brouwer’s weak and strong counterexamples and Michael Dummett’s intuitionistic notion of truth.
Two significant problems emerge from the use of ‘not true’ within the standard intuitionistic system: (1) the system proves the rejection of negating the law of excluded middle (LEM), which leads to a contradiction; and (2) it establishes an equivalence between ‘𝜑 is not true’ and ‘𝜑 is false,’ the equivalence intuitionistically unacceptable. These issues demonstrate that the standard system inadequately formalizes the intuitionistic concept of ‘not true,’ thereby failing to fully articulate the intuitionistic stance against LEM.
To address these deficiencies, an enhanced intuitionistic natural deduction system is proposed, incorporating both the classical falsity constant (⊥) and an intuitionistic absurdity symbol (⋏), explicitly representing
본 논문은 표준 직관주의 자연연역 체계가 ‘참이 아님’에 대한 직관주의적 의미를 적절히 포착하지 못한다고 주장한다. 먼저, 역사적으로 직관주의자들은 ‘참이 아님’을 두 가지 방식으로 사용했음을 살펴 본다. 특히 L. E. J. 브라우어의 약한 반례와 강한 반례 그리고 마이클 더밋의 직관주의적 진리 개념에 초점을 맞춰 이를 탐구한다. 표준 직관주의 체계에서 ‘참이 아님’을 사용할 때 두 가지 중요한 문제가 발생한다. 첫째, 이 체계는 배중률 문장의 이중부정 형식이 증명되며 이는 모순을 야기한다. 둘째로 이 체계에서는 “𝜑가 참이 아니다.”와 “𝜑가 거짓이다.”가 동치임이 증명된다. 이는 직관주의적 으로 받아들일 수 없는 부분이다. 이러한 문제들은 표준 체계가 ‘참이 아님’의 직관주의적 의미를 적절히 형식화하지 못함을 보이는 것이며 배중률에 대한 직관주의적 입장을 명확히 표현하지 못함을 보여준다. 이러한 문제점을 해결하기 위해, 증명 없음을 표현할 수 있는 직관주의 자연연역 체계를 제안한다. 이 체계는 고전적 거짓을 표현하는 상항인 ⊥과 증명 없음을 표현하는 ⋏를 차용한다. 이를 통해 제시된 두 가지 문제가 해결됨을 확인할 수 있으며 마지막으로 ⋏를 논리 상항으 로 고려해야 하는 가에 대한 문제를 논한다.
한국논리학회, 한림대학교 최승락
