pith. sign in

arxiv: 1906.11236 · v1 · pith:OJHBNQFAnew · submitted 2019-06-26 · 🧮 math.LO · math.CO

First-order proofs without syntax

Dominic J. D. Hughes This is my paper

Pith reviewed 2026-05-25 14:54 UTC · model grok-4.3

classification 🧮 math.LO math.CO
keywords combinatorial proofsfirst-order logiclax fibrationgraph-theoretic proofssoundness and completenesspredicate calculusvaliditygraph morphism
0
0 comments X

The pith

A first-order formula is valid exactly when it admits a combinatorial proof as a lax fibration over its associated graph.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Traditional proofs in first-order logic are syntactic objects generated inductively from axioms and rules. This paper replaces that inductive syntax with graph-theoretic objects. It associates a graph with each formula and defines a combinatorial proof as a lax fibration into that graph. The main theorem establishes that such a fibration exists if and only if the formula is semantically valid. This equivalence gives a non-syntactic characterization of validity that rests entirely on the existence of a certain graph morphism.

Core claim

The paper proves that a first-order formula φ is valid if and only if it possesses a combinatorial proof, where a combinatorial proof is a lax fibration over the graph associated with φ.

What carries the argument

A lax fibration over the graph associated with the formula, which serves as the combinatorial stand-in for a proof.

If this is right

  • Validity can be certified by the existence of a graph morphism of a specific kind rather than by a syntactic derivation.
  • The inductive construction of proofs is eliminated; only the existence of the fibration matters.
  • Soundness and completeness are established simultaneously for this graph-theoretic notion of proof.
  • First-order logic receives an equivalent combinatorial semantics that makes no reference to terms or formulas as syntactic entities.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Search procedures for proofs could be recast as searches for fibrations in graphs rather than term manipulations.
  • The approach supplies a static, non-inductive object that could be compared directly with semantic models.
  • Similar graph constructions might be tested on fragments of first-order logic or on related systems such as equational logic.

Load-bearing premise

The graph constructed from each formula and the precise definition of lax fibration are set up so that they capture exactly the standard semantic notion of validity.

What would settle it

Exhibit a first-order formula that is semantically valid yet admits no lax fibration over its graph, or a formula that is not valid yet does admit such a fibration.

Figures

Figures reproduced from arXiv: 1906.11236 by Dominic J. D. Hughes.

