{
  "id": "2105.06877",
  "version": "v2",
  "published": "2021-05-14T15:03:45.000Z",
  "updated": "2021-05-19T11:58:07.000Z",
  "title": "First order logic properly displayed",
  "authors": [
    "Samuel Balco",
    "Giuseppe Greco",
    "Alexander Kurz",
    "Andrew Moshier",
    "Alessandra Palmigiano",
    "Apostolos Tzimoulis"
  ],
  "categories": [
    "math.LO"
  ],
  "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.",
  "revisions": [
    {
      "version": "v2",
      "updated": "2021-05-19T11:58:07.000Z"
    }
  ],
  "analyses": {
    "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"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}