Free Definite Description Theory – Sequent Calculi and Cut Elimination
Andrzej Indrzejczak
Abstract
We provide an application of a sequent calculus framework to the formalization of definite descriptions. It is a continuation of research undertaken in [20, 22]. In the present paper a so-called free description theory is examined in the context of different kinds of free logic, including systems applied in computer science and constructive mathematics for dealing with partial functions. It is shown that the same theory in different logics may be formalised by means of different rules and gives results of varying strength. For all presented calculi a constructive cut elimination is provided.
Topics & Concepts
SequentSequent calculusMathematicsCut-elimination theoremCalculus (dental)Discrete mathematicsMathematical proofGeometryMedicineDentistryLogic, Reasoning, and KnowledgeLogic, programming, and type systemsAdvanced Algebra and Logic