A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)
Abstract
Kurt G\"odel 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\"odel's limiting result.
Keywords
Cite
@article{arxiv.2308.13664,
title = {A new decision method for Intuitionistic Logic by 3-valued non-deterministic truth-tables (pre-print version)},
author = {Renato Leme and Marcelo Coniglio and Bruno Lopes},
journal= {arXiv preprint arXiv:2308.13664},
year = {2025}
}
Comments
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)