Camillo Fiorentini | Searcharxiv

arXiv2026

A G\"odel Modal Logic Over Witnessed Models

We introduce GW, a G\"odel modal logic based on Kripke models in which the value of each modal formula is witnessed by an accessible world. This witnessed semantics eliminates the limit-based phenomena that preclude the finite model property in the usual Kripke semantics for G\"odel modal logics, thereby yielding a more constructive semantic framework. We present a sound and complete refutation calculus for GW and design a terminating backward proof-search procedure with countermodel generation. As a direct consequence of this procedure, GW enjoys the finite model property.

cs.LO↗

arXiv2018

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

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.

math.LO↗