# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1906.11236