First order logic properly displayed
Samuel Balco, Giuseppe Greco, Alexander Kurz, Andrew Moshier, and Alessandra Palmigiano, Apostolos Tzimoulis
TL;DR
This paper presents a new display calculus for first-order logic that is sound, complete, and has desirable proof-theoretic properties, with rules that are substitution-closed and side-condition free.
Contribution
It introduces a proper display calculus for first-order logic with proven soundness, completeness, and cut elimination, improving proof-theoretic methods.
Findings
Proved soundness and completeness of the calculus
Established cut elimination and subformula property
Rules are substitution-closed and side-condition free
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems