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

2023/08/25 by RENATO R. LEME, Leme, Renato, MARCELO E. CONIGLIO +3 · 1 citation
#03B20 #03B25 #03B35 #03B45 #68V15 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2308.13664

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.

Cited by

• Hyper swap structures and Kalman functors: the case study of da Costa logic C_ω

Related

• Efficient Decision Procedures for RNmatrix Semantics
• On the Jaśkowski Models for Intuitionistic Propositional Logic
• A polynomial time complete disjunction property in intuitionistic propositional logic
• A simple decision procedure for da Costa's Cn logics by Restricted Nmatrix semantics
• First-Order Intuitionistic Logic with Decidable Propositional Atoms