{
  "id": "1902.07404",
  "version": "v1",
  "published": "2019-02-20T04:56:14.000Z",
  "updated": "2019-02-20T04:56:14.000Z",
  "title": "The Provability of Consistency",
  "authors": [
    "Sergei Artemov"
  ],
  "categories": [
    "math.LO"
  ],
  "abstract": "Provability semantics suggests well-principled notions of constructive truth and constructive falsity of classical sentences in Peano arithmetic PA. F is constructively true iff PA proves F. F is constructively false iff PA proves that for each x, there is a proof that x is not a proof of F. We also consider an associated notion of constructive consistency of PA, CCon(PA), for each x, there is a proof that x is not a proof of 0=1. We show that PA proves CCon(PA) hence there is no a Goedel-style impossibility barrier for case-by-case consistency proofs. Furthermore, we prove a finitary version of constructive consistency directly, for any PA-derivation S we find a finitary proof that S does not contain 0=1. This proves consistency of PA by finitary means and appears to vindicate Hilbert program of establishing consistency of formal theories.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2019-02-20T04:56:14.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F03",
      "03F25",
      "03F30",
      "03F40",
      "03F50"
    ],
    "keywords": [
      "vindicate hilbert program",
      "peano arithmetic pa",
      "case-by-case consistency proofs",
      "goedel-style impossibility barrier",
      "constructive consistency"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}