First-order proofs without syntax
Logic
2019-06-27 v1 Combinatorics
Abstract
Proofs are traditionally syntactic, inductively generated objects. This paper reformulates first-order logic (predicate calculus) with proofs which are graph-theoretic rather than syntactic. It defines a combinatorial proof of a formula as a lax fibration over a graph associated with . The main theorem is soundness and completeness: a formula is a valid if and only if it has a combinatorial proof.
Cite
@article{arxiv.1906.11236,
title = {First-order proofs without syntax},
author = {Dominic J. D. Hughes},
journal= {arXiv preprint arXiv:1906.11236},
year = {2019}
}
Comments
42 pages