Natural deduction for neutral free logic with definite descriptions

Yaroslav Petrukhin

We provide natural deduction systems for the minimal theory of definite descriptions grounded in Lambert’s axiom within the context of neutral free logic. This framework accommodates non-denoting terms by introducing a third truth value for the case of formulae that include them, in addition to the traditional true and false values. We adhere to Pavlović and Gratzl’s approach [1] regarding quantifiers, atomic formulas, and simple terms. However, we diverge by utilising natural deduction systems instead of sequent calculi. Additionally, we enhance their foundational framework by integrating identity and definite descriptions into the system. We focus on the normalisation theorem for the natural deduction systems indicated above.

Bibliography

1. E. Pavlovi’{c} and N. Gratzl,Neutral Free Logic: Motivation, ProofTheory and Models,Journal of Philosophical Logic,vol. 52 (2023), no. 2, pp. 519–554.

 Overview  Program