arXiv:2105.06877 Abstract | arXiv Analytics

arXiv:2105.06877 [math.LO]Abstract References Reviews Resources

First order logic properly displayed

Samuel Balco, Giuseppe Greco, Alexander Kurz, Andrew Moshier, Alessandra Palmigiano, Apostolos Tzimoulis

Published 2021-05-14, updated 2021-05-19Version 2

We introduce a proper display calculus for first-order logic, of which we prove soundness, completeness, conservativity, subformula property and cut elimination via a Belnap-style metatheorem. All inference rules are closed under uniform substitution and are without side conditions.

Categories: math.LO

Subjects: 03B10, 03B35, 03B45, 03B47, 03F03, 03F05, 03F07, 03G05, 03G10, 03G15, 03G30, 06A06, 06A11, 06D10, 06D50, 06E15

Keywords: first order logic, proper display calculus, side conditions, subformula property, cut elimination

Related articles: Most relevant | Search more

arXiv:math/0210387 [math.LO] (Published 2002-10-24)

Consistency Without Cut Elimination

Kai Bruennler, Alessio Guglielmi

arXiv:1606.01763 [math.LO] (Published 2016-06-06)

A Constructive Proof of Cut Elimination for a System of Full Second Order Logic

Sandro Skansi

arXiv:1605.03501 [math.LO] (Published 2016-05-11)

Is Leibnizian calculus embeddable in first order logic?

Piotr Blaszczyk, Vladimir Kanovei, Karin U. Katz, Mikhail G. Katz, Taras Kudryk, Thomas Mormann, David Sherry

Links

Toolbox