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

TL;DR

This paper introduces a novel 3-valued non-deterministic truth-table approach to characterize and decide Intuitionistic Logic, overcoming G"odel's limitations with finite deterministic tables.

Contribution

It provides a semantical characterization of IPL using a restricted 3-valued non-deterministic matrix and a simple decision algorithm, extending G"odel's classical results.

Findings

Developed a 3-valued non-deterministic matrix for IPL

Created an algorithm to remove unsound truth-table rows

Established a new decision procedure for IPL

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.