First-order proofs without syntax

TL;DR

This paper introduces a novel graph-theoretic approach to first-order logic proofs, replacing traditional syntactic methods with combinatorial proofs based on graph fibrations, establishing soundness and completeness.

Contribution

It reformulates first-order logic proofs as combinatorial structures, providing a new perspective that bridges logic and graph theory.

Findings

Proofs are represented as graph fibrations over associated graphs.

Main theorem proves soundness and completeness of the combinatorial proof system.

Establishes equivalence between validity and existence of combinatorial proofs.

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 $\phi$ as a lax fibration over a graph associated with $\phi$. The main theorem is soundness and completeness: a formula is a valid if and only if it has a combinatorial proof.