First order logic properly displayed
Logic
2021-05-20 v2
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.
Cite
@article{arxiv.2105.06877,
title = {First order logic properly displayed},
author = {Samuel Balco and Giuseppe Greco and Alexander Kurz and Andrew Moshier and Alessandra Palmigiano and Apostolos Tzimoulis},
journal= {arXiv preprint arXiv:2105.06877},
year = {2021}
}