Two Senses of ‘Not True’ and the Intuitionistic Natural Deduction System.

Abstract

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