Towards a proof theory for quantifier macros

This paper focuses on globally sound but possibly locally unsound analytic sequent calculi for quantifier macros defined by sequences of quantifiers. It is demonstrated that no locally sound analytic representation based on the usual eigenvariable condition exists. In consequence, representations by globally sound but possibly locally unsound analytic sequent calculi are used. Cut-elimination is shown by translating proofs into LK and retranslating cut-free proofs into the desired format. Finally, criteria are given for sequents to be proved without reference to the extended eigenvariable conditions.

Authors

• Matthias Baaz
• Anela Lolic

Keywords

• Sequent calculus
• Cut-elimination
• Quantifier macros