arXiv · 2606.11735
Normalisation for Positive Free Logics without and with Definite Descriptions
Abstract
This paper proves normalisation theorems for intuitionist and classical positive free logic, without and with the iota operator for definite descriptions `the F'. Positive free logic also opens a number of options for rules for iota. In total, six different formalisations of theories of definite descriptions will be discussed, three proposed by Lambert, and three alternatives. The latter are motivated by considerations relating to proof-theoretic harmony between introduction and elimination rules. The philosophical importance of the various systems and results is indicated. The paper builds on K\"urbis (2025), but is largely self-contained. The proofs for the present systems are easier than those for negative free logic.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Nils Kürbis. 2026-06-10. Normalisation for Positive Free Logics without and with Definite Descriptions. https://doi.org/10.1017/s1755020326101166
Cite the original work for its findings. Save a collection to share your selection of sources.