A NEW DECISION METHOD FOR INTUITIONISTIC LOGIC BY 3-VALUED NON-DETERMINISTIC TRUTH-TABLES
Renato Reis Leme, Marcelo E. Coniglio, Bruno Lopes · Journal of Symbolic Logic · 2025
Abstract Kurt Gödel proved that it is not possible to characterize intuitionistic propositional logic ( ${IPL}$ ) by means of finite and deterministic truth-tables. After extending the same result with respect to non-deterministic matrices (Nmatrices), we provide a semantical characterization of ${IPL}$ by means of a $3$ -valued Nmatrix with a restricted set of valuations. This structure allows to define an algorithm to delete unsound rows from the non-deterministic truth-tables generated for each formula, which constitutes a new and very simple decision procedure for ${IPL}$ . This method can be seen as truth-tables in a broader sense, and a way to overcome Gödel’s limiting result.