First order logic properly displayed

arXiv2105.06877MaRDI QIDQ6367658FDOQ6367658

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

Publication date: 14 May 2021

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.

Mathematics Subject Classification ID

Partial orders, general (06A06) Modal logic (including the logic of norms) (03B45) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof theory in general (including proof-theoretic semantics) (03F03) Cut-elimination and normal-form theorems (03F05) Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Categorical logic, topoi (03G30) Logical aspects of lattices and related structures (03G10) Cylindric and polyadic algebras; relation algebras (03G15) Algebraic aspects of posets (06A11) Complete distributivity (06D10) Logical aspects of Boolean algebras (03G05) Lattices and duality (06D50) Stone spaces (Boolean spaces) and related structures (06E15)

This page was built for publication: First order logic properly displayed

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6367658)