Figure 1
Figure 1. Figure 1: A syntactic proof of ∃x(px ⇒ ∀y py), in Gentzen’s sequent calculus LK [Gen35]. x px y py pfy (∀x px) ⇒ ∀y (py∧pfy) qab qba x y qxy qab ∨ qba ⇒ ∃x ∃y qxy x pfx px y pffy py [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Four combinatorial proofs, each shown above the formula proved. Here x and y are variables, f is a unary function symbol, a and b are constants (nullary function symbols), p is a unary predicate symbol, and q is a binary predicate symbol [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Condensed forms of the four combinatorial proofs in [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A skew bifibration (left), its binding fibration (centre), and its skeleton (right). x px y qy pz qfz z x px y qy pz qfz z [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: A fonet N (left) with unique dualizer {x7→z, y7→fz} and its leap graph LN (right). 5 Fonets (first-order nets) Two atoms are pre-dual if they have dual predicate symbols (e.g. pxy and pyfa) and two literals are pre-dual if their atoms are pre-dual. Definition 5.1. A linked fograph is a coloured fograph such that • every colour, called a link, comprises two pre-dual literals, and • every literal is either 1… view at source ↗
Figure 6
Figure 6. Figure 6: A standard combinatorial proof (left) and a homogeneous combinatorial proof (right) of Peirce’s law (p⇒q)⇒p  ⇒p = [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Four simple propositions ϕ (top row), their fographs G(ϕ) (middle row), and their dualizing graphs D(ϕ). Each vertex in G(ϕ) and D(ϕ) is aligned vertically with the corresponding atom occurence in ϕ. Dualities are shown dashed and curved. Definition 7.2. The dualizing graph D(ϕ) of a simple proposition ϕ is the dualizing graph D with • VD = { occurrences of predicate symbols in ϕ }, • vw ∈ ED if and only i… view at source ↗
Figure 8
Figure 8. Figure 8: A combinatorial proof f : N → G of the monadic formula ∃x(px ⇒ ∀y py) (left), copied from the Introduction, and its homogeneous combinatorial proof f ′ : N′ → G′ (right). The directed edges of N′ and G′ are those of the binding graphs N and G, the dashed edge of N′ captures the colour of N, and the dashed edge of G′ captures the duality between the two predicate symbols p and p in G. 7.3 Propositional homo… view at source ↗
Figure 9
Figure 9. Figure 9: A monadic formula ϕ, its fograph G(ϕ), and its mograph M(ϕ), respectively. of a binding, otherwise a binder. If hb,li ∈ BM we say that b binds l. 15 The scope of a binder b in M is the smallest proper strong module of (VM, EM) containing b. Definition 8.2. A mograph M is a pre-mograph such that no binder is in a duality, every binder has non-empty scope, and hb,li ∈ BM only if l is in the scope of b. For e… view at source ↗
Figure 10
Figure 10. Figure 10: A monet N (left) and its leap graph LN (right). 8.1 Monets A mograph is linked if every literal is in a unique duality. An example of a linked mograph is shown in [PITH_FULL_IMAGE:figures/full_fig_p011_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Examples E1–6. Each syntactic formula ϕ is followed by its graph G = G(ϕ), cotree T(G), and binding graph G. Examples E5 and E6 show two syntactic formulas with the same combinatorial formulas [PITH_FULL_IMAGE:figures/full_fig_p039_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Examples E7–12. Each syntactic formula ϕ is followed by its graph G=G(ϕ), cotree T(G), and binding graph G. Each example shows multiple syntactic formulas with the same combinatorial formula [PITH_FULL_IMAGE:figures/full_fig_p040_12.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper reformulates first-order logic proofs in graph-theoretic terms rather than as inductively generated syntactic objects. It defines a combinatorial proof of a formula φ as a lax fibration over a graph associated with φ, and establishes soundness and completeness: a formula is valid if and only if it admits such a combinatorial proof.

Significance. If the result holds, the work supplies an explicit combinatorial characterization of first-order validity that avoids traditional syntactic induction. The manuscript provides direct constructions for the formula-associated graph and the lax fibration relation together with a direct soundness-and-completeness argument; these features strengthen the contribution by making the equivalence checkable without hidden parameters or self-reference.

minor comments (3)
  1. The abstract states the main theorem but does not indicate the arity or signature of the graph construction; a single sentence summarizing the vertex/edge sets would improve accessibility.
  2. Notation for the lax fibration relation (e.g., the precise meaning of the 'lax' condition in the first-order setting) is introduced without an immediate small example; adding one in §2 or §3 would clarify the definition for readers unfamiliar with fibration terminology.
  3. The manuscript should explicitly state whether the graph construction is functorial with respect to formula substitution or only defined for closed formulas; this affects the scope of the completeness claim.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript and the recommendation for minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity; explicit constructions with direct proof

full rationale

The paper defines the formula graph and lax fibration explicitly, then proves soundness and completeness directly. No load-bearing step reduces the validity equivalence to a self-referential definition, fitted parameter, or self-citation chain; the central claim rests on independent graph-theoretic constructions and argument rather than by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper introduces a new definition of combinatorial proofs resting on standard first-order logic semantics and graph theory; no free parameters are mentioned and no new physical entities are postulated.

axioms (1)
  • domain assumption Standard semantics of first-order predicate logic
    The validity notion being characterized is the usual model-theoretic one presupposed by the soundness-completeness claim.
invented entities (1)
  • lax fibration over a formula-associated graph no independent evidence
    purpose: To serve as the definition of a combinatorial proof
    New combinatorial object introduced to replace syntactic proofs; no independent evidence outside the paper is supplied in the abstract.

pith-pipeline@v0.9.0 · 5569 in / 1207 out tokens · 39568 ms · 2026-05-25T14:54:33.521245+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

56 extracted references · 56 canonical work pages

  1. [1]

    Alcolei, P

    A. Alcolei, P. Clairambault, J. M. E. Hyland, and G. Winskel. The true concurrency of herbrand's theorem. In CSL'18 , 2018

    work page 2018

  2. [2]

    P. B. Andrews. Refutations by matings. IEEE Transactions on Computers , 25(8), 1976

    work page 1976

  3. [3]

    P. B. Andrews. Theorem proving via general matings. J.\ ACM , 28, 1981

    work page 1981

  4. [4]

    Acclavio and L

    M. Acclavio and L. Stra burger. From syntactic proofs to combinatorial proofs. In Int.\ Joint Conf.\ on Automated Reasoning . Springer, 2018

    work page 2018

  5. [5]

    W. Bibel. An approach to a systematic theorem proving procedure in first-order logic. Computing , 12(1), 1974

    work page 1974

  6. [6]

    W. Bibel. On matrices with connections. J.\ ACM , 28(4), 1981

    work page 1981

  7. [7]

    Bellin and J

    G. Bellin and J. Ketonen. A decision procedure revisited: Notes on direct logic, linear logic and its implementation. Theor.\ Comp.\ Sci. , 95:115--142, 1992

    work page 1992

  8. [8]

    A. Carbone. A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs. Inf.\ Comput. , 208(5), 2010

    work page 2010

  9. [9]

    D. G. Corneil, H. Lerchs, and L. K. Stewart-Burlingham . Complement reducible graphs. Disc.\ Appl.\ Math. , 1981

    work page 1981

  10. [10]

    S. A. Cook and R. A. Reckhow. The relative efficiency of propositional proof systems. J.\ Symb.\ Logic , 44:36--50, 1979

    work page 1979

  11. [11]

    G. V. Davydov. The synthesis of the resolution method with the inverse method. Zapiski Nauchnykh Seminarov Lomi. , 20:24--35, 1971. Translation in J.\ Sov.\ Math.\ 1(1) 1973 12-–18

    work page 1971

  12. [12]

    Eilenberg and G

    S. Eilenberg and G. M. Kelly. A generalization of the functorial calculus. J.\ Algebra , 3:366--375, 1966

    work page 1966

  13. [13]

    G. Frege. Begriffsschrift, eine der arithmetischen nachgebildete F ormelsprache des reinen D enkens . Halle, 1879

    work page

  14. [14]

    T. Gallai. Transitiv orientierbare graphen. Acta Math.\ Acad.\ Sci.\ Hungar , 18:25--66, 1967

    work page 1967

  15. [15]

    G. Gentzen. Untersuchungen \"u ber das logische S chlie en. II . Mathematische Zeitschrift , 39:405--431, 1935

    work page 1935

  16. [16]

    J.-Y. Girard. Linear logic. Theor.\ Comp.\ Sci. , 50:1--102, 1987

    work page 1987

  17. [17]

    J.-Y. Girard. Towards a geometry of interaction. In Categories in Computer Science and Logic , volume 92 of Contemporary Mathematics , pages 69--108, 1989. Proc.\ of June '87 meeting in Boulder, Colorado

    work page 1989

  18. [18]

    J.-Y. Girard. A new constructive logic: Classical logic. Mathematical Structures in Comp.\ Sci. , 1:255--296, 1991

    work page 1991

  19. [19]

    J. W. Gray. Fibred and cofibred categories. In Proc.\ Conf.\ on Categorical Algebra '65 , pages 21--83. Springer, 1966

    work page 1966

  20. [20]

    Grothendieck

    A. Grothendieck. Technique de descente et th\'eor\`emes d'existence en g\'eom\'etrie alg\'ebrique. I . G \'en\'eralit\'es. D escente par morphismes fid\`element plats. In S\'eminaire Bourbaki: ann\'ees 1958/59--1959/60, expos\'es 169-204 . Soci\'et\'e math\'ematique de France, 1960

    work page 1958

  21. [21]

    Heijltjes

    W. Heijltjes. Classical proof forestry. Annals of Pure and Applied Logic , 161(11), 2010

    work page 2010

  22. [22]

    Herbrand

    J. Herbrand. Recherches sur la th\'eorie de la d\'emonstration . PhD thesis, Sorbonne, Paris, 1930

    work page 1930

  23. [23]

    Heijltjes, D

    W. Heijltjes, D. J. D. Hughes, and L. Stra burger. Intuitionistic proofs without syntax. In Proc.\ LICS'19 , 2019

    work page 2019

  24. [24]

    Heijltjes, D

    W. Heijltjes, D. J. D. Hughes, and L. Stra burger. Proof nets for first-order additive linear logic. In Proc.\ FSCD'19 , 2019

    work page 2019

  25. [25]

    H. Hu. Contractible Coherence Spaces and Maximal Maps. Electr. Notes Theor. Comput. Sci. , 20:309--319, 1999

    work page 1999

  26. [26]

    D. J. D. Hughes. Proofs without syntax. Annals of M athematics , 143:1065--1076, 2006

    work page 2006

  27. [27]

    D. J. D. Hughes. Towards H ilbert's 24 ^ th P roblem: C ombinatorial P roof I nvariants. In Proc.\ WOLLiC '06 , volume 165 of Lec.\ Notes in Comp.\ Sci. , 2006

    work page 2006

  28. [28]

    D. J. D. Hughes. Unification nets: canonical proof net quantifiers. In Proc.\ LICS '18 , 2018

    work page 2018

  29. [29]

    P. T. Johnstone. Note on Logic and Set Theory . Cambridge University Press, 1987

    work page 1987

  30. [30]

    G. M. Kelly and S. Mac Lane. Coherence in closed categories. J.\ Pure Appl.\ Algebra , 1:97--140, 1971

    work page 1971

  31. [31]

    A. Kotzig. On the theory of finite graphs with a linear factor ii. Mat.-Fyz. Casopis. Slovensk. Akad. Vied , 9(3), 1959

    work page 1959

  32. [32]

    Ketonen and R

    J. Ketonen and R. Wehyrauch. A decidable fragment of predicate calculus. Theor.\ Comp.\ Sci. , 32:297--307, 1984. Error in proof of main theorem corrected in BK92

    work page 1984

  33. [33]

    H. Lerchs. On cliques and kernels. Tech.\ report, U.\ Toronto, 1981

    work page 1981

  34. [34]

    Lov\'asz and M

    L. Lov\'asz and M. D. Plummer. Matching Theory . North-Holland, 1986

    work page 1986

  35. [35]

    Lamarche and L

    F. Lamarche and L. Stra burger. Naming proofs in classical propositional logic. In Proc.\ Typed Lambda Calculus '05 , Lec.\ Notes in Comp.\ Sci., 2005

    work page 2005

  36. [36]

    McKinley

    R. McKinley. Expansion nets: Proof nets for for propositional classical logic. In LPAR 17 , volume 6397 of LNCS , 2010

    work page 2010

  37. [37]

    McKinley

    R. McKinley. Proof nets for herbrand's theorem. ACM Trans.\ Comp.\ Logic , 14, 2010

    work page 2010

  38. [38]

    McKinley

    R. McKinley. Canonical proof nets for classical logic. Annals of Pure and Applied Logic , 164(6):702--732, 2013

    work page 2013

  39. [39]

    D. A. Miller. Expansion tree proofs and their conversion to natural deduction proofs. Lec.\ Notes in Comp.\ Sci. , 170, 1984

    work page 1984

  40. [40]

    S. Mimram. The structure of first-order causality. Mathematical Structures in Comp.\ Sci. , 21, 2011

    work page 2011

  41. [41]

    G. Mints. A short introduction to modal logic . CSLI, 1992

    work page 1992

  42. [42]

    Martelli and U

    A. Martelli and U. Montanari. Unification in linear time and space: a structured presentation. Technical report, U.\ Pisa, 1976

    work page 1976

  43. [43]

    C. S. Peirce. Description of a notation for the logic of relatives, resulting from an amplification of the conceptions of B oole's calculus of logic. In Collected Papers of Charles Sanders Peirce. III . E xact Logic . Harvard University Press, 1933

    work page 1933

  44. [44]

    D. Prawitz. A proof procedure with matrix reduction. Lecture Notes in Mathematics , 125, 1970

    work page 1970

  45. [45]

    W. V. Quine. A proof procedure for quantification theory. J.\ Symbolic Logic , 20(2), 1955

    work page 1955

  46. [46]

    Retor\'e

    C. Retor\'e. Handsome proof-nets: perfect matchings and cographs. Theor.\ Comp.\ Sci. , 2003

    work page 2003

  47. [47]

    J. A. Robinson. A machine-oriented logic based on the resolution principle. J.\ ACM , 12(1), 1965

    work page 1965

  48. [48]

    Robinson

    E. Robinson. Proof nets for classical logic. J.\ Logic and Computation , 13(5):777--797, 2003

    work page 2003

  49. [49]

    Stra burger

    L. Stra burger. A characterisation of medial as rewriting rule. In Term Rewriting and Applications, RTA07 , volume 4533. Lec.\ Notes in Comp.\ Sci., 2007

    work page 2007

  50. [50]

    Stra burger

    L. Stra burger. Combinatorial Flows and Their Normalisation . In Proc.\ FSCD 2017 , volume 84 of Leibniz Int.\ Proc.\ Informat. , 2017

    work page 2017

  51. [51]

    Stra burger

    L. Stra burger. The problem of proof identity, and why computer scientists should care about hilbert's 24th problem. Phil.\ Trans.\ Royal Soc.\ A , 377(2140), 2019

    work page 2019

  52. [52]

    D. P. Sumner. Graphs indecomposable with respect to the x-join. Discr.\ Math. , 6, 1973

    work page 1973

  53. [53]

    R. Thiele. Hilbert's twenty-fourth problem. The American Mathematical Monthly , 110(1), 2003

    work page 2003

  54. [54]

    A. S. Troelstra and H. Schwichtenberg. Basic Proof Theory . Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambrige, U.K., 1996

    work page 1996

  55. [55]

    Thiele and L

    R. Thiele and L. Wos. Hilbert's twenty-fourth problem. Journal of Automated Reasoning , 29(1):67--89, 2002

    work page 2002

  56. [56]

    Elements of Homotopy Theory

    G.W Whitehead. Elements of Homotopy Theory . Springer-Verlag, 1978

    work page 1978