First-order proofs without syntax
Dominic J. D. Hughes



























T1qzc
T1qzcmit<-> s * [1.2] ec-qzcmi

qzcmit








Umathx45
Umathxmn
      <5> <6> <7> <8> <9> <10>
      <10.95> <12> <14.4> <17.28> <20.74> <24.88>
      mathx10
      
mathxUmathxmn
Umathxmn
0mathx"71
0mathx"75

#1



endtheorem



  
 
mythmstyle
  
  
  
  0pt
  
  .
   
  #1 #2 (#3)
mythmlikestyle
  
  
  
  0pt
  
  .
   
  #1 #2 (#3)
mythmstyle
theoremTheorem[section]
mythmlikestyle
corollary[theorem]Corollary
definition[theorem]Definition
lemma[theorem]Lemma
proposition[theorem]Proposition

proofof[1]
  * Proof of #1.□





















empty
empty








natural

nodesep=3pt,linewidth=.5pt,

	arrowsize=4pt 1,
	arrowlength=.9,
	arrowinset=.4











=.2pt
=1.5em
=0.3ex
=0.1ex
=0pt




























































































































let@tokenonedot
onedotlet@token..
e.g E.g
i.e I.e

c.f C.f
etc vs
w.r.t d.o.f
et al















=5mu plus 3mu minus 1mu
=4mu plus 2mu minus 3mu

oldsymbolsOMScmsymn
∧oldsymbols"5E
∨oldsymbols"5F
oldsymbols"3A

#1
  0=#1
  1#10.4OcFFS










































































































































































































































*->0ex1ex






















































































eqpic[3]
    (0,#1)(0,#2)pic[2]
    (0,#1)(0,#2)f
    
    .8
    .75
     
    222223
    
    
    
    
    
     egno
    
    
    
    
      
     
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
    
     First-order proofs without syntax
        
     Dominic J. D. Hughes
    
     Stanford University & U.C. Berkeley
    
      I conducted this research as a Visiting Scholar at Stanford then
      Berkeley. Many thanks to my hosts, Vaughan Pratt (Stanford Computer
      Science), Sol Feferman (Mathematics) and Wes Holliday
      (Berkeley Logic Group).
    
      I am extremely grateful for very helpful feedback from
      Willem Heijltjes, Lutz Straß burger, Grisha Mints, Sam Buss, Martin Hyland, Marc Bagnol and Nil Demirçubuk.
      In memoriam Sol and Grisha.
    
    
        December 30, 2023
    ====================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================
    
    
    
    4.75inProofs 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.
    
    
    
    
    § INTRODUCTION
    
    
    Proofs are traditionally syntactic, inductively generated objects.
    
    For example,
    
    Fig. <ref> shows a syntactic proof ofthe formula.
    
    This paper reformulates first-order logic (predicate calculus) <cit.> with proofs which are graph-theoretic rather than syntactic.
    
    It defines a combinatorial proof of a formula  as a lax graph fibration  over a graph  associated with , where  is a partially coloured graph.
    
    For example, if =
    then  is
    
    
    and a combinatorial proof  of  is
    
    
    
    
    The upper
    
    graph is 
    (two coloured vertices
    
    
    and three uncoloured vertices),
    
    the lower graph is ,
    
    and the dotted lines define .
    
    Additional combinatorial proofs are depicted in Fig. <ref>.
    
    The
    
    combinatorial proof  above can be condensed
    
    by leaving  implicit and drawing
    
    
    over the formula :
    
    
    
    
    The reader may contrast this with the
    
    syntactic proof of the same formula in Fig. <ref>.
    
    The four combinatorial proofs of Fig. <ref> are rendered in condensed form in Fig. <ref>.
    
    The main theorem of this paper is soundness and completeness: a formula is valid if and only if it has a combinatorial proof (Theorem <ref>).
    The propositional fragment was presented in <cit.>.
    
    
    
    § NOTATION AND TERMINOLOGY
    First-order logic
    We mostly follow the notation and terminology of <cit.> for first-order logic without equality <cit.>.comment 0 1
    Terms and atoms (atomic formulas) are generated
    
     inductively from variables x, y, z,… by: if γ is
    
    an n-ary
    function (resp. predicate) symbol
    
    and t_1,…,t_n are terms then γ t_1… t_n is a term (resp. atom).
    
    We extend the set of atoms with the logical constants 1 (true) and 0 (false).
    
    For technical convenience we assume every predicate symbol p is assigned a dual predicate symbol  with p and p, and extend duality to atoms with p0ex1.1ext_1… t_n= t_1… t_n,
    0=1 and 1=0.
    
    Formulas are generated from atoms by binary
    
    ∧
    and ∨
    and
    
    quantifiers ∀ x
    and ∃ x
    per variable x.
    
    Define 
    and 
    as abbreviations:
    
    (α)=α on atoms α,
    ()=()∨(),
    ()=()∧(),
    2mu∀ x2mu =∃ x2mu1mu,
    2mu∃ x2mu =∀ x2mu1mu,
    and
    =() ∨.
    A formula is rectified if all bound variables are distinct from one another and from all free variables, 
    
    but not
    
    .
    
    Throughout this paper we assume all formulas are rectified
    
    (losing no generality since every unrectified formula has a logically equivalent rectified form).
    
    
    Graphs
    An edge on a set  is a two-element subset of .
    
    A graph is a finite
    
    set  of vertices and a set  of edges on .
    
    Write  and  for the vertex and edge sets of a graph , and
    
     for {1mu,-2mu1mu}.
    
    The complement  of  is the graph ^-1mu𝖼 with vw^-1mu𝖼 if and only if vw-2mu.
    
    A graph  is (partially) coloured if it carries a partial equivalence relation  on  such that  only if ; each equivalence class is a colour.
    
    A graph is labelled in a set L if each vertex has an element of L associated with it, its label.
    
    A vertex renaming of  along a bijection
     ():→ is the graph 2mu1mu, with colouring and/or labelling inherited (,  if , and the label of  that of ).
    
    Following standard graph theory, we identify graphs modulo vertex renaming.
    
    Let 3mu and 3mu be graphs.
    
    A homomorphism:→ is a function  such that if
    -2mu∈-2mu then 1mu-2mu∈-2mu.
    
    Without loss of generality, assume
     (by renaming vertices if needed).
    
    The union is 
    and
    
    join is ;
    any colourings or labellings are inherited.
    
     is disconnected if =_1_2 for graphs _i, else connected,
    
    and coconnected if
    its complement
    
    is connected.
    
    The subgraph of
    
    induced by W is W  W for W the restriction of  to edges on W.
    
    A graph is -free if  is not an induced subgraph.
    
    A cograph is a -free graph, where
    ==.
    
    In
    
     the neighbourhood of  is ,
    
    a module
    is a set 
    such that = for all ,-2mu,
    
    and  is strong if
    
    every module  satisfies -3mu∩-1mu-2mu=-2mu∅, -1mu or .
    
    A directed graph is a set
    
     of vertices
    
    and a set
    
    -4mu-4mu of directed edges.
    
    A directed graph homomorphism:-2mu→-2mu is a function :-3mu→-3mu such that -2mu implies
    ()().
    
    
    
    § FOGRAPHS (FIRST-ORDER COGRAPHS)
    
    
    A cograph is logical if every vertex is labelled by a variable or atom, and it has at least one atom-labelled vertex.
    
    Write  for a -labelled vertex.
    
    
    The graph of a formula
    
     is the logical cograph defined
    inductively by:[ is a first-order extension of the propositional translation G of <cit.>.
    The latter is well-known in graph theory, as the function from a (prime-free) modular decomposition tree <cit.> or cotree <cit.> to a cograph, and is employed in logic and category theory,  <cit.>. See <ref> for details.]
    
    [                  = 
     for every atom; [  ;  ;  ][ ∀ x   x; ∃ x   x;     ];  ]
    
    
    For example,  and 
    have the same graph :
    
    
        =4mu(0ex1.7ex6mu6mu)        
           =4mu(0ex1.7ex6mu6mu)  =
        (1.3,.1) x y
         x px x py
    
    
    Vertices of  correspond to occurrences of atoms and quantifiers in :
    
    each occurence of an atom  in  becomes an α-labelled vertex, and each occurrence of a quantifier ∀ x or ∃ x becomes an x-labelled vertex.
    
    A literal is an atom-labelled vertex and a binder is a variable-labelled vertex.
    
    Thus  has two literals,
     and ,
    and two binders,
     and  (obtained from ∃ x and ∀ y).
    
    A module is proper if it has two or more vertices.
    
    The scope of a binder 
    is the smallest proper strong module containing .[Since, by definition, every logical cograph has a literal, the requisite strong module in the scope definition exists.],[To discern scope it is helpful to draw the modular decomposition tree <cit.>, , cotree <cit.>. See Lemma <ref>.]
    For example, in ,
    the scope of  is ,,,
    and
    the scope of  is ,,,, illustrated below by shading.
    
    -11(-2.5,0)
    (-3,0)[ scope;    of ]=linewidth=linecolor=,linecap=2,px-,-y,-py
      *[fillcolor=,linecolor=,radius=,framesep=0pt](,-)centre
      [angleA=-100,angleB=100,nodesep=0,linecap=2] pxpy[angleA=10,angleB=170,nodesep=0,linecap=2] y py[angleA=20,angleB=-110,nodesep=0,linecap=2] y px x y
     x px x py
    (5.7,0)
    (-3,0)[ scope;    of ]=linewidth=linecolor=,linecap=2-,x,px-,-y,-py
      *[fillcolor=,linecolor=,radius=,framesep=0pt](,-)centre x py y px
      [angleA=-100,angleB=100,nodesep=0,linecap=2] pxpy[angleA=10,angleB=170,nodesep=0,linecap=2] y py[angleA=20,angleB=-110,nodesep=0,linecap=2] y px[angleA=70,angleB=-160,nodesep=0,linecap=2] y px[angleA=-80,angleB=80,nodesep=0,linecap=2] x y
      [angleA=-10,angleB=-170,nodesep=0,linecap=2] x px x y
     x px x py
    A binder  is existential (resp. universal) in a logical cograph  if, for every other vertex  in the scope of , we have  (resp. ).[Since the scope of a binder is a proper strong module, every binder is either universal or existential (and not both).]
    In , for example,
     is existential
    and
     is universal
    
    (corresponding to
    ∃ x
    and
    ∀ y
    in the formula(s) generating ).
    
    An -binder is a binder with variable , which is legal if its scope contains at least one literal and no other -binder.
    
    
      A fograph or first-order cograph is a logical cograph whose binders are legal.
    
    For example,  above is a fograph, but
    
    x x
     y y
     p
     x y
    is not (since neither binder scope contains a literal),
    
    nor is
    
    a x
     b x
    px 
    (since each x-binder is in the other's scope).
    
    
      The graph  of every formula  is a fograph.
    
      By structural induction on . The base case with  an atom is immediate.ensure def ref correct
      For the induction step, note that all four operations defined in Def. <ref> preserve the property of being a fograph, since all formulas are rectified.[Naively applying  to an unrectified formula such as
    
    (∀-1mu x p-2mu x-1mu) (∀-1mu x (-2mu q-2mu x-2.5mu-2mu r-1mu x-1mu)-2mu)
    yields
    
    -1mu x-1mu p-2mu x-1mu x-1mu q-2mu x-1mu r-1.5mu x
    with all three literals bound ambiguously by both binders. Whence our assumption that every formula be in rectified form.]“place a formula” in footnote
    
    An -literal is one whose atom contains the variable .
    
    An -binder binds every -literal in its scope.
    
    In  above, for example,  binds  and  binds .
    
    An -binder is rectified if it is the only -binder and its scope contains every -literal.
    
    A fograph is rectified if its binders are rectified.[In <ref> we will observe that  (Def. <ref>) is a surjection onto rectified fographs (lem:graph-surj).]
    For example,
    
     above is rectified
    
    but  is not (since it has two x-binders), nor is 
    (since
    
     does not bind
    
    ).
    
    To rectify an unrectified  in a fograph  is to
    change its label to a variable  which is fresh (, not in any label of )
    
    and
    
    substitute  for x in the
    label of every literal
    
    bound by .
    
    A rectified form is any result of rectifying binders until reaching a rectified fograph.
    
    For example,  xx  has the rectified form  yz .
    
    This is analogous to the unrectified formula
     having the rectified form
    
    .
    
    The binding graph of a fograph  is the
    
    directed graph
    .
    
    For example, the binding graph of  above is
    
    -1.7(-1.5,0)=(1.3,0) x px y py
    
    § SKEW BIFIBRATIONS
    
    
    A directed graph homomorphism
    
    :→ is a fibration<cit.> if
    for all
     and -1mu() there exists a unique  with -2mu and () =.
    
    This definition is illustrated below-left.
    
    
    [nodesep=2pt,labelsep=2pt](0,-.35)(0,2)
      (-5,0)(-,1.55)liftw∃1mu!1mu(-,0) w (,1.55) v v(,0)fv(v)
          [arrows=->]wfv
          [arrows=->]liftwv
     
          liftwwvfv(0,0)(-,1.55)liftw∃1mu!1mu(-,0) w (,1.55) v v(,0)fv(v)
          wfv
          liftwv
     
          liftwwvfv(5,0)(,1.55)vv
          (,0)fvf(v)(-,.3)fwhatf( w)(-,1.8)what∃2mu(-,-.35)ww
          vwhat
          fvfwhatfvw
     
          vfvwhatfwhat
    
    Similarly, an undirected graph homomorphism :→ is a fibration
    if for all
     and
    3mu()∈ there exists a unique  with 2mu and () =.
    
    This definition is illustrated above-centre.[An undirected graph fibration is a special case of a topological fibration <cit.>, by viewing every edge as a copy of the unit interval.]
    An undirected graph homomorphism :→ is a skew fibration<cit.>
    if for all
     and
    3mu-.3mu() there exists
     with
    2.5mu∈ and
    f( w)2mu w∉.
    
    This definition is illustrated above-right.
    
    Since () implies
    f( w)2mu w∉,
    skew fibrations generalize fibrations.
    
    A graph homomorphism :→ between fographs preserves labels if
    
    for every vertex  the
    label of  in  equals the label of () in ,
    
    and preserves existentials if
    for every existential binder  in  the vertex () is an existential binder in .
    
    
    A skew bifibration-2mu:-2mu-2mu→-2mu between fographs is a label- and existential-preserving graph  such that
    
      * :→ is a skew fibration
      
      * :→ is a fibration.
    
    We refer to :→ as the binding fibration.
    
    For example, a skew bifibration is shown in Fig. <ref>, with its binding fibration.
    
    The skeleton of a skew bifibration is the result of dropping labels from its source.
    
    Fig. <ref> shows an example.
    
    We identify a skew bifibration with its skeleton.
    
    No information is lost since the source labels can be lifted from the target (because skew bifibrations preserve labels, by definition).[We need the explicit preservation of existentials in the definition of skew bifibration since that property does not follow from the other conditions.
    For example, the unique label-preserving function from
    ∃ x2mu p
    =
     x x p p x p
    to
    (∀ x2mu q) p
    =
     x x q q p p q p[nodesep=0pt,angleA=35,angleB=150]x p
    satisfies all the conditions of being a skew bifibration except existential preservation (since it maps an existential binder to a universal binder).]
    
    § FONETS (FIRST-ORDER NETS)
    
    
    Two atoms are pre-dual if they have dual predicate symbols (  and y fa) and two literals are pre-dual if their atoms are pre-dual.
    
    
    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-labelled or in a link.
    
    Fig. <ref>p q so validates cp?
    shows a linked fograph 
    with two links,
    
    and
    .
    
    Let  be a linked fograph.
    ,
    
    assume
    
     is rectified (by rectifying binders as needed).
    
    A dualizer for  is
    
    a function 
    assigning to each existential binder variable x a term
    (x)
    such that
    
    for every link {2mu,2mu}, the atoms
     and  are dual, where  denotes the result of substituting (x) for x throughout 
    (simultaneously for each x).
    
    
    For example,
    
    is a dualizer[In the context of a function we write a b for the ordered pair ⟨ a,b⟩.] for
    
     (Fig. <ref>) since
    = is dual to , and = is dual to ; this is the unique dualizer for .
    
    A dependencybond cord tether linkage link tie
    of 
    is an existential binder  and a universal binder  such that every dualizer
    
    for 
    assigns to x a term containing y.[In <ref> we show that all dependencies can be constructed in polynomial time, despite quantification over every dualizer.]link to p-time
    For example, {2mu,2mu} is a dependency of  (Fig. <ref>)
    since the unique dualizer  assigns  to y.
    
    A leap is a dependency or link.
    
    The leap graph is the graph (,) where  comprises all leaps of .
    
    See Fig. <ref> for an example.
    
    A graph  is a matching if  is non-empty and
    
    for all -3mu∈-2mu there is a unique -4mu∈-2mu with -3mu∈-2mu.
    
    A set Winduces a bimatching in a linked fograph  if W induces
    a matching in  and induces a matching in .
    
    
      A fonet or first-order net is a
    
     linked fograph which has a dualizer but no induced bimatching.
    
    
    See Fig. <ref> for an example of a fonet.
    
    The minimal fonet is 1 (an uncoloured 1-labelled vertex).[A fonet can be viewed as a graph-theoretic abstraction and generalization of a unification net <cit.>. Upon forgetting vertex labels,
    propositional fonets correspond to nicely coloured cographs <cit.>,
    which are in bijection with certain R&B cographs <cit.>.
    See <ref> for details.]
    
    § COMBINATORIAL PROOFS
    
      A combinatorial proof of a fograph is a skew bifibration
      from a fonet.
    
      A combinatorial proof of a formula  is a combinatorial proof of its graph .
    
    
    For examples, see <ref>.
    
    
      A formula is valid if it has a combinatorial proof.
    
    
      Section <ref>.
    
    
      Every valid formula has a combinatorial proof.
    
    
      Section <ref>.
    
    Combining the two theorems above, we obtain the main theorem of this paper:
    
    
      A formula
      of first-order logic
      is valid if and only if it has a combinatorial proof.
    
    
    § PROPOSITIONAL COMBINATORIAL PROOFS WITHOUT LABELS
    
    A proposition is a formula with no quantifiers or terms,  , and a proposition is simple if it has no logical constant (1 or 0).
    
    This section provides an alternative representation of fographs and combinatorial proofs in the simple propositional case, without labels (variables and atoms).
    
    An illustrative example is shown in
    
    
    Fig. <ref>.
    
    The left side
    
    shows a standard combinatorial proof (Def. <ref>) of Peirce's law =.
    
    The right side shows the label-free form, called a homogeneous combinatorial proof, defined below.
    
    The source colouring and target labels (, p and q) have disappeared,
    
    replaced by duality edges, shown dashed and curved.
    
    The adjective homogeneous reflects the common type of the source and target (both cographs with additional duality edges), in contrast to a standard combinatorial proof skeleton which is heterogeneous (the source is coloured, while the target is labelled).
    
    
    
     §.§ Dualizing graphs
    
    
    A graph is triangle-free if it is -free, where ==.
    
    
    A dualizing graph is a non-empty cograph  equipped with a second set  of undirected edges on , called dualities, such that  is a triangle-free cograph.
    
    
    Four examples of dualizing graphs are shown in the bottom row of
    
    Fig. <ref>.
    
    Dualizing graphs generalize R&B-cographs <cit.>.[An R&B-cograph is a dualizing graph such that every vertex is in a unique duality.]
    
    The dualizing graph  of a simple proposition  is the dualizing graph  with
    
    
      * =occurrences of predicate symbols in,
    
    
      *  if and only if
    
    the smallest subformula of 
    containing both  and  is
    
    a conjunction (, of the form )
    
    
      *  if and only if  and  have dual predicate symbols (, p and ).
    
    
    For example, for each simple proposition  in the top row of Fig. <ref>,
    the bottom row shows the corresponding dualizing graph .
    
    For comparison, the fograph  is in the middle row.
    
     is a well-defined dualizing graph for every simple proposition .[We will observe in <ref> that  is a surjection from simple propositions onto dualizing graphs (lem:prop-surj).]
    
    Let =.
    
    We must show
     and
     are P_4-free and
    
     is -free.
    
    Suppose
    _1,-2mu_2,-2mu_3,-2mu_4_1_2,-1mu_2_3,-1mu_3_4
    is an induced subgraph of
    .
    
    Since _1_2 there exist subformulas
    _1 and _2 of  containing _1 and _2, respectively, with
    _1_2 a subformula of .
    
    Necessarily
    _3 is in _1, otherwise (since  is a syntactic tree) _1_3 (a contradiction), and similarly
    _4 is in _2, otherwise _2_4 (a contradiction).
    
    But then _1_4, a contradiction.
    
    Suppose
    _1,-2mu_2,-2mu_3,-2mu_4_1_2,-1mu_2_3,-1mu_3_4
    is an induced subgraph of
    ,
    where v_i is an occurrence of the nullary predicate symbol p_i.
    
    By definition of , we have _1=p_2, _2=p_3 and _3=p_4.
    
    Thus p_3=p_1, hence p_4=_1, so _1_4∈, a contradiction.
    
    Suppose
    _1,-2mu_2,-2mu_3_1_2,-1mu_2_3,-1mu_3_1
    is an induced subgraph of ,
    where v_i is an occurrence of the nullary predicate symbol p_i.
    
    By definition of , we have _1=p_2, _2=p_3 and _3=p_1.
    
    Thus p_3=_2=_1=p_1, contradicting _3=p_1.
    
    
    
     §.§ Dualizing nets
    
    
    A set W⊆induces a bimatching in
    a dualizing graph
     if W induces a matching
    
    in 
    and induces a matching in
    .
    
    
    A dualizing net is a dualizing graph with no induced bimatching,
    such that  is a matching.
    
    For example,
    
     a b  c  d  a b [angleA=30,angleB=150] a c [angleA=-30,angleB=-150] b d 
    is a dualizing net, while
    
     a b  c  d  a b  c d  [angleA=30,angleB=150] a c [angleA=-30,angleB=-150] b d 
    and
    
     a b  c  d  a b [angleA=25,angleB=155] a d [angleA=-30,angleB=-150] b d 
    are not.
    
    The third dualizing graph in the bottom row of Fig <ref> is a dualizing net, while the other three
    
    are not.
    
    Dualizing nets
    are in bijection with
    
    even-length alternating elementary acyclic R&B cographs <cit.>.
    
    
    
     §.§ Propositional homogeneous combinatorial proofs
    
    
    A skew fibration-0mu:-1mu-1mu→-1mu
    of dualizing graphs is a skew fibration
    :→
    such that
    
    :→ is a homomorphism.
    
    
      A homogeneous combinatorial proof of a dualizing graph is a skew fibration
      from a dualizing net.
    
      A homogeneous combinatorial proof of a simple proposition  is a homogeneous combinatorial proof of its dualizing graph .
    
    For example,
    
    a homogeneous combinatorial proof of Peirce's law = is shown on the right of Fig <ref>.
    
    
    
     §.§ Propositional homogeneous soundness and completeness
    
    A simple proposition is valid if and only if it has a homogeneous combinatorial proof.
    
    
    A corollary of Theorem <ref>, detailed in  <ref>.
    
    
    § MONADIC COMBINATORIAL PROOFS WITHOUT LABELS
    
    
    A formula is monadic if its predicate symbols are unary and it has no function symbols or logical constants, , .
    
    This section extends homogeneous combinatorial proofs to the monadic case.
    
    Fig. <ref> shows an illustrative example:
    on the left is the combinatorial proof of  presented in the Introduction,
    and on the right is the corresponding homogeneous combinatorial proof, to be defined below.
    
    For technical convenience throughout this section we assume every monadic formula is closed, , has no free variables. This loses no generality because a formula  with free variables x_1,…,x_n is valid if and only if its closure ∀ x_1…∀ x_n2mu is valid.
    
    Given a directed edge e=,  is the source of e,  is the target of e, and  and  are ine.
    
    
    A pre-monadic graph or pre-mograph is a dualizing graph
     equipped with a non-empty set
     of directed edges on
    ,
    called bindings, such that
    if a vertex  is the target of a binding then
     is in no other binding.[In other words, if , then (1)
     for all vertices , and (2)
    
    implies =.]
    
    An example of a pre-mograph is shown on the right of Fig. <ref>, with two dualities (dashed and curved) and three bindings (directed and curved).
    
    A vertex in a pre-mograph  is a literal if it is the target of a binding, otherwise a binder.
    
    If  we say that
    binds.[Note that, by the condition in the definition of pre-mograph,
     must be a binder.]
    The scope of a binder  in 
    is the smallest proper strong module of  containing .
    
    
    A mograph is a pre-mograph such that
    
    no binder is in a duality,
    
    every binder has non-empty scope,
    
    and
     only if
     is in the scope of .
    
    
    For example, the pre-mograph on the right of Fig. <ref> is a mograph.
    
    
    The mograph of a closed monadic formula  is the mograph defined by:
    
    
    
      * =occurrences of atoms and quantifiers in,
    
    
      *  if and only if either
      
      *  the smallest subformula containing both  and  is
    
    a conjunction (, of the form )
    
      
      *  is an existential quantifier,  is in its scope, and .
    
      
    
      *  if and only if  and  are atoms with dual predicate symbols (,  and ), and
    
    
      *  if and only if  is a quantifier,  is an atom, and  binds .
    
    
    For example, in Figure <ref>, the closed monadic formula = on the left has the mograph  on the right.
    
     is a well-defined mograph for every closed monadic formula .[We will observe in <ref> that  is a surjection from closed monadic formulas onto mographs (lem:surj-closed-monadic-formulas-to-mographs).]
    
    Let =.
    
    Since every atom-occurrence in  has a single variable, each literal is the target of at most one binding in , and since no atom-occurrence binds another atom-occurrence,  satisfies the condition on bindings in the definition of pre-mograph (Def. <ref>).
    
    By reasoning as in the proof of lem:dualizing-graph-of-prop-well-defined,  is -free and -free.
    
    By definition of , no binder is in a duality.
    
    It remains to show that  is a cograph, every binder has non-empty scope, and
     only if  is in the scope of .
    
    We proceed by induction on the structure of .
    
    Base case: = for some p and x, so  is a single vertex, hence a mograph.
    
    Induction case: =_1_2 for .
    
    By induction hypothesis _i=_i is a mograph (i=1,2).
    
    By definition of , we have
    =_1_2
    or
    =_1_2,
    
    thus  is a cograph since each _i is a cograph.
    
    The scope of a binder  in  is at least the scope of  in the _i containing ,
    thus the scope of  in  is non-empty and contains every literal bound by , since _i is a mograph.
    
    Induction case: =-1mu x2mu for .
    
    By induction hypothesis, = is a mograph.
    
    By definition of  we have
    = or
    = for a vertex
    
    (the initial occurrence of -1mu x in ),
    
    thus  is a cograph since  is a cograph.
    
    The scope of  in  comprises every literal, and is therefore non-empty and contains every literal bound by .
    
    The scope of any other binder  in  is equal the scope of  in ,
    so is non-empty and contains every literal bound by , since  is a mograph.
    
    
    
     §.§ Monets
    
    
    A mograph is linked if every literal is in a unique duality.
    
    An example of a linked mograph is shown in Fig. <ref> (left).
    
    
    Let  be a linked mograph.
    
    Its binder equivalence is the equivalence relation on binders generated by
    _1_2 if there exist literals _1 and _2 with
    _1_1,_2_2
    and _1_2.
    
    
    Thus
    
    _1_2
    if and only if there exists a binding/duality pattern of the form
    
    
    [               1       2               3       4         -1.2ex…               5       6;     b_1                       u                       v               w                     c_2 ]u2u3v4w5c6nodesepA=0ptb1 1 2
     3 4
     5 6
    
    
    Let  be a linked mograph.
    
    A binder  in  is existential (resp. universal) if, for every other vertex  in the scope of , we have
     (resp. ).[Since the scope of a binder is a proper strong module, every binder is either universal or existential (and not both).]
    A conflict in  is a pair b,c of distinct universal binders b and c such that b c.
    
    
    A mograph is consistent if it has no conflict.
    
    A dependency of  is a pair b,c of binders with b c, b existential, and c universal.
    
    A leap is a dependency or duality.
    
    
    The leap graph of a linked mograph  is
    
     for  the set of leaps of .
    
    An example of a leap graph is shown in Fig. <ref> (right).
    
    A set of vertices W⊆induces a bimatching in a linked mograph
     if W induces a matching in
    
    
    and induces a matching in
    .
    
    
    A monet (monadic net) is a consistent linked mograph with no induced bimatching.
    
    
    An example of a monet is shown in
    Fig. <ref>.
    
    
    
     §.§ Monadic homogeneous combinatorial proofs
    
    Let  and  be mographs.
    
    A function :→preserves existentials
    if
    for every existential binder  in 
    the vertex () is an existential binder in .
    
    
    A skew bifibration:→ between mographs is
    an existential-preserving skew fibration
    
    :→
    such that
    
    
      * :→
    is a homomorphism and
    
    
      * :→
    is a fibration.
    
    
    An example of a skew bifibration between mographs is shown on the right of Fig. <ref>.
    
    
    A homogeneous combinatorial proof of a mograph  is a skew bifibration  from a monet .
    A homogeneous combinatorial proof of a closed monadic formula  is a homogeneous combinatorial proof of its mograph .[Although, for technical convenience, throughout this paper we have assumed (without loss of generality) that every formula is rectified, this definition of homogeneous combinatorial proof also works directly for non-rectified closed monadic formulas, without the need to first transform to rectified form.
    
    This is because  is agnostic to the choice of bound variables, since mographs do not contain any variables.
    
    For example,
    (∀ x1mu px)
    ∨
    (∀ x1mu qx)
    
    =
    
    (∀ x1mu px)
    ∨
    (∀ y1mu qy)
    
    =
      x pxxxqxnodesepA=1pt,nodesepB=.5pt[angleA=30,angleB=155]xpx[angleA=30,angleB=155]xxqx
    and
    ∀ x2mu∃ x2mu px
    =
    ∀ x2mu∃ y2mu py
    =
      x xxpxxxpxnodesepA=1.5pt,nodesepB=1pt[angleA=35,angleB=150]xxpx.]
    A homogenous combinatorial proof of  is shown in Fig <ref> (right).
    
    
    
     §.§ Monadic homogeneous soundness and completeness
    
    A closed monadic formula is valid if and only if it has a homogeneous combinatorial proof.
    
    
    A corollary of Theorem <ref>, detailed in  <ref>.ref
    
    § MODAL COMBINATORIAL PROOFS
    
    
    A modal formula is
    
    generated from
    
    the modal operators (necessity) and  (possibility) instead of quantifiers and has all predicate symbols nullary,
    
    .
    
    Every modal formula abbreviates a standard first-order one <cit.>:
    
    replace every  by ∀ x,
    
     by ∃ x, and
    
    predicate symbol
    p by px. For example,  abbreviates ,
    or
    
     in rectified form.
    
    
    A modal combinatorial proof of a modal formula
     is a standard combinatorial proof (Definition <ref>) of the first-order formula abbreviated by .
    
    For example, a modal combinatorial proof of  is shown below-left, in condensed form.
    
    
    -.3.85(-3,0)(3,0)
    
    It abbreviates the first-order combinatorial proof
    
    above-right (copied from the Introduction).
    
    
      A modal formula is valid in S5 modal logic if and only if it has a modal combinatorial proof.
    
    
      By Theorem 3.2 of <cit.>, a modal formula is valid in S5 if and only if the first-order formula it abbreviates is valid in first-order logic.
    
    Thus the result follows from Theorem <ref>.
    
    
     §.§ Modal combinatorial proofs without labels
    
    
    A modal formula is closed if
    
    every predicate symbol occurrence is bound by a modal operator ( but not )
    and simple if it has no logical constant (1 or 0).
    
    
    The mograph  of a simple closed modal formula  is the mograph  defined by
    
    
    
      * =occurrences of predicate symbols and modal operators in,
    
    
      *  if and only if either
      
      *  the smallest subformula containing both  and  is
    
    a conjunction (, of the form )
    
      
      *  is a  with  is in its scope and v w.
    
      
    
      *  if and only if  and  are dual predicate symbols, and
    
    
      *  if and only if  is a modal operator,  is a predicate symbol, and  binds .
    
    
    
    For example,
    
    
    
    =
    (0,1.3ex)
    
    
    
    A homogeneous combinatorial proof of a closed modal formula 
    is a homogeneous combinatorial proof of its mograph .
    
    For example, a homogeneous combinatorial proof of  is shown on the right of Fig. <ref>.
    
    
    A closed modal formula is valid in S5 modal logic if and only if it has a homogeneous combinatorial proof.
    
    
    Since = for  the first-order formula encoded by , the result is a corollary of Theorem <ref>.
    
    
    § PROOF OF THE SOUNDNESS THEOREM
    
    
    In this section we prove the Soundness Theorem, Theorem <ref>.
    
    The function  (Def. <ref>) is a surjection from formulas onto .[Dropping the assumption that every formula is rectified leads to a surjection onto all fographs: see lem:xgraph-surj.]
    Two formulas have the same graph if and only if they are equal modulo[Recall that, without loss of generality, we assume all formulas are rectified. Thus these equations do not include cases such as
    px∧∃ x2mu qx
    =
    ∃ x(px∧2mu qx), an equality between formulas which are not logically equivalent.]
      
        ∧()     ()∧       ∃ x2mu∃ y2mu    ∃ y2mu∃ x2mu       ∧∃ x2mu   ∃ x2mu()
        
            
        
                  ∨()     ()∨   ∀ x2mu∀ y2mu    ∀ y2mu∀ x2mu   ∨∀ x2mu   ∀ x2mu()
    
    
    
      A routine induction.elaborate in appendix
    
    Let  be a rectified fograph. Using the above Lemma,
    
    choose a formula  such that .
    
    Define  as valid if  is valid.
    
    This is well-defined with respect to choice of  since
    every equality in Lemma <ref> is a logical equivalence.
    
    Define a coloured fograph as valid if its underlying uncoloured fograph is valid.
    
    Write χ to assert that a formula or fograph χ is valid,
    
    and  for the result of substituting a term  for all occurrences of the variable  in a formula ,
    where, without loss of generality (by renaming bound variables in  as needed), no variable in  is a bound variable of <cit.>.
    
    
      Let ,  and  be formulas.
    
      
      *  if and only if ( and ).
      
      *  if ( or ).
      
      * () implies ()∨().
    
      
      * ∀ x2mu if and only if .
      
      * x t implies ∃ x2mu.
      
      * ∨ x t implies ∨∃ x2mu.
    
      
      * () implies ().
      
    <ref>–<ref> are standard inferences and properties of validity in first-order classical logic. See <cit.> and <cit.>, for example. Property <ref> follows from <ref> and <ref>.
    
    
     §.§ Soundness of fonets
    
    
    In this section we prove that fonets are sound, , every fonet is valid (Lemma <ref> below).
    
    Let  be a fograph.
    A set  is well-founded if  contains a binder only if  contains a literal.
    
    
    A portion of a rectified fograph  is a set  such that  and   are well-founded, and  is closed under adjacency and binding:
    if  or -3mu,
    then  if and only if .
    
    A variable x in a fograph  is
    
    bound if  contains an x-binder,
    
    and free if  contains an x-literal but no x-binder.
    
    Two fographs are
    
    independent
    if
    
    any variable in both is free in both.
    
    
    
      §.§.§ Fusion
    
    Let  and  be independent rectified fographs with respective portions  and -2mu.
    
    The fusion of  and -1mu at  and -2mu is the union -2mu-2mu together with edges between every vertex in  and every vertex in -2mu.
    
    
    For example, if =2mu x x 12muppx x ppx7mu2mu,
    
    =4mu6mu6mu2mu,
    
    =
    and
    
    =1mu,4mu,
    
    then
    
    the fusion of  and  at  and  is
    
    x x 12muppx x ppx7mu py12mu
     q qpyq6muqq[nodesep=0ex,angleA=25,angleB=145]pyqq6mu2mu.
    
    Colourings are inherited during fusion, since they are inherited during graph union .
    
    For example, if =2mu x x 12mu x v 7mu2mu,
    
    =4muq2mu q6muqq2mu 6mu2mu,
    
    =
    and
    
    =q2mu q1mu,4muqq2mu,
    
    then
    
    the fusion of  and  at  and  is
    
    x x 12mu x v 7mu py12mu
    qpyq.5mu q6muqq[nodesep=0ex,angleA=25,angleB=145]pyqq1mu 6mu2mu.
    
    Write W for the subgraph of  induced by W.
    
    
      Every fusion of valid rectified fographs is valid.
    
    
      Let  be the fusion of valid rectified fographs  and  at portions  and .
    
      We consider four cases.
    
      
      *  or  is empty. Without loss generality, we may assume both are empty, since with one portion empty the fusion operation no longer depends on the other.
    
    Thus = for rectified fographs  and , so by Lemma <ref> there exist formulas  and  with  and .
    
    Since  and  are independent, =. Since  and  we have  and , hence  by Lemma <ref>.<ref>. Thus .
    
      
      *  and =.  Thus =.
    As in the previous case we have valid formulas  and  with  and . Thus  since  by Lemma <ref>.<ref> and =.
    
    
      *  or , and the previous two cases do not hold. Without loss of generality assume , so ∅.
    
    Let -1mu≠∅.
    
    Thus =().
    
    By Lemma <ref> there exist formulas ^*,  and ' with ^*,
     and .
    
    Since  we have , and since  and ^*=, we have ^*.
    
    Thus (^*) by Lemma <ref>.<ref>, so
    
    ^*() by Lemma <ref>.<ref>, hence  since =^*().
    
    
      *  Otherwise ∅≠ and
    ∅≠-1mu≠.
    
    Let =-1mu≠∅ and
    =-1mu≠∅.
    
    Thus the rectified fograph  is ().
    
    By Lemma <ref> there exist formulas ^*, ^*,  and  with ^*=,
    ^*=,
    =, and
    =.
    
    Since  and ^*= we have ^*, and
    since  and ^*= we have ^*.
    
    
    Thus , so  since =.
    -4ex
    
    
      Every fusion of two rectified fonets is a rectified fonet.
    
    
      Let  be a fusion of rectified fonets  and .
    
      Since each portion is closed under adjacency,  is a union of cographs,
    
      hence is a cograph.
    
      Every binder scope contains a literal, by inheritance from  and .
    
      Since  and  are rectified and (by the constraint on the definition of fusion) independent,
      and no links traverse between the two in ,
    
      every union of dualizers for  and  is a dualizer for , and vice versa.
    
      Thus the set of dependencies of  is the union of those of  and , so any W inducing a bimatching in  would induce a bimatching in  or .
    
    Because  and  are independent,  is rectified.
    
    
      §.§.§ Universal quantification
    
    Let  be a rectified fograph with no -binder.
    The universal quantification of  by x
    is -1mu-1mu.
    
    
    
      Every universal quantification of a valid rectified fograph is valid.
    
    
      Let = be the universal quantification of a valid rectified fograph  by x. By Lemma <ref> there exists a formula  such that , and  since . Thus ∀ x2mu=, hence  since ∀ x2mu if and only if , by Lemma <ref>.<ref>.
    
    If  is a coloured rectified fograph, in the universal quantification  we assume that the colouring of  is inherited, while  remains uncoloured.
    
    
      Every universal quantification of a rectified fonet is a rectified fonet.
    
    
      Let  be the universal quantification -1mu-1mu.
    
      Dualizers for  are dualizers for , and vice versa, since if x occurs in , it has merely transitioned from free to bound.
    
      The leap graph of  is that of  together with additional dependencies involving .
    
      Since  is in no edge, any W inducing a bimatching in  would induce a bimatching in .
    
    
      §.§.§ Existential quantification
    
    Let  be a rectified fograph without the variable x, let  be a non-empty portion of , and let  be a set of occurrences of a term t in labels of literals in , such that t contains no bound variable of .
    
    The existential quantification of  by x at  in  is -1mu-1mu t ω x together with an edge between  and each vertex in , where t ω x is the result of substituting x for every occurrence of t in .
    
    For example, if =2mup  g y7mu gy2mu,
    
    =p  g y
    and
    
     is the occurrence of the term gy in p  g y,
    
    the existential quantification of  by x at  is
    
    2mu x x 12mu v p  x x v 7mu g y2mu,
    
    while if  is empty
    
    the existential quantification becomes
    
    2mu x x 12mu v p  g y x v 7mu g y2mu.
    
    If =p  g y, gy and  comprises both occurrences of the term gy in , then the existential quantification is
    2mu x x 12mu v x v 7mu w [nodesep=0ex,angleA=25,angleB=145] x w2mu
    
      Every existential quantification of a valid rectified fograph is valid.
    
    
      Let  be the existential quantification of a valid rectified fograph  by x at a set  of occurrences of the term t in the non-empty portion .
    
    Thus = t ω x plus edges from  to every vertex in .
    
    We consider two cases.
    
    
      * 
    Suppose .
    
    Thus = t ω x.
    
    By Lemma <ref> there exists a formula  such that = t ω x.
    
    Therefore
    = t ω x==∃ x2mu.
    
    Since x does not occur in  we have x t=, and x t since .
    
    By Lemma <ref>.<ref> we have ∃ x2mu since
    x t, thus .
    
    
      * 
      Otherwise ∅≠≠.
    
      Let =-1mu≠∅.
    
      Since  is a portion, it is well-founded and closed under adjacency and binding,
    
      t ω x= t ω x t ω x with  and t ω x both rectified fographs, and t ω x= since ω does not intersect . Thus t ω x= t ω x.
    
      By Lemma <ref> there exist formulas ^* and  with ^*= and = t ω x.
    
      Thus
    
      
        =  t ω x = ^*∃ x2mu = ^*∃ x2mu
    
      Since = t ω x and x does not occur in  we have x t=. Thus
      
        =  = ^* x t = ^* x t
    
      Since  we have ^* x t,
      so by  Lemma <ref>.<ref>
      we have ^*∃ x2mu,
      hence .
    
    
    -4ex
    When quantifying a coloured rectified fograph existentially, the colouring is inherited, while the added binder remains uncoloured.
    
    For example, if =2mup  g y7mu gy2mu,
    
    =p  g y
    and
    
     is the occurrence of
    
    y in p  g y,
    
    the existential quantification of  by x at  in  is
    
    2mu x x 12mup  g x x v 7mu g y2mu.
    
    In the remainder of this section (<ref>) we prove that every existential quantification of a rectified fonet is a rectified fonet (Lemma <ref>).
    
    Let  be a linked rectified fograph.
    
    An existential (resp. universal) variable of  is one labelling an existential (resp. universal) binder in .
    
    An output of a function is any element of its image.
    
    A stem of a dualizer  for  is a variable in an output of  but not in .
    
    For example, if = and  and  are variables,
    
    the dualizer  has one stem ,
    x f, y f has two stems  and ,
    x f z, y f z has one stem ,
    and  has no stem.
    
    A dualizer generalizes a dualizer  if  yields  by substituting terms for stems, , there exists a function  from the stems of  to terms such that (x)=(x) for every existential variable x of , where  denotes the result of substituting () for  in , simultaneously for each stem  of .
    
    For example, if = and  is a variable, the dualizer -1mu= generalizes -2mu= x f z a, y f z a via  since (x)=(y)==fza.
    
    A dualizer  is most general if it generalizes every other dualizer.
    
    For example,
    
     is a most general dualizer for  but
    
    x f , y f and
     are not.
    
    A linked rectified cograph is dualizable if it has a dualizer.
    
    
      Every dualizable linked rectified fograph has a most general dualizer.
    
    
      Let  be the dualizable linked rectified fograph.
    
      Every dualizer for  is, by definition,
      a unifier for the unification problem 
      (binary relation on terms) <cit.>
      defined by t_i t'_i for each link
      p t_1… t_n, t'_1… t'_n and 1≤ i≤ n, solved for the existential variables.
    
      Let  be a most general unifier of <cit.>.
    
      By renaming variables as needed, we may assume that no output of  contains an existential variable.
    
      Define  as the restriction of  to existential variables.
    
      Since  is a most general unifier,  is a most general dualizer.
    
    Let  be a linked rectified fograph with dualizer .
    
    A pair  is a dependency of  if
     is existential,  is universal, and (x) contains y.
    
    
      Let  be a linked rectified fograph with a most general dualizer . A pair  is a dependency of  if and only if  is a dependency of .
    
    
      Since  is most general, for any dualizer  every dependency of  is a dependency of .
    
      By definition,  is a dependency of  if and only if it is a dependency of every dualizer for .
    
      Thus  is a dependency of  if and only if it is a dependency of .
    
    
      Every existential quantification of a rectified fonet is a rectified fonet.
    
    
    Let  be the existential quantification of  by x at  in , where  is a set of occurrences of the term t in labels of literals in .
    
    Since  is closed under adjacency,  is a cograph and every binder scope in  contains a literal.
    
    In the following two paragraphs we will show that the dependencies of  and  coincide.
    
    For any dualizer  for , the function
    
    =∪ x t is a dualizer for , since the links of  are those of  but for some occurrences of t becoming x.
    
    The dependencies of  in  are the same as those of  in ,
    since t contains no binder variable of .
    
    Every dependency of  is a dependency of :
    a dependency of  is (by definition) a dependency of every dualizer of ,
    hence a dependency of  for every dualizer  for ,
    thus a dependency of .
    
    Conversely, to show that every dependency of  is a dependency of ,
    we take a most general dualizer  for  and construct a dualizer
     for  with the same dependencies as ;
    since a dependency of  is (by definition) a dependency of every dualizer of ,
    it is a dependency of  in ,
    hence a dependency of  in ,
    and therefore a dependency of  by lem:mgd-deps (since  is most general).
    
    Let  be a most general dualizer for .
    By the argument in the previous paragraph, =∪ x t is a dualizer for .
    
    Since  is most general for ,
    there exists a function  from the stems of  to terms such that
    t=(x)=(x).
    Let  be the restriction of  to stems appearing in (x).
    
    Define  by (y)=(y), for every existential variable y of .
    
    In particular, (x)=t.
    The function  is a dualizer for  (since it is  with terms substituted for stems), and has the same dependencies as  because (x)=t so (z) is a sub-term of t for every stem z of  in (x), and t contains no bound variable of , hence no bound variable of .
    
    Define  as the restriction of  to the existential variables of 
    (thus =∪ x t).
    
    The function  is a dualizer for  since for every link p t_1… t_n, u_1… u_n in  we have t_i u_i, because for the corresponding link p t'_1… t'_n, u'_1… u'_n in  we have t'_i=u'_i with
    t_i=t'_i x t
    and
    u_i=u'_i x t, and by construction (x)=t.
    
    The dualizer  is a restriction of , which has the same dependencies as , thus  has the same dependencies as .
    
    Thus, by the argument at the start of this paragraph, every dependency of  is a dependency of .
    
    Since the dependencies of  and  coincide, the leap graphs  and  are identical but for an extra vertex  in the latter which is not in any leap. Thus induced bimatchings of  and  coincide, so  is a fonet because  is a fonet.
    
    
    
      §.§.§ Soundness of fonets
    
    
    An axiom is a coloured rectified fograph comprising two dual literals of the same colour ( ) or a single (uncoloured) 1-literal.
    
    
      Every coloured rectified fograph constructed from axioms by fusion and quantification is a rectified fonet.
    
    
      Every axiom is a rectified fonet, and fusion and quantification preserve the property of being a rectified fonet, by Lemmas <ref>, <ref>, and <ref>.
    
    A fonet is universal if it has a binder in no edge (necessarily a universal binder).
    
    
      Every universal rectified fonet is a universal quantification of a rectified fonet.
    
    
    
    Let  be a universal rectified fonet, with (universal) binder  in no edge.
    
    The result ^- of deleting  from  is a fonet,
    since ^- inherits all dualizers from  (because x goes from being universal to being free) and if W induces a bimatching in ^- then W induces a bimatching in .
    
    Since ^- is an induced subgraph of a rectified fograph, ^- is rectified.
    
    Since =^-, the rectified fonet  is the universal quantification of the rectified fonet ^- by x.
    
    
      Every fonet with no edge and no binder is a union λ_1…λ_n of axioms λ_i (n 1).
    
    
    
    Since  has no edges, it has no existential binders, hence the empty dualizer.
    
    Thus every link in  has literals with dual atoms, and every literal that is not in a link is 1-labelled.
    
    Since  has no edges, it is the union of axioms.
    
    
    Let  be a rectified fonet with underlying uncoloured fograph
    _1
    1mu1mu(_1-2mu-2mu_2)
    1mu1mu_2
    for each _i a fograph and each _j empty or a fograph.
    Suppose no leap of  is between _1∪_1 and _2∪_2.
    Then  is a fusion of rectified fonets.
    
    
    
      Since  is a fograph and no leap goes between _1∪_1 and _2∪_2, the graphs
     and
    
    are well-defined fonets upon inheriting colouring from
    
    by restriction. Thus
     is a fusion of rectified fonets
    _1_1 and _2_2 at portions
    _1 and _2.
    
    
    Let  be a rectified fonet with underlying uncoloured fograph
    
    _11mu1mu()1mu1mu_2 for  a fograph and each _i empty or a fograph.
    
    Suppose no leap of  is between _1∪ and ∪_2.
    
    Then the binder  is in no leap of .
    
    
    In this proof leap supposition refers to the supposition on leaps in the Lemma statement.
    
      Suppose for a contradiction that , is a leap, hence dependency, of . By the leap supposition, the universal binder  is in _1.
    
      Let  be a most general dualizer for , which exists by lem:mgd. Since , is a dependency, the term () contains y, by Lemma <ref>.
    
      There must be a link v,w such that the atom label of the literal v contains x, otherwise ()=z for a stem variable z not occurring in , so () would not contain y.
    
      Since  is rectified, the literal v must be in the scope of , thus v is in .
    
      The atom label of w cannot contain y, since w would then be in _1 (because  is rectified so w must be in the scope of , which is in _1), and v,w would be a link (hence leap) between  and _1, contradicting the leap supposition.
    
      Thus, for (x) to be a term containing y, there must be a link v,w with the label of v containing x and the label of w containing an existential variable  such that the term () contains y.Elaborate by delving into unification problem equations?
    Therefore  has a leap ,.
    
    Since v is in  and v,w is a link, hence a leap, by the leap supposition w must be in  or _2.  Because  is rectified, the literal w must be in the scope of the existential binder , so  is in  or _2. Since  is in _1, the leap , is between _1 and  or _2, contradicting the leap supposition.
    
    
    
    Let  be a rectified fonet with underlying uncoloured fograph
    _11mu1mu()1mu1mu_2 for  a fograph and each _i empty or a fograph.
    Suppose no leap of  is between _1∪ and ∪_2.
    Then  is an existential quantification of a rectified fonet by x.
    
    
    
      By Lemma <ref> the existential binder  is in no leap of .
    
    Let  be a most general dualizer for  and let t=(x).
    
    Define  as the result of deleting  from  and substituting t for x in the atom label of every literal.
    
    Since  is a rectified fograph and  is in no leap of ,  is a rectified fograph.elaborate
    Thus  is an existential quantification of  by x at  in the portion  for  the set of occurrences of t in  which replaced occurrences of x in  during the construction of .
    
    The mate of a literal in a link is the other literal in the link.
    
    
      Every non-universal rectified fonet with at least one edge is a fusion of rectified fonets or an existential quantification of a rectified fonet.
    
    
    
    Let  be a non-universal fonet with an edge, and let  be its underlying uncoloured fograph.
    
    Since  is a (labelled) cograph, it has the form
    =(_1_2) (_3_4)…(_n-1_n) for (labelled) cographs _i
    and , where  is a union of literals,
    
    and n 1 since  (hence ) has an edge.
    
    Let  be the graph whose vertices are the _i
    with _i_j E() if and only if  has an edge or leap
    {v,w} with v∈V(_i) and w∈ V(_j).
    
    A 1-factor is a set of pairwise disjoint edges whose
    union contains all vertices.  Since  is a fonet, Z={_1_2,_3_4,…,_n-1_n} is the only 1-factor of
    .  For if Z' is another 1-factor, then
    Z'-2mu∖-2mu Z determines a set of leaps in 
    whose union induces a bimatching in : for each
    _i_j∈ Z'-2mu∖-2mu Z pick a leap
    {v,w} with v∈ V(_i) and w∈ V(_j).  Since 
    has a unique 1-factor, some _m_m+1∈ Z is a bridgeRelated work: emphasize Retoré's use of bridge<cit.>,
    
    i.e.,
    -1.5mu∖-1mu _m_m+1=X
    Y with _m∈ X and _m+1∈ Y.[A similar construction of a unique 1-factor with a bridge is used in <cit.>, and <cit.> uses a related argument involving the existence of a bridge.]
    Without loss of generality assume G_i X for i m and
    G_j Y for j m+1.
    
    Let _X be the restriction of  to literals with mate in a vertex of X, and let _Y be the
    restriction of  to literals not in _X.
    
    Thus _X_Y since  contains only literals and no binders.
    
    Define _1=_X(G_1 G_2)…(G_m-2 G_m-1)
    and _2=_Y(G_m+2 G_m+3)…(G_n-2 G_n),
    
    so =_1(_m_m+1)_2.
    
    Since  comprises literals only, each of _1 and _2 is either empty or a fograph.
    
    If _m and _m+1 both contain a literal, they are fographs, so we can appeal to Lemma <ref> with _1=_m and _2=_m+1 to conclude that  is a fusion of rectified fonets.
    
    Otherwise one of _m or _m+1, say _m, has no literal, thus _m=. Then _m+1 must contain a literal, since  hence _m_m+1 is a fograph, therefore _m+1 is a fograph.
    
    Applying Lemma <ref>  with
    _m+1, we conclude that  is an existential quantification of a rectified fonet.
    
    
      Every rectified fonet can be constructed from axioms by fusion and quantification.
    
    
    Let  be a rectified fonet.
    
    We proceed by induction on the number of binders and edges in .
    
    In the base case with no edge or binder,  is a union of axioms by Lemma <ref>, hence a fusion of axioms since union is a special case of fusion (with empty portions).
    
    If  is universal, apply Lemma <ref> then appeal to induction with one less binder.
    
    Thus we may assume  is non-universal with a binder or edge.
    
    Had  no edge, it would have no binder (since every existential binder must be in an edge, and
    a universal binder would make  universal),
    
    thus  has at least one edge.
    
    Apply Lemma <ref> then appeal to induction with fewer edges.
    
    
      Every fonet is valid.
    
    
      By Lemma <ref> every fonet can be constructed from axioms by fusion and quantification. Since every axiom is valid, and fusion and quantification preserve validity by Lemmas <ref>, <ref>, and <ref>, every fonet is valid.
    
    
     §.§ Soundness of skew bifibrations
    
    
    In this section we no longer assume implicitly that every formula is rectified.
    
    An intrusion is a formula of the form
    ∀ x2mu,
    (∀ x2mu ),
    ∃ x2mu, or
    (∃ x2mu ).
    
    A formula is extruded if no subformula is an intrusion.
    
    For any variable x, an x-quantifier is a quantifier of the form ∀ x or ∃ x.
    
    A formula is unambiguous if no x-quantifier is in the scope of another x-quantifier, for every variable x.
    
    A formula is clear if it is extruded and unambiguous.
    
    
    The graph of a clear formula
     is the logical cograph defined inductively by:
    
    
    
    [                   =  for every atom; [  ;  ;  ][ ∀ x   x; ∃ x   x;     ];  ]
    
    
    Note that  coincides with  (Def. <ref>) on extruded rectified formulas.
    
    
    The function  is a surjection from clear formulas onto fographs.
    
    Two clear formulas have the same graph if and only if they are equal modulo
    
      
        ∧()     ()∧       ∃ x2mu∃ y2mu    ∃ y2mu∃ x2mu    
            
        
                  ∨()     ()∨   ∀ x2mu∀ y2mu    ∀ y2mu∀ x2mu
    
    
    
      A routine induction, akin to the proof of Lemma <ref>.elaborate in appendix
    Let  be a fograph. Using the above Lemma,
    choose a clear formula  such that .
    
    Define  as valid if  is valid.
    
    This is well-defined with respect to choice of  since every equality in Lemma <ref> is a logical equivalence.
    
    Fographs  and  are
    ∧-compatible if
     is a well-defined fograph and
    -2mu-2mu7ex=,
    and
    ∨-compatible if
     is a well-defined fograph and
    -2mu-2mu7ex=.
    
    Thus ∨- and ∧-compatibility ensure that no new bindings are created during graph union and join.
    
    For any variable x, a fograph  is x-compatible if  does not contain an x-binder .
    
    
      Let  and  be fographs. Define the fograph connectives∧, ∨, ∀ and ∃ by:
    
      
      *  if  and  are ∧-compatible, define 2mu=2mu
      *  if  and  are ∨-compatible, define 2mu=2mu
      
      *  for any variable x, if  is x-compatible,
    define ∀ x2mu2mu=2mu
      *  for any variable x, if  is x-compatible,
    define ∃ x2mu2mu=2mu.
    
      
    
    The fograph connectives ∧, ∨, ∀ and ∃ are well-defined on fographs. In other words, given fographs as input(s),
    each connective, when defined, produces a fograph as output.
    
    
    
      By the compatibility constraints, no x-binder of
    ,
    ,
    ∀ x2mu, or
    ∃ x2mu can be in the scope of another x-binder.
    
    
    The following equalities hold for clear formulas:
    
    
    [ [         1mu∨2mu;         1mu∧2mu;         ][    ∀ x ∀ x6mu;    ∃ x ∃ x6mu;        ] ]
    
    
    
    Since  and  are clear,  and  are ∨- and ∧-compatible, thus ∨1mu and ∧1mu are well-defined.
    
    Because ∀ x2mu and ∃ x2mu are clear, no x-quantifier occurs in , so  contains no binder , thus ∀ x3mu and ∃ x3mu are well-defined.
    
    
      A labelled graph is a fograph if and only if it can be constructed from literals by the fograph connectives ∧, ∨, ∀ and ∃.
    
    
    Let  be a fograph.
    
    By Lemma <ref> there exists a clear formula 
    such that .
    
    By Lemma <ref> the  and  operations in the inductive translation  of  are well-defined ∧, ∨, ∀ and ∃ operations on fographs. Thus  can be constructed from literals by
    
    fograph connectives.
    
    Conversely, any labelled graph constructed from literals by fograph connectives is a fograph, by repeated application of Lemma <ref>, starting from the fact that any literal vertex is a fograph.
    
    
    A map is a label-preserving graph homomorphism between fographs.
    
    
    Extend the fograph connectives to maps :→ and :→
    as follows:
    
    
      * 
    if  and  are well-defined,
    define -1mu:→
    as ∪
    
      * 
    if  and  are well-defined,
    define -1mu:→
    as ∪
    
      * 
    if ∀ x2mu and
    if ∀ x2mu are well-defined,
    define ∀ x2mu2mu:∀ x2mu→∀ x2mu
    as ∪3mu3mu
    
      * 
    if ∃ x2mu and
    if ∃ x2mu are well-defined,
    define ∃ x2mu2mu:∃ x2mu→∃ x2mu
    as ∪3mu3mu.
    
    
    
    The fograph connectives are well-defined on skew bifibrations: if  and  are skew bifibrations, then, when defined, each of the maps , , ∀ x2mu and ∃ x2mu is a skew bifibration, where x is any variable.
    
    
    Due to the compatibility constraint in the definitions of the fograph connectives,
    the skew fibration condition is preserved and the directed graph homomorphisms between binding graphs are fibrations.elaborate?
    In the ∧ and ∃ connectives, additional requisite skew liftings are created across the corresponding graph join.
    
    
      Skew bifibrations between fographs compose: if :→ and :→ are skew bifibrations between fographs, their composite -1mu:→ is a skew bifibration.
    
    
      Skew fibrations between cographs compose <cit.>, and directed graph fibrations compose <cit.>. Existential preservation is transitive.
    
    
      If  is a fograph and ∨ is well-defined, define pure contraction as the canonical map ∨→.
    
      If  and  are fographs and ∨ is well-defined, define pure weakening as the canonical map →∨.
    
    
      Every pure contraction and pure weakening is a skew bifibration.
    
    
      Immediate from the definitions of pure contraction and pure weakening.elaborate
    
    A contraction is any map generated from a pure contraction by fograph connectives, and a weakening is any map generated from a pure weakening by fograph connectives.
    
    
    Every contraction and weakening is a skew bifibration.
    
    
    Pure contraction and pure weakening are skew bifibrations by lem:pure-cw-are-bifibs, and
    fograph connectives are well-defined on skew bifibrations by Lemma <ref>.
    
    
      A structural map is any map constructed from isomorphisms, contractions, and weakenings by composition.
    
    
      Every structural map is a skew bifibration.
    
    
      Every isomorphism is a skew bifibration, and every contraction and weakening is a skew bifibration by Lemma <ref>.
    
      Skew bifibrations compose by Lemma <ref>.
    
    
    
    Structural maps are sound: if  is a valid fograph and :→ is a structural map, then  is valid.
    
    
      Isomorphisms, pure contraction, pure weakening, composition and fograph connectives are sound.
    
    
    
      §.§.§ The image of a skew bifibration is a fograph
    
    
    We recall the modular decomposition<cit.> of a cograph, called its cotree<cit.>.
    
    A directed graph  is acyclic if the transitive closure of  (viewed as a binary relation on ) is irreflexive.
    
    A forest is an acyclic directed graph  such that for every n there exists at most one m with nm∈-3mu.
    
    We refer to the vertices of a forest as nodes.
    
    Write m n or n m for n m∈-3mu, and say that m is a child of n and n is the parent of m.
    A leaf (resp. root) is a node with no child (resp. parent).
    
    A tree is a forest with a unique root.
    
    A  is a tree in which
    a node is labelled  or  if and only if it is not a leaf.
    
    Each node labelled  or  is a
    
    .
    
    An isomorphism ι:→ of  is a bijection
    ι:→ such that
    m n if and only if ι(m)1mu2muι(n) and
    ι(n) is a  (resp. ) node
    if and only if n is a  (resp. ) node.
    
    We identify  up to isomorphism.
    
    Given _1,…,_n for n≥ 1 define _1…_n (resp. _1…_n) as the disjoint union of the _i together with a  (resp. ) root node r and an edge to r from the root of each _i (1 i n).
    
    Write  for the  with a unique node.
    
    For example, the ()-4mu(0ex1.7ex-4mu-4mu())
    is below-left and
    ()()-4mu(0ex1.7ex-4mu-4mu(()))
    is below-right.
    
    
    (0,)(0,-)(-5.5,)
    (-.2,0)-,a-,0b a b
    
      0,c
      (,0)0,d0,0e,f,0g d e
         d f
         e f
         d g
         e g
      
    (5.5,0).75.75.6-.235.6-.235.6
    
    
    
    The cograph of a  is the cograph defined inductively by
    
        =
        
        _1…_n=_1…_n
        
        _1…_n=_1…_n
    
    For example, the cograph of the  above-left is shown above-center; this cograph is also the cograph of the  above-right.
    
    
      The leaves of a  are in bijection with the vertices of its cograph .
    
    
      Induction on the number of vertices in , pattern-matching the three cases in
    Def. <ref>.
    
    
    A repeats if it has a parent with the same label, and is unary if it has a unique child.
    
    A alternates if it has no repeating  and
    branches
    if it has no unary .
    
      A cotree is a branching and alternating .
    
    For example, the  above-left is a cotree, while the  above-right is not (since it has a repeating  node and a unary and repeating  node).
    
    We recall the following definition from <cit.>.
    
    
    The cotree of a cograph  is the cotree defined inductively by
    
    =[                                _1…_n                                _1…_n       if _i is connected for 1 i n 2;                                _1…_n                                _1…_n if _i is coconnected for 1 i n 22mu. ]
    
    The following Lemma articulates a standard property of cotrees.
    
    Recall from <ref> that a module in a graph is proper if it has two or more vertices.
    
    A module  of a cograph  is connected (resp. coconnected) if the induced subgraph  is connected (resp. coconnected).
    
    
    The nodes of the cotree  of a cograph  correspond to the strong modules of ,
    and the  (resp. ) nodes correspond to proper connected (resp. coconnected) strong modules.
    
    
      Induction on the number of vertices in <cit.>.
    
    The following Lemma is also a standard cotree property.
    
    
    The function -
    is a bijection from cographs to cotrees.
    
    
      Induction on the number of vertices in the cograph <cit.>.
    
      The cotree  of a cograph  is the unique branching and alternating  such that =.
    
    
      A routine induction on the number of vertices in .
    
    
    
      The vertices of a cograph  are in bijection with the leaves of its cotree .
    
    
      Lemmas <ref> and <ref>.
    
    Let  be a node in a tree =.
    
    Define the absorption of  in  as the result of deleting  (and incident edges) from  and, if  has a parent , adding an edge from each child of  to .
    
    Thus
    
    =
    1mu-2mu-2mu and
    mm if and only if m  m
    or
    m    m.
    
    
    Given a  define its cotree as
    the cotree obtained by iteratively and exhaustively absorbing unary  and repeating  in .
    
    For example, if  is the  above-right of Def. <ref> then its cotree  is above-left of Def. <ref>.
    
    
      = for every .
    
    
      By induction on the number of nodes in , pattern-matching the three cases in Def. <ref>, combined with the associativity and commutativity of the graph union  and join  operations.
    
    Recall that U is the subgraph of a graph  induced by a set of vertices U.
    
    Define the Uinduced by a non-empty set of leaves U in a  by deleting from  every leaf not in U, and then iteratively and exhaustively deleting any resulting childless .
    
    For example, if  is the cotree below-left and U comprises the left-most four leaves of , then the U is below-center, and the cotree U is below-right.
    
    
    (0,)(0,-)(-5,)
    (.5,).9
      .75
        
        .6
          
         
      
    
    
    (5.5,).9.75
        
        
      
    
    
    
      If U is a non-empty set of leaves in a cotree , then
      U =  U.
    
    
      Induction on the number of nodes in .
    
    
    If U is a non-empty set of vertices in a cograph , then
    U= U.
    
    
    By lem:cograph-absorb,
    U
    =
     U, which is
    U
    by lem:induced-subtree,
    hence
    U
    by lem:unique-branching-alternating.
    
    
      If U is a non-empty set of vertices in a cograph , then
      U =  U.
    
    
    By lem:unique-branching-alternating it suffices to show that
    U= U, which is lem:cograph-cotree-induced.
    
    
    Write  for the set of nodes of a tree ,  for its set of directed edges,  for the transitive closure of , and  for the reflexive closure of .
    
    Define
     as
    ,
    and say that
     is above or
     is below;
    define
     as
    ,
    and say that
     is at or above or
     is at or below.
    
    Define
    
    the meet of nodes  and  in a tree  as the 2mu-least node  with  and .
    
    
      Let  be a cograph and v,w∈. Then vw if and only if v w in the cotree  is a  node and vw if and only if v w is a  node or v w.
    
    
      This follows directly from lem:node-strong-module.
    
    Write v w (resp. v w) for v w if it is a  (resp. ) node.
    
    For a cograph  write
    ,
    ,
    and
     for
    
    ,
    ,
    and
    , respectively.
    
    
    If  is a cograph with vw,vu, wu, w u,
    then
    v  v w  w u  w,u.
    
    
    
    By Lemma <ref>v w is a  node and w u is a  node.
    Since v w w w u and  is a tree, either
    v w w u or
    v w w u.
    
    If v w w u then v u is a  node, contradicting vu (by Lemma <ref>), so v w w u.
    
    
    
    If  is a cograph with vw,vu and wu
    then v  v w  w u  w,u.
    
    
    Necessarily w u since wu, hence v w and v u.
    Thus we can apply Lemma <ref> to the complement of .
    
    
      If :→ is a skew fibration between cographs and
      v    v  w    w
      for v,w with (v)(w),
      then
      (v)   (v)(w)   (w).
    
    
    
    Since (v)(w) the meet (v)(w) in
    
     is a  or  node.
    
    If the former,
    
    we have
     as desired.
    
    Otherwise
    
    .
    
    By Lem. <ref> since
    ,
    and
     since
    .
    
    Because  is a skew fibration and ,
    there exists u with
    vu and .
    
    Since  is a graph homomorphism,
    (v)1mu(u) and
    wu,
    and w u (otherwise vw since vu, contradicting vw).
    
    Since wv,wu and vu,
    
    by Lemma <ref> we have
    w  w v  v u  v,
    
    hence
    v v u v w, contradicting v v w.
    
    The following Lemma refines
    (v)(v)(w)
    in the above Lemma to
    (v)(v)(w).
    
    
      If :→ is a skew fibration between cographs and
      v    v  w    w
      for v,w with (v)(w),
      then
      (v)   (v)(w)   (w).
    
    
    By Lemma <ref> we have
    (v)   (v)(w)   (w).
    
    Suppose not (v)(v)(w). Then
    
    for some u.
    
    Since (v)   (v) u   u
    we have (v)1mu u by lem:meet.
    
    Because  is a skew fibration and (v)1mu u, there exists ũ with vũ and (u)-1mu(ũ).
    
    Necessarily ũ w, otherwise lem:covee applied to
    vw,ũ w
    and
    vũ
    yields
    w  w v  vũ v
    so
    v    vũ   w v
    contradicting v  v w.
    
    
    If :→ is a skew fibration of cographs and m   m n   n, then
    
    (v) m for some v
    if and only if
    (w) n for some w.
    
    
    
    Assume m n, otherwise the result is immediate.
    
    Suppose (v) m for v.
    
    Choose u with u n.
    
    Thus (v)   m    m n    n    u.
    
    Since m n=(v) u is a  node,
    we have (v)1mu u by Lemma <ref>.
    
    Because  is a skew fibration and (v)1mu u,
    there exists
    u
    with
    vu
    and
    (u)1mu u.
    
    Since vu and  is a graph homomorphism, we have
    (v)1mu(u).
    
    If u(u) then since
    n    u
    we have (u) n as desired.
    
    Otherwise u(u), so applying Lemma <ref> to
    (v)1mu u,(v)1mu(u),
    u1mu (u),
    u(u)
    yields
    (v)   (v) u    u(u)    u,(u).
    
    Thus since (v) u=m n is the parent of n,
    both
    
    and
    ,
    so because  is a tree,
    we have
    n    w1mu1mu(u),
    hence
    
    (u)    n.
    
    Given a function :V→ W write (V) for (v)v V⊆ W.
    
    
    Let :→ be a graph homomorphism between cographs. Define the image as the subgraph () of  induced by ().
    
    
    Define v w if v and w are leaves and v   w for the parent v of v.
    
    Recall that a cograph is logical if every vertex is a binder or literal (, is labelled by a variable or atom), and at least one vertex is a literal.
    
    Write  for the scope of a binder  in a logical cograph .
    
    The following Lemma shows that the scope of  is the set of leaves below the parent of  in the cotree .
    
    
      For any vertex  and binder  in a logical cograph ,
    
    
    if and only if
    .
    
    
    By definition the scope of  is the smallest proper strong module containing ,
    which corresponds to the parent of  in the cotree  by lem:node-strong-module.
    
    
      For any  and non-root  in ,
      if v w then v w.
    
    
      Immediate from the definition of .
    
    
      For any , if v w then v w.
    
    
      Iterate lem:absorption-parent-below for every absorption step in the construction of  in Def. <ref>.
    
    
      For any  and non-empty set U of leaves in ,
      if v w and v,w U then v U w.
    
    
      The edge relation U is a subset of .
    
    
    Let  be a logical cograph which is an induced subgraph of a logical cograph .
    
      For every vertex  and binder  in ,
    
      if ∈ then ∈.
    
    
    
    Let ∈.
    
    By lem:scope-parent, .
    
    By lem:induced-parent-below, .
    
    By lem:absorbed-parent-below,
    .
    
    By lem:induced-cotree,
    
    =,
    
    and =,
    thus
    .
    
    Therefore ∈ by lem:scope-parent.
    
    
    A fograph map :→preserves universals if every universal binder  in  maps to a universal binder () in .
    
    
      Every skew fibration between fographs preserves universals.
    
    
      By  lem:node-strong-module, a binder is universal if and only if its parent in the cotree is a  node. Thus the result follows from lem:preserve-parent-plus.
    
    A fograph map preserves binders if every universal (resp. existential) binder  in  maps to a universal (resp. existential) binder () in .
    
    
      Every skew bifibration between fographs preserves binders.
    
    
      Skew bifibrations preserve existentials by definition, and universals by lem:pres-universals.
    
    For every skew bifibration :→ of fographs, the image  is a logical cograph.
    
    
    Every vertex of  is inherited from , and is therefore a binder or literal.
    
    Since  is an induced subgraph of a cograph , it is a cograph.
    
    Because  is a logical cograph, it contains a literal , thus  contains the literal () (a literal since  preserves labels).
    
    
    For every skew bifibration :→ between fographs and universal binder  in ,
    
    the scope  contains a literal in .
    
    
    Choose  in  with ()=.
    
    By lem:pres-binders,  is universal.
    
    Since  is a fograph there exists a literal ∈,
    
    so
    b̃ by lem:parent-scope.
    
    Since ()() by label preservation,
    by lem:preserve-parent-plus
    we have
    b()  (),
    so ()∈ by lem:parent-scope.
    
    For every skew bifibration :→ between fographs and universal binder  in ,
    
    the scope  contains a literal.
    
    
    By lem:target-universal-scope, the scope  contains a literal ().
    
    Since  is an induced subgaph of , by lem:induced-scope we have ()∈.
    
    
    
    For every skew bifibration :→ between fographs and existential binder  in ,
    
    the scope  contains a literal in .
    
    
    Since  is a fograph there exists a literal  in  in the scope of .
    Thus
    b by lem:parent-scope.
    
    Therefore
    n for some child n of .
    
    Since  is in  there exists ∈
    with
    (), so
    we may apply lem:balance with
    m and v to obtain
    w∈ with (w) n.
    
    If w is a literal, then the literal (w) is in , and the Lemma holds.
    
    Otherwise w is a binder, hence (w) is a binder.
    
    We proceed by induction on the number of vertices in the scope .
    
    Since (w)    n for (w) a binder and  a literal,
    n must be a  or  node,
    and since  and  alternate in a cotree,
    n is a  node because its parent  is a  node.
    
    Let n be the parent of (w).
    
    Thus
    n    n  (w).
    
    If n is a  node, then (w) is universal so by lem:image-universal-scope the scope of (w) contains a literal in , , a literal () for some literal  in .
    
    Therefore
    n    n  (), so () is also in .
    
    Otherwise n is a  node, so (w) is existential. Since (w) is strictly contained in , by induction there exists a literal  in  such that () is in (w), thus the literal () is in .
    
    
    
    For every skew bifibration :→ between fographs and binder  in ,
    
    the scope  contains a literal in .
    
    
      If  is universal (resp. existential) apply lem:target-universal-scope (resp. <ref>).
    
    
    For every skew bifibration :→ between fographs and existential binder  in ,
    
    the scope  contains a literal.
    
    
      By lem:image-existential-scope-prep there exists a literal  with () in . Since  is an induced subgraph of , we have () in  by lem:induced-scope.
    
      A logical cograph  is fair if binders  and  have the same variable only if .
    
    Note that every rectified fograph is fair.
    
    
      For every skew bifibration :→ between fographs with  fair,  is a fair fograph.… is a fair fograph needed anywhere?
    
    By lem:im-logical is a logical cograph, and  is fair since if  for binders  and  with the same variable, then  since  is an induced subgraph, contradicting the fairness of . It remains to show that
    
    (1) for every binder  in  the scope  contains a literal, and (2) for every variable x and every x-binder  in , the scope  contains no other x-binder.
    
    (1) If  is universal (resp. existential), then by lem:image-universal-scope (resp. <ref>), the scope
     contains a literal.
    
    (2)
    Suppose  were another x-binder with ,
    , .
    
    If  is universal,
    then
    ,
    so
    
    ,
    whence , contradicting the fact that  is a fograph.
    
    Otherwise,  is existential,
    
    and , so .
    
    Since  is an induced subgraph of , we have , contradicting the fairness of .
    
    
    The following example illustrates why fairness of  is required to ensure no x-binder is in the scope of another in lem:image-fograph.
    
    Let =(∃ x2mu)(∃ x2mu)
    =
    xxpxpxxpxxxpxpxxpx,
    let
    =q-.5mu∨∃ x2mu
    =
    xxpxpxxpx,
    and let  be the unique label-preserving graph homomorphism →, which is a skew bifibration between fographs.
    
    Then
    :→=
    is a skew bifibration between fographs, with  not fair, and  is
    
    (xxpxpxxpx)
    
    (xxpxpxxpx), which is not well-defined fograph since each  is in the scope of the other.
    
    
    
      §.§.§ Marking and pruning
    
    Let  be a cograph and let U.
    
    A node  in the cotree  is overU if
    
    n u
    for some vertex u U.
    
    Define
    
    the supportU⊆
    as the set of nodes over U,
    
    and say that U is balanced for  if, for every  node  in  and child  of , we have U if U.
    
    If :-2mu→-2mu is a skew fibration between cographs
    then (-2mu) is balanced for .
    
    
    A corollary of lem:balance.
    
    Let  be a cograph and let U.
    
    A  in U is literal-supported
    if there exists a literal U with .
    
    We say that U is binding-closed if, for every literal U and binder  in 
    such that  binds , we have U.
    
    
    Let  be a fograph. A set U is a marking for  if it is balanced, every  of U is literal-supported, and U is binding-closed.
    
    
    If :→ is a skew bifibration
    
    between fographs
    then
    
    () is a marking for .
    
    
    Let U=().
    By lem:balance, U is balanced, by lem:target-scope, every node  in U is literal-supported,more
    and U is binding-closed since :→ is a directed graph fibration.
    
    Let  be the child of a  node  in a .
    
    The node  is critical to  if  is the only child of  which is at or above a literal.
    
    If  is an x-binder for some variable x, then  is vacuous if it is the unique node in the subtree rooted at  whose label contains x.[Thus in the cograph , the binder  (which is universal since its parent is a  node) binds no literal.]
    A node  in a  is pareable if:
    
    
      *  has a parent  node ,
    
      *  is not critical to , and
    
      *  if  is a binder (necessarily universal) then it is vacuous.
    
    
    To pare a pareable node  in a  is to delete the subtree rooted at .
    
    
    A pruning is any result of iteratively paring zero or more pareable  nodes.
    
    
    
      Let  be a fograph with marking U,
      and let  be a  such that =.
    
    There exists a pruning  of  with = U.
    
    
      A routine induction on the number of nodes in .elaborate: see sheet 22 of notepad Apr'19
    
      §.§.§ Decomposition of skew bifibrations
    
      If  is a connected fograph without the variable x, define slackeningx as the canonical inclusion map →∀ x2mu.
    
    
      Every slackening is a structural map.
    
    
      Weaken  to ∨∀ x2mu, which is ∀ x(∨), then contract under ∀ x to ∀ x2mu. (Note that ∨ is well-defined because  is connected.)
    
    
      A  is any map constructed from isomorphisms, weakenings and slackenings by composition and fograph connectives.
    
    
      Every  is a structural map.
    
    
      Iterate lem:slackening-structural.
    
    
      Let  be a fograph,
    
      let  be a  such that =,
      let  be the result of paring a pareable node in , and let =.
    
    There exists a →.
    
    
      If the paring is of a vacuous binder (condition 3 in Def. <ref>), then we obtain a slackening in the context of a fograph connective, otherwise (condition 2 in Def. <ref>) we obtain a weakening in the context of a fograph connective.
    
    
      Let  be a fograph,
    
      let  be a  such that =,
      let  be a pruning of , and let =.
    
    There exists a →.
    
    
      Apply lem:paring-ws to each paring in the pruning.
    
    
      Let :→ be a skew bifibration with  fair. The inclusion → is a .
    
    By lem:image-fograph,  is a fograph.
    
      Let U=(), thus  is the induced subgraph U.
    
      By lem:im-marking, U is a marking.
    
      Let  be the cotree .
      By lem:im-marking, there exists a pruning  of  with = U=.
    
      By lem:pruning-ws, there exists a →, ,G(T(G))=G lemma earlier?→.
    
     Let :→ be a skew fibration and let K be a connected component of . The multiplicity of K is the number of connected components of ^-1(K), and the weight of K is one more than its multiplicity.
    
    The weight of  is the sum of the weights of the connected components of .
    
    A skew bifibration is shallow if the multiplicity of every connected component of  is at most one.
    
    
      Every skew bifibration into a fair fograph is a structural map.
    
    elaborate?
      By induction on the weight of the skew bifibration :→ and its multiplicity.
    
    By lem:image-inclusion-wsmap
    (and the fact that every  is a structural map by lem:ws-structural)
    we may assume  is a surjection, and by pre-composing with contractions
    
    we may assume  is shallow.
    
      If = then = since  is a shallow surjection, hence =∀ x2mu, and by induction  is a structural map.
    
      Otherwise if =_1_2 then =_1_2 (since  is not of the form ).
    
      Since  is a shallow surjection, =_1_2, so =_1_2 for _i:_i→_i. By induction each _i is a structural map, hence  is structural.
    
      Otherwise  is connected. If  has no edge then  is an isomorphism from a literal to a literal, hence is a structural map. Thus we may assume  has an edge.
    
    If = then = since  is a shallow surjection, hence =∃ x2mu, and by induction  is a structural map.
    
    Otherwise =_1_2 for fographs _i, with _i not of the form x_i'. Thus =_1∧_2, hence =_1∧_2 with (_i)⊆_i. Therefore =_1∨_2 for skew bifibrations _i:_i→_i, and by induction each _i is a structural map, so  is a structural map.
    
    
    
      If  is a valid fograph and :→ is a skew bifibration with  fair, then  is valid.
    
    
      By Lemma <ref>,  is a structural map, which is sound by lem:strucmap-sound.
    
    
     §.§ Proof of the Soundness Theorem
    
    Let :→ be a combinatorial proof of a formula . By lem:fonet-soundness is valid,
    thus by lem:bifib-sound is valid (applicable since  is rectified, hence fair), therefore  is valid.
    
    
    § PROOF OF THE COMPLETENESS THEOREM
    
    
    In this section we prove the Completeness Theorem, Theorem <ref>.
    
    Our strategy will be to show that
    every syntactic proof of a formula  in Gentzen's classical sequent calculus <cit.>
    generates a combinatorial proof of , so completeness follows from that of Gentzen's system.
    
    A sequent is a finite sequence  of formulas, n 0.
    
    We identify a formula  with the single-formula sequent containing .
    
    Let  be the sequent .
    
    Its formula is , and  is
    valid
    (resp. rectified)
    if  is
    valid
    (resp. rectified).
    
    As with formulas, we shall assume, without loss of generality, that every sequent is rectified (by renaming bound variables as needed).
    
    The graph of a sequent  is the graph
    
    
    of its formula.
    
    For example,
    ∃ y2mu2mu=4mu y yppy yppy2mu.
    
    A combinatorial proof of  is a combinatorial proof of its formula .
    
    For technical convenience we will use a right-sided formulation  of Gentzen's sequent calculus <cit.>,
    comprising the following rules.
    
    Here
     and 
    are arbitrary sequents,
     and  are arbitrary formulas,
     is any atom which is not a logical constant,
    and ≅ denotes that  is
    equal to  up to bound variable renaming (,
    ∀ x2mu pxy
    ≅∀ z2mu pzy).[For the ∃ rule, recall
    (from <ref>)
    that  denotes
    the result of substituting a term  for all occurrences of the variable  in , where,
    without loss of generality (by renaming bound variables in  as needed),
    no variable in  is a bound variable of .]
    2̌.̌5̌14[               [lb](.3,.3)(≅); [lb](.3,.3)(x not free in Γ) ]2̌.̌5̌
    
    The rules ,   and  are called exchange, contraction and weakening.
    
    Each sequent above a rule is a hypothesis of the rule, and the sequent below a rule is the conclusion of the rule.
    
    
      A sequent is valid if and only if it has an  proof.
    
    
      System  is equivalent to , which is sound and complete <cit.>.
      It differs in that  retains Gentzen's explicit formula-exchange (or permutation) rule ,
      while <cit.> leaves exchange implicit by formulating sequents as multisets rather than sequences.
    
    
    
     §.§ Interpreting rules as operations on combinatorial proofs
    
    
    We interpret each rule of  with hypothesis sequents _1,…,_n and conclusion sequent  as an operation taking combinatorial proofs _i of _i as input to produce a combinatorial proof  of .
    
    
      *  rule. Define  as the identity on , with both vertices the same colour in the source.
    
    
      * 1 rule. Define  as the identity on 1, with no colour in the source.
    
    
      * ∨ rule
    with hypothesis = and conclusion =.
    
    Let  be the combinatorial proof of .
    Note that =.
    Define =.
    
    
      *  rule
    with hypothesis = and conclusion =.
    
    Let  be the combinatorial proof of , and let  be the canonical isomorphism →.
    
    Define =∘.
    
    
      *  rule with hypothesis = and conclusion =.
    
    Let  be the combinatorial proof of , and let  be the canonical injection →.
    
    Define =∘.
    
    
      * ∀ rule
    with hypothesis = and conclusion =.
    
    Let :→ be the combinatorial proof of  and
    let  be the canonical injective graph homomorphism .
    
    Note =.
    
    If ^-1() is empty define =∘:→.
    
    Otherwise,
    
    define  as
    
    the extension of ∘:→
    which maps
    
    x to the (unique) x-binder in .
    
    
      *  rule
    with hypothesis = and conclusion =.
    
    Let :→ be the combinatorial proof of .
    
    Let  be the result of dropping the labels from  and
    let  be the skeleton of .
    
    Let  be the canonical surjective graph homomorphism .
    
    Define h=∘:→.
    
    A universal binder in  is outer if it is in no edge.
    A duplicator is an outer universal binder  in  such that
    h^-1() contains two vertices.
    To collapse a duplicator  is to
    delete one of the two vertices of h^-1() from .
    Define ^- as the derivative of  obtained by collapsing every duplicator.
    Define the skeleton :^-→ of  as
    the restriction of h to ^-.
    Thus :^-→ for ^- the result of adding the canonical labels to ^-
    (, the label of  in ^- is the label of () in ).[For example,
    let =∀ x1mu 13mu∀ y1mu 1,
    let =∀ x1mu 1,
    let =
    =
     x 1
     y  1,
    and let  be the identity →.
    
    
    
    Then = x 1
    and x in  is a duplicator.
    
    Thus
    ^-= and the combinatorial proof
     of  is the unique label-preserving function from
     to = x1.
    We must delete y from  to form ^- because otherwise  will be
    
    from
    
    to
    x1, whose source  is not a well-defined fograph since it has two universal x-binders in the scope of one another.]
    
      * ∧ rule
    with hypotheses _1=1 and _2=2 and conclusion =.
    
    Let _i:_i→_i be the combinatorial proof of _i and let _i be the canonical injective graph homomorphism _i→.
    
    Note that _i=_i_i.
    
    Let _i=_i^3mu-1(_i)
    and define _i as weak if _i is empty, else strong.
    
    Define  according to the following cases.
    
    
    
    
      * _1 and _2 are both strong or both weak.
    Let  be the fusion of _1 and _2 at the portions P_1 and P_2.
    Define :→ as the union of _1∘_1 and _2∘_2.
    
    
      * _i is weak and _3-i is strong.
    Define :_i→ as _i∘_i.
    
    
      * ∃ rule
    with hypothesis = and conclusion =.
    
    Let :→ be the combinatorial proof of .
    
    Let  be the result of dropping the labels from  and let :→ be the skeleton of .
    
    Let  be the canonical injective graph homomorphism .
    
    Note =.
    
    Let P=^-1().
    
    Define the skeleton  of  according to the following cases.
    
    
    
      * P is empty. Define  as ∘:→.
    
      * P is non-empty. Let ^+ be the
    
    extension of  with an additional vertex v and edges from v to every vertex in P.
    
    Define :^+→ as
    the extension of ∘:→ to ^+ which maps  to the x-binder of .
    
    
    
    The interpretation of each rule of  defined above
    produces a well-defined combinatorial proof.
    
    
    A routine verification of the fograph and skew bifibration conditions defining a combinatorial proof.
    
    
     §.§ Proof of the Completeness Theorem
    
    Let  be a valid formula.
    
    By lem:r-sound-complete there exists an  proof Π of .
    
    By lem:interp-well-defined we obtain a combinatorial proof of  from Π by interpreting each rule of Π as an operation on combinatorial proofs, as defined in <ref>.
    
    
    
    § HOMOGENEOUS SOUNDNESS AND COMPLETENESS PROOFS
    
    
     §.§ Propositional homogeneous soundness and completeness proof
    
    
    In this section we prove the propositional homogeneous soundness and completeness theorem, Theorem <ref>.
    
    We begin by observing that the function  from simple propositions to dualizing graphs (Def. <ref>) factorizes through simple propositional fographs.
    
    A fograph is propositional if every predicate symbol is nullary, and simple if it has no 1- or 0-labelled literal.
    
    For example, the middle row of Fig. <ref> (p. fig:dualizing-graphs) shows four simple propositional fographs.
    
    
      The dualizing graph of a simple propositional fograph is the dualizing graph  with =, =, and ∈ if and only if
     and  have dual predicate symbols.[In <ref> we will show that  is a surjection from simple propositional fographs onto dualizing graphs (lem:surj-prop-fographs-to-dualizing-graphs).]
    For example, for each simple propositional fograph  in the middle row of Fig. <ref> (p. fig:dualizing-graphs),
    the corresponding dualizing graph  is shown below .
    
     is a well-defined dualizing graph for every simple propositional fograph .
    
    
    Let
    
    =.
    
    Since
    =,
    =
    and
     is a fograph,
     is a cograph.
    
    By reasoning as in the proof of lem:dualizing-graph-of-prop-well-defined,  is P_4- and -free.
    
    
    
    The function  from simple propositions to dualizing graphs (Def. <ref>) factorizes through simple propositional fographs:
    = for every simple proposition .
    
    
    A routine induction on the structure of .todo
    
    A simple proposition is valid if it has a homogeneous combinatorial proof.
    
    
    Suppose
    :→=
    is a homogeneous combinatorial proof of the simple proposition .
    
    By lem:prop-factorization, =.
    
    Define  as the cograph 
    with a link , for each ∈
    and the label of a vertex  in  defined as the label of () in ,
    
    where ()
    can be viewed as a vertex of  since
    =
    by definition of .
    
    Since  is a dualizing net,  is a fonet: (a) every colour is a pre-dual pair of literals, since :→ is an undirected graph homomorphism,
    
    (b)  trivially has a dualizer, the empty assignment, since it is propositional, with no existential variables,
    
    and
    (c)  has no induced bimatching, since the leap graphs  and  are equal and
     has no induced bimatching.
    
    We claim that :→ is a skew bifibration.
    
    Since :→ is a skew fibration,
    =, and
    =,
    
    we know :→ is a skew fibration.
    
    Because the label of  in  is
    that of () in , :→ preserves labels. Since there are no binders, existentials are preserved trivially and :→ is trivially a directed graph fibration.
    
    Thus :→ is a skew bifibration, hence a combinatorial proof (since  is a fonet).
    
    By Theorem <ref>,  is valid.
    
    
    
    Every valid simple proposition has a homogeneous combinatorial proof.
    
    
    Let  be a valid simple proposition.
    
    By Theorem <ref> there exists a (standard) combinatorial proof :→.
    
    Let  be the dualizing graph obtained from  by replacing each link (colour) , by a duality .
    
    Since, by definition of a linked fograph, every literal is in exactly one link,
     is a matching,
    
    and since  is a simple propositional fonet,  has no induced bimatching; thus  is a dualizing net.
    
    Let
    =.
    
    By lem:prop-factorization,
    
    =, thus
    =.
    
    We claim that :→ is a homogeneous combinatorial proof, , (1) :→ is a skew fibration and (2)  is a graph homomorphism.
    By definition, (1) holds if  is a skew fibration, which is true because  is a skew bifibration,
    =, and
    =.
    
    For (2), suppose . Since  is a fonet, it has a dualizer, so the labels of  and  are dual, say, p and , respectively.
    
    Because  preserves labels, () and () are labelled p and , thus ()2mu()∈, and (2) holds.
    
    Theorem <ref> (Propositional homogeneous soundness and completeness)
    
    Lemmas <ref> and <ref>.
    
    
     §.§ Monadic homogeneous soundness and completeness proof
    
    
    In this section we prove the monadic homogeneous soundness and completeness theorem, Theorem <ref>.
    
    The proof of completeness is similar to that of the propositional case,
    
    lem:prop-completeness:
    transform a standard first-order combinatorial proof of a monadic formula into a homogeneous combinatorial proof.
    
    The proof of soundness is more subtle. In the propositional case,
    
    lem:prop-soundness,
    we transformed a homogeneous combinatorial proof directly into a standard one, with the same vertices in both source and target.
    
    The monadic case involves quotienting indistinguishable vertices in the source monet.
    
    
    
      §.§.§ Factorization through closed monadic fographs
    
    
    A fograph is closed if it contains no free variables,
    and monadic if its predicate symbols are unary and it has no function symbols or logical constants (1 or 0).
    
    
    The mograph of a closed monadic fograph  is the mograph  with
    
    
      * =,
    
      * =,
    
      *  if and only if
    
     and  are literals whose predicate symbols are dual, and
    
      *  if and only if
    
     binds .
    
    
    For example, the closed monadic fograph  in Fig. <ref> (centre)
    
    has the mograph  to its right.
    
     is a well-defined mograph for every closed monadic fograph .
    
    
    The underlying cograph  is inherited directly from .
    
    By reasoning as in the proof of lem:dualizing-graph-of-prop-well-defined,  is P_4- and -free.
    
    It remains to show
    
    (a) every target of a binding in  is in no other binding,
    
    (b) no binder is in a duality,
    
    (c) the scope of every binder  is non-empty, and
    
    (d)  only if  is in the scope of .
    
    (a) Since  is monadic, every literal label contains exactly one variable, hence is bound by at most one binder in . By definition of , no literal binds any other vertex, thus every literal target of a binding is in no other binding.
    
    (b) Dualities are defined as pairs of literals in , which become literals in  since  is closed.
    (Every literal in  is bound by a binder in , so becomes a literal in .)
    
    (d) By definition of fograph binding,  is bound by a binder  only if  is in the scope of .
    
    
    
    The function  from closed monadic formulas to mographs (Def. <ref>) factorizes through closed monadic fographs:
    = for every closed monadic formula .
    
    
    A routine induction on the structure of .todo
    
      §.§.§ Collapsing indistinguishable vacuous universal binders
    
    
    Given an equivalence relation ∼ on a set  write ∼
    for the ∼-equivalence class ∼ and
    ∼ for the set of ∼-equivalence classes ∼.
    
    For a set  of edges on  define ∼ as the set ∼∼,∈ of edges on ∼.
    
    Given a mograph  and an equivalence relation ∼ on  define the quotient mograph ∼ by
    3mu∼=∼,
    3mu∼=∼,
    3mu∼=∼,
    and
    3mu∼=∼.
    
    A binder in a mograph is vacuous if it binds no literal.
    
    Let :→ be a skew bifibration of mographs.
    
    Vacuous universal binders  and  in  are indistinguishable
    if their images and neighbourhoods are equal, ,
    ()=() and =.
    
    Define  as the equivalence relation on  generated by indistinguishability,
    
    and the collapse:→
    as the canonical function on the quotient,
    
    , ()=(), a well-defined function since  implies ()().
    
    
    Let  be a mograph and  a monet.
    If
    :→ is a homogeneous combinatorial proof then its collapse
    :→ is a homogeneous combinatorial proof.
    
     is a monet because if
    W2mu induces a bimatching in
     then it induces a bimatching in :
    since indistinguishable vertices are vacuous binders, they cannot be in both a leap and an edge of
    , so cannot occur in W.
    
    The function
    :→
    is a skew fibration because
    :→ is a skew fibration and indistinguishable vertices have the same image and neighbourhood, and
    
    
    is a homomorphism because
    
    is a homomorphism and no binder is in a duality edge.
    
    Finally,
    :→
    is a fibration because
     is a
    fibration and indistinguishable binders are vacuous, therefore absent from bindings.
    
    
    
      §.§.§ Monadic fonets without dualizers
    
    
    Monets were defined (<ref>) without need for dualizers, in terms of the binder equivalence relation -4mu.
    
    In this section we take an analogous approach with monadic fonets (<ref>).
    
    Let rmf abbreviate rectified monadic fograph.
    
    
    Let  be a linked rmf.
    
    Variable equivalence is the equivalence relation on binders generated by
    x y
    for each link , in .
    
    
    In the above definition p is any predicate symbol (necessarily unary, since  is monadic).
    
    A conflict in  is a pair x,y of distinct non-existential variables x and y such that x y.
    
    
    A linked rmf is consistent if
    
    it has no conflict.
    
    
    A linked rmf has a dualizer if and only if it is consistent.
    
    
    Let  be the linked rmf.
    
    Suppose  has a dualizer. By lem:mgd has a most general dualizer .
    
    Thus for every colour  we have () dual to ().
    (Recall that  denotes the result of substituting (x) for x in .)
    
    For a contradiction, suppose z_1,z_2 were a conflict in , ,
    z_1-2mu-2mu z_2 for
    non-existential variables z_1 z_2.
    
    Since
    z_1 z_2
    we have variables
    x_1,…, x_n for n 1 with x_1=z_1, x_n=z_2, and for 1 i n there exists a link p_ix_i, _ix_i+1.
    
    Since  is a dualizer we have (p_ix_i) dual to (_ix_i+1), so x_i=x_i+1.
    
    Thus x_1=x_n so z_1=z_2.
    
    Since z_1 and z_2 are non-existential, we have z_1=z_1 and z_2=z_2, hence z_1=z_2, contradicting z_1 z_2.
    
    Conversely, suppose  is consistent.
    
    Let e_1,…,e_n be the equivalence classes of .
    
    Define y_i as the unique non-existential variable in e_i, if it exists (unique since  is consistent), and otherwise define y_i as a fresh variable, where fresh means not in  and distinct from y_j for 1 j i.
    
    Given an existential variable x, define (x)=y_i if e_i is the equivalence class containing x_i.
    
    We must show that for every link  in  we have (px) dual to ().
    
    Thus it remains to show that x=y.
    
    Since x and y are in the same link, they are in the same equivalence class e_i (for some i).
    
    We consider three cases.
    
    
      *  Both x and y are existential. Since x and y are in e_i, we have (x)=(y)=y_i.
    
    
      *  Both x and y are non-existential. Therefore x=x and y=y, so we require x y.
    This holds because x y would imply that x,y is a conflict, contradicting the consistency of .
    
    
      *  Exactly one of x and y is existential, say x. Since y is non-existential, y=y, and y is the unique y_i non-existential variable in e_i. Since x is also in e_i, we have (x)=y_i.
    
    
    
    
      Let  and  be binders in a consistent linked rmf , with  existential and  universal.
    
      The pair , is a dependency of  if and only if x y.
    
    
      By lem:mgd-deps, the dependencies of  are those of a most general dualizer , so it suffices
    
      to show that x y if and only if (x)=y.
    
      Since every predicate symbol in  is unary,  is the transitive closure of the unification problem  (see the proof of lem:mgd).
    
    Thus the dualizer  defined in the proof of lem:consistent-dualizable is most general, and by construction x y if and only if (x)=y.
    
    Note that the above lemmas simplify the definition of (standard, non-homogeneous) monadic combinatorial proof :→:
    
    
      *  Instead of checking for the existence of a dualizer for (the rectified form of) , we merely check that  is consistent, via the variable relation , using lem:consistent-dualizable.
    
      *  Instead of building the leap graph  with dependencies via a dualizer,
    
    we read dependencies directly from , using lem:monadic-deps.
    
    
      §.§.§ The linked mograph of a linked closed monadic fograph
    
    The linked mograph of a linked closed monadic fograph  is the linked mograph  with
    
    
      * =,
    
      * =,
    
      * 
    if and only if
    , is a link
    
      *  if and only if
    
     binds .
    
    
     is a well-defined linked mograph for every linked closed monadic fograph .
    
    Let λ_1,…,λ_n be the links of  for λ_i=_i,_i.
    
    Choose distinct predicate symbols p_1,…,p_n, and define  by replacing the predicate symbols in the labels of _i and _i by p_i and _i, respectively.
    
    By construction, =, and
    
    since two literals in  are pre-dual in  if and only if they constitute a link,
    
    we have =.
    
    Thus = which is a well-defined mograph by lem:mograph-of-fograph-well-defined.
    
    Since the p_i are distinct, every literal of  is in a unique duality, so  is linked.
    
    
    
    A linked closed monadic fograph  is a fonet if and only if its linked mograph  is a monet.
    
    
    Without loss of generality we may assume  is rectified.
    
    By lem:consistent-dualizable,  has a dualizer if and only if it is consistent in the sense of Def. <ref>, and consistency of  coincides with consistency of  (Def. <ref>).
    
    By lem:monadic-deps the dependencies of  are those pairs x,y of variables with x existential, y universal and x y,
    
    which, by definition of , correspond to pairs _x,_y of binders in  with _x and _y the unique binders corresponding to the variables x and y, and _x_y.
    
    Thus the leap graphs of  and  are the same, so  has an induced bimatching if and only if  has an induced bimatching.
    
    
    
      §.§.§ Proof of monadic homogeneous combinatorial soundness
    
    
    Recall that, by definition of , = for every closed monadic fograph .
    
    
    Let  be a closed monadic fograph.
    
    A vertex is a literal in  if and only if it is a literal in the mograph .
    
    
    Immediate from the definition of the binding set  (Def. <ref>) and that, by definition,
    a vertex is a literal in a mograph if and only if it is the target of a binding.
    
    
    
    Let  be a closed monadic fograph.
    A binder is universal in  if and only if it is universal in the mograph .
    
    
    By definition =, and in both cases,
    a binder is universal if and only if its scope contains no edge.
    
    Define the type∈ of a vertex 
    in a mograph or fograph  as  if  is a literal,  if  is a universal binder, and  if  is an existential binder.
    
    
    For every closed monadic fograph , = for every vertex .
    
    
    Lemmas <ref> and <ref>.
    
    
    Every mograph skew bifibration :→ preserves vertex type, , =() for every vertex  in .
    
    
    
    A vertex is a literal if and only if it is the target of a binding, and
    
    since :→ is a fibration,
    
    a vertex  in  is the target of a binding if and only if () is the target of a binding.
    
    Thus  maps literals to literals and binders to binders.
    
    By definition (Def. <ref>) a skew bifibration maps existential binders to existential binders,
    
    so it remains to show that universal binders map to universal binders.
    
    This follows from the proof of lem:pres-universals, which applies in the homogeneous setting because it does not depend on labels.
    
    
    
    A closed monadic formula is valid if it has a homogeneous combinatorial proof.
    
    
    Suppose
    :→=
    is a homogeneous combinatorial proof of the monadic formula .
    
    Without loss of generality, we may assume  is collapsed, by lem:collapse.
    
    Define  as the
    coloured labelled cograph with
    =,
    =,
    a colour , for each ∈,
    and
    the label of  in  defined as
    the label of () in ,
    
    where ()∈ can be viewed as a vertex in
     since
    = by lem:prop-factorization and, by definition of  (Def. <ref>),
    = for any closed monadic fograph .
    
    We claim that  is a well-defined fograph (Def. <ref>, p. def:fograph).
    
    By lem:types,
    
    =
    so by lem:mograph-bifib-preserves-literals,
    = (since the label of  in  is that of () in ).
    
    Thus  has a literal since  has one (because it is a mograph), so  is a logical cograph.
    
    We must show, for all variables x, that every x-binder  is legal,
    , the scope of  contains
    
    (a) at least one literal and (b) no other x-binder.
    
    For (a), the scope  of  in a fograph or mograph  depends only on the underlying cograph , so
    
    =.
    Thus  has a literal because  does (since  is a mograph).
    
    For a contradiction to (b), Suppose  were an x-binder in .
    
    Let  be the cotree  and let  be the parent of  in .
    
    If  is existential, then  (since, by lem:scope-parent, all distinct vertices in the scope of an existential binder are in an edge, since  is a  node in ),
    contradicting ()=() (which holds because, without loss of generality,  is rectified, so there is a unique x-binder in ).
    
    Otherwise  is universal.
    
    Since ∈, by lem:scope-parent
    we have
    
    ,
    
    ,
    , with  a -node, since  is universal.
    
    Because  is collapsed and ()=(),
    we cannot have
    
    (otherwise  and  would be indistinguishable, contradicting  being collapsed),
    
    thus
     for some vertex .
    
    Since  and  is a graph homomorphism we have
    ()1mu(),
    so
    ()1mu()
    (because ()=()).
    
    Since  is a skew fibration, there exists  such that
    ∈ and ()1mu()∉.
    
    Because ∈, the meet  is a ,
    , =,
    and since the parent  of  is a ,
    we have ,
    hence
    .
    
    Therefore , so ()1mu()∈ a contradiction.
    
    Thus we have proved that  is a well-defined fograph.
    
    Since every literal label in  comes from ,  is monadic, and since  is a directed graph fibration
    →,  is closed.
    
    By construction, = (Def. <ref>),
    so by lem:fograph-mograph-net,  is a fonet.
    
    Since :→ is a skew bifibration of mographs,
    :→ is a skew bifibration of fographs,
    hence a (standard) combinatorial proof,
    so  is valid by Theorem <ref>.
    
    Give non-collapsed example
    The crux of the soundness proof above is to transform a collapsed monadic homogeneous combinatorial proof into a standard combinatorial proof.
    
    The following example shows why collapse occurs before this transformation.
    
    A monadic homogeneous combinatorial proof of the closed monadic formula  is shown below-left.
    
    -.32.4(-4,0)(0,0)(4,0)
    Its collapse, also a monadic homogeneous combinatorial proof (by lem:collapse), is shown above-centre.
    
    Above-right is the standard combinatorial proof constructed from the collapse in the soundness proof above.
    
    Observe that, were we to attempt to construct a standard combinatorial proof directly from the uncollapsed form,
    it would have two source vertices above  in the target,
    each implicitly labelled x (implicit since we are drawing the skeleton),
    so the source would have a (universal) x-binder in the scope of another x-binder and therefore fail to be a well-defined fograph.
    
    Collapse is directly related to the deletion of select universal binders in the interpretation of the  rule as an operation in <ref>.
    
    
    Every valid closed monadic formula has a homogeneous combinatorial proof.
    
    
    Let  be a valid closed monadic formula.
    
    By Theorem <ref> there exists a (standard) combinatorial proof :→.
    
    Let  be the linked mograph obtained from  with =, =,
    
     if and only if and , is a link (colour) in ,
    and
    = (, ∈ if and only if  binds  in ).
    
    Since there are no logical constants in  there are none in  (by label-preservation of ),
    so every literal in  is in exactly one link.
    
    Thus every literal of  is in a unique duality, no binder of  is in a duality,
    
    and  has no induced bimatching because  is a fonet;
    thus  is a monet.
    
    Let ==.
    
    We claim that :→ is a homogeneous combinatorial proof, ,
    (1)  preserves existential binders,
    (2) :→ is a skew fibration,
    (3) :→ is an undirected graph homomorphism,
    and
    (4) :→ is a directed graph fibration.
    
    (1) holds because :→ preserves existential binders, and by construction the existential binders of  and  coincide, as do those of  and .
    
    By definition (2) holds if :→ is a skew fibration, which is true because  is a skew bifibration,
    =, and
    =.
    
    For (3), suppose . Since  is a fonet, it has a dualizer, so the labels of  and  are dual, say, p and , respectively.
    
    Because  preserves labels, () and () are labelled p and , thus ()2mu()∈, and (3) holds.
    
    (4) holds because :→ is a skew bifibration, thus :→ is a directed graph fibration, and by construction = and
    =.
    
    
    
    Lemmas <ref> and <ref>.
    
    
    
    § HOMOGENEOUS SURJECTIONS
    
    
    Recall from <ref> that  is a surjection from rectified formulas onto rectified fographs (Lem. <ref>),
    
    and that  is a surjection from clear formulas onto fographs (Lem. <ref>).
    
    This section exhibits similar surjections onto duality graphs and mographs.
    
     is a surjection from simple propositional fographs onto dualizing graphs.
    
    
    
      Let  be a dualizing graph.
    
    We construct a fograph  such that =.
    
    Define = and =, with a nullary predicate symbol label on each vertex defined as follows.
    
    Since  is P_4-free and -free, it is a disjoint union of complete bipartite graphs[Recall that a complete bipartite graph is one of the form  for edgeless graphs  and .]_1,…,_n.
    
    Choose distinct nullary predicate symbols p_1,…,p_n such that _i p_j (1 i,j n).
    
    If _i has no edges, it has a single vertex v_i; assign p_i as the label of v_i.
    
    Otherwise, _i=_i'_i” for _i' and _i” without edges.
    
    Assign the label p_i to every vertex in _i' and the label _i to every vertex in _i”.
    
    The graph  is a non-empty cograph with vertices labelled by nullary predicate symbols, hence  is a simple propositional fograph.
    
    By construction, =.
    
    
    
    The function  from simple propositions to dualizing graphs (Def. <ref>) is a surjection.
    
    
    
    By lem:graph-surj is a surjection from (rectified) formulas onto fographs.
    
    The restriction of  to simple propositions is a surjection onto simple propositional fographs.
    
    Since =∘ by lem:prop-factorization, and  is a surjection by lem:surj-prop-fographs-to-dualizing-graphs,  is a surjection.
    
     is a surjection from closed monadic fographs onto mographs.
    
    
    
    Let  be a mograph.
    
    We will construct a closed monadic fograph  with =.
    
    Define = and =, and define the predicate symbol in the label of each vertex of  exactly as in the proof of lem:surj-prop-fographs-to-dualizing-graphs, only this time we shall make each such predicate symbol p unary rather than nullary by adding a variable after p. For each binder  in , choose a distinct variable x_, set the label of  to x_, and for every literal  with ∈, add the variable x_ to the label of  as the argument of the predicate symbol already assigned to .
    
    Since every binder in  has non-empty scope, every binder in  has non-empty scope.
    
    By construction every literal label is a unary predicate symbol followed by a variable, so  is monadic.
    
    Because every variable x_ is distinct for each binder , no literal in  can be bound by two binders in .
    
    Thus  is a rectified monadic fograph.
    
    Since, by definition of a literal in a mograph, every literal in  is the target of a binding in , every literal in  is bound, so  is closed.
    
    By construction, =.
    
    
    The function  from closed monadic formulas to mographs (Def. <ref>) is a surjection.
    
    
    
    By lem:graph-surj is a surjection from (rectified) formulas onto fographs.
    
    The restriction of  to closed monadic formulas is a surjection onto closed monadic fographs.
    
    Since =∘ by lem:monadic-factorization, and
     is a surjection by lem:surj-closed-monadic-fographs-to-mographs,  is a surjection.
    
    
    
    § POLYNOMIAL-TIME VERIFICATION
    
    
    In this section we show that a combinatorial proof can be verified in polynomial time.
    
    Thus combinatorial proofs constitute a formal proof system<cit.>.
    
    The size of a graph  is the sum of the number of vertices in  and the number of edges in .
    
    
    The dependencies of a linked rectified fograph  can be constructed in time polynomial in the size of .
    
    
    Let x_1,…,x_n be the existential variables in .
    
    The main unification algorithm of <cit.> provides in linear time an assignment x_1u_1,…,x_nu_n with x_i not in u_j for i j, such that the most general unifier σ
    is x_1t_1,…,x_nt_n for
    t_i=u_i
    x_i+1u_i+1…x_nu_n
    (the sequential composition of n i one-variable substitutions applied to u_i).
    
    Let y_i1,…,y_im_i be the set of variables occurring in u_i,
    
    and define u'_i as f_iy_i1… y_im_i for a fresh m_i-ary function symbol f_i.
    
    The assignment σ'=x_1t'_1,…,x_nt'_n for
    t'_i=
    u'_i
    x_i+1u'_i+1…x_nu'_n
    has the same dependencies as σ but can be constructed in polynomial time since each x_j appears at most once in each u'_i.
    
    The above proof is essentially the first part of the proof of Theorem 3 in <cit.>.
    
    
      The correctness of fonet can be verified in time polynomial in its size.
    
    
    Let  be a fonet of size n.
    
    By lem:deps-ptime we can construct all dependencies of  in polynomial time, hence the leap graph  in polynomial time.
    
    By lem:fonet-constructible every fonet is constructible from axioms by fusion and quantification.
    
    Since there can be at most n fusions and/or quantifications, it suffices to show that each step in the inductive decomposition of a fonet in the proof of lem:fonet-constructible can be performed in polynomial time.
    
    In the first case the proof of lem:fonet-constructible,  has no edges (which can be determined in polynomial time), and to confirm that  is a union of axioms takes polynomial time.
    
    In the second case,  is universal, and the universal binder can be found and deleted in polynomial time, by inspecting each vertex of  in succession.
    
    In the final case,  is not universal and has at least one edge, and we seek to decompose  as a fusion or existential quantification via lem:split-fusion-existential.
    
    Henceforth we follow the proof of lem:split-fusion-existential closely.
    
    The graph  in the proof of lem:split-fusion-existential can be constructed in polynomial time from the cotree,
    which can built in polynomial time <cit.>.
    
    The bridge _m_m+1 can be located in polynomial time (by iterating through the edges of ),
    and _1 and _2 can be determined in polynomial time by traversing edges.
    The underlying fograph  of
    
    
    is
    _1(_m_m+1)_2.
    
    Depending on whether both _m and _m+1 both contain literals, the proof of lem:split-fusion-existential now provides either  as a fusion of _1_m and _m+1_2, and we recurse with each half of the fusion, or =, and we delete the existential binder  and recurse with .
    
    
    Define the size of a combinatorial proof :→ as the sum of the size of  and the size of .
    
      The correctness of a combinatorial proof can be verified in time polynomial in its size.
    
    
      Let :→ be a combinatorial proof.
    
      By lem:fonet-ptime the fonet  can be verified in polynomial time.
    
      Verifying that  is a skew bifibration is polynomial time because the skew fibration and directed graph fibration conditions apply to pairs of vertices, one in  and one in , seeking the existence of a vertex in , which can be found be iterating through each vertex of  in turn.
    
    
    § CUT COMBINATORIAL PROOFS
    
    
    Just as sequent calculus proofs may include cuts <cit.>, combinatorial proofs can be extended with cuts.
    
    Define an n-cut combinatorial proof of a formula  as a combinatorial proof of
    
     for (arbitrary) formulas _1,…,_n.
    
    Each formula _i_i is a cut.
    
    A cut combinatorial proof is an n-cut combinatorial proof for some n 0; if n=0 the combinatorial proof is cut-free.[We can define a cut combinatorial proof of a sequent similarly.]
    
    A formula is valid if and only if it has a cut combinatorial proof.
    
    
    Since
    ∨(_1_1)∨…∨(_n_n) is valid if and only if  is valid,
    the result follows from Theorem <ref>.
    
    
    § SEMI-COMBINATORIAL PROOFS
    
    
    Using the surjections
     (Def. <ref>) from (implicitly rectified) formulas onto rectified fographs
    and
     (Def. <ref>) from clear formulas onto fographs,
    
    given a combinatorial proof :→, such as the one whose skeleton is drawn below-left (copied from the Introduction),
    by choosing
    a rectified formula  with =
    and
    a clear formula  with  equal to the underlying uncoloured fograph of ,
    we can render  in the form below-centre.
    
    
    -.92.9(-5,0)(0,-.25)(0,0)(5,0)
    
    We have drawn the bifibration between the quantifier variables and predicate symbols of the formulas = and
    = corresponding to the vertices of  and ,
    and replaced the link (coloured pair of vertices) on  with a three-segment edge between the dual predicate symbols  and p in , in the style of proof nets for linear logic <cit.>.
    
    Above-right we have simplified the presentation further by removing redundant bifibration edges between quantifier variables (since they can be left implicit due to label-preservation, , both occurrences of the existential quantifier variable x in the source map to the (unique) existential quantifier variable x in the target), and we have drawn non-dotted edges.
    
    We have also replaced the formula  with the corresponding sequent
    , and suppressed the comma of the sequent.
    
    We call this presentation of a combinatorial proof a semi-combinatorial proof, a first-order generalization of the propositional case in <cit.>.[The source sequent, with links, can be viewed as generalization of a unification net <cit.>. See <ref> for details.]
    
    § CONCLUSION AND RELATED WORK
    
    
    This paper reformulated classical first-order logic with combinatorial rather than syntactic proofs (<ref>–<ref>),
    
    extending the propositional case of <cit.> to quantifiers.
    
    The proof of soundness (<ref>) was more intricate than
    that of the propositional case <cit.>.
    
    In the logical-constant-free propositional, monadic and S5-modal special cases, labels
    can be removed from a combinatorial proof, and colouring from the source,
    for a homogeneous form (<ref>–<ref>).
    
    Propositional combinatorial proofs are related to sequent calculus <cit.> in <cit.> and <cit.>,
    and to other syntactic systems (including resolution and analytic tableaux) in <cit.> and <cit.>.
    
    Skew fibrations are decomposed as propositional structural maps (composites of contraction and weakening maps) in <cit.> and <cit.>.
    
    Combinatorial proofs may provide an avenue towards tackling Hilbert's 24th problem <cit.>.
    
    Combinatorial proofs for non-classical logics are being pursued actively. For example,
    combinatorial proofs for propositional intuitionistic logic are presented in <cit.>.
    
    A potential topic of future research is first-order intuitionistic combinatorial proofs.
    
    Cut elimination procedures for propositional cut combinatorial proofs are presented in <cit.> and <cit.>.
    
    Natural open questions include the extension of propositional intuitionistic combinatorial proofs to first-order,
    
    and cut elimination procedures for first-order combinatorial proofs (classical and intuitionistic).
    
    The function  from first-order formulas to fographs (Def. <ref>)
    is a first-order extension of the propositional translation G of <cit.>.
    The latter is well-known in graph theory, as the function from a (prime-free) modular decomposition tree <cit.> or cotree <cit.> to a cograph, and is employed in logic and category theory. For example, <cit.> uses G with
    ∧ and ∨⊕ in linear logic, <cit.> uses G with ∧ and ∨ as product and coproduct for free bicompletion (and emphasizes the -freeness of the image), and <cit.> uses G with ∧⊗ and ∨ in linear logic.
    
    That cographs are exactly the P_4-free graphs is proved in <cit.>.
    
    Links between pre-dual literals in fonets, which become dual only after applying a dualizer or unifier,
    are akin to the
    first-order connections or matings employed in automated theorem proving <cit.>.
    
    Bibel in <cit.> proposed link as an alternative name for a connection,
    and we have adopted that terminology.
    
    Since combinatorial proofs can be verified in polynomial time (<ref>), they constitute a formal proof system<cit.>,
    
    in contrast to the connection and mating methods.
    
    The roots of first-order connections/matings
    
    go back to Herbrand <cit.>, Quine <cit.>, Robinson <cit.> and Prawitz <cit.>, amongst others.
    
    Propositional links between dual literals can be found in
    
    <cit.>,
    and sets of such propositional links form a category <cit.> via path composition.
    
    The pairing of dual propositional occurrences can be found in the study of other forms of syntax, such as
    closed categories <cit.> (see also <cit.>),
    contraction-free predicate calculus <cit.> and linear logic <cit.>.
    
    A fonet can be viewed as a graph-theoretic abstraction and generalization of
    a unification net <cit.>,
    which in turn abstracts proof nets for first-order multiplicative linear logic <cit.>.
    
    The sense of generalization is that fographs admit the multiplicative mix rule /, interpreted as the fusion operation with empty portions (, disjoint union).
    
    The relationship with a unification net is made clearer when rendering a combinatorial proof in semi-combinatorial form,  as in <ref>. (For example, in the right-most example at the start of <ref>, the source is exactly a unification net in the sense of <cit.>.)
    
    Unification nets are also available for first-order additive linear logic <cit.>.
    
    Upon forgetting vertex labels, propositional fonets correspond to the nicely coloured cographs of <cit.>,
    and nicely coloured cographs without singleton colours are in bijection with the even-length alternating elementary acyclic R&B cographs of <cit.>.
    
    An additional constraint on fonets can be applied to reject the mix rule, and retain soundness and completeness ( the alternating elementary connectedness condition of <cit.>).
    
    Abstract representations of first-order quantifiers with explicit witnesses are in <cit.> (extending expansion
    trees <cit.>) and <cit.> (for classical logic) and <cit.> (for additive linear logic).
    
    Composition of witnesses is analysed in <cit.> and <cit.>.
    
    Proof nets <cit.> were extended to propositional classical
    logic in <cit.> (developed in detail in <cit.>).
    
    The paper <cit.> fixes issues of redundancy due to contraction and weakening nodes
    and relates classical propositional proof nets to propositional combinatorial proofs <cit.>.
    
    Peirce <cit.> provides an early graphical representation of propositional formulas.
    
    
    
    § FOGRAPH EXAMPLES
    Figures <ref> and <ref>
    show a progression of examples of fographs  for various formulas .alpha
