Duality between unprovability and provability in forward proof-search for Intuitionistic Propositional Logic

TL;DR

This paper introduces a forward proof-search method for Intuitionistic Propositional Logic that can determine unprovability by constructing minimal height countermodels and extracting derivations from failed proof searches.

Contribution

It develops a new forward calculus FRJ(G) for unprovability in intuitionistic logic, enabling constructive unprovability proofs and minimal countermodel generation.

Findings

Constructs minimal height countermodels for unprovability.

Provides a method to extract derivations from failed proof searches.

Clarifies the role of saturated databases in proof and unprovability.

Abstract

The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability which is prone to constructively ascertain the unprovability of a formula G by providing a concise countermodel for it; in particular we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as result of a failed proof-search in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.