Towards a proof theory for Henkin quantifiers. (5th January 2021)

• Record Type: Journal Article
• Authors: Baaz, Matthias; Lolic, Anela
• Is Part Of: Journal of logic and computation. Volume 31:Number 1(2021)
• Page Start: 40
• Page End: 66
• Publication Date: 2021-01-05
• Subjects: Henkin quantifiers -- sequent calculus -- cut elimination; Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exaa071
• Languages: English
• ISSNs: 0955-792X

Abstract

Abstract: This paper presents a methodology to construct globally sound but possibly locally unsound analytic calculi for partial theories of Henkin quantifiers. It is demonstrated that usual locally sound analytic calculi do not exist for any reasonable fragment of the full theory of Henkin quantifiers. This is due to the combination of strong and weak quantifier inferences in one quantifier rule.