Talk: Nicola Bonatti (MCMP)

Title:

Intuitionistic Free Logic with ɛ-operator

Abstract:

Contrary to the classical case, the extension of intuitionistic predicate logic with Hilbert’s axiom for the ɛ-operator is not conservative. Shirai (1971) proposes an intuitionistic sequent calculus for a first-order language (without identity) enriched with an existence predicate and a suitably defined ɛ-operator. He further proves that this system is conservative over standard intuitionistic predicate logic. In this talk, we present a complete Kripke-style semantics for Shirai’s system. In our semantics, Shirai’s axioms correspond to restrictions on the interpretation of ɛ-terms. The completeness proof relies on the construction of reduction trees, which transform a failed proof search into a semantic countermodel (based on joint work with Norbert Gratzl).