A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)

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, we provide a semantical characterization of IPL by means of a 3-valued non-deterministic matrix 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.

Several typos were corrected. Full proofs of soundness and completeness for S4 and IPL were included. IPL is now presented in terms of sequents, which allows us to fix a bug in the proof of our previous Lemma 4.32 (Co-analyticity). The Journal of Symbolic Logic, Accepted manuscript (Dec. 2025)