Tableaux for Free Logics with Descriptions
Andrzej Indrzejczak, Micha{\l} Zawidzki

TL;DR
This paper develops tableau proof systems for various free logic theories involving definite descriptions, including those used in computer science and mathematics, and proves their soundness and completeness.
Contribution
It introduces and formalizes tableau systems for multiple free logic variants, including negative and quasi-free logics, with proofs of soundness and completeness.
Findings
Tableau systems are sound for all considered free logics.
Tableau systems are complete with respect to their semantics.
The approach covers free logic with and without the existence predicate.
Abstract
The paper provides a tableau approach to definite descriptions. We focus on several formalizations of the so-called minimal free description theory (MFD) usually formulated axiomatically in the setting of free logic. We consider five analytic tableau systems corresponding to different kinds of free logic, including the logic of definedness applied in computer science and constructive mathematics for dealing with partial functions (here called negative quasi-free logic). The tableau systems formalise MFD based on PFL (positive free logic), NFL (negative free logic), PQFL and NQFL (the quasi-free counterparts of the former ones). Also the logic NQFLm is taken into account, which is equivalent to NQFL, but whose language does not comprise the existence predicate. It is shown that all tableaux are sound and complete with respect to the semantics of these logics.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
