{"id":"arxiv/2606.11735","url":"https://arxiv.org/abs/2606.11735","tags":["math.LO"],"score":0,"title":"Normalisation for Positive Free Logics without and with Definite Descriptions","domain":"math.LO","source":"arxiv","authors":["Nils Kürbis"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-10","reactions":{}}