We developed, and computer-checked by means of the Ref verifier, a formal proof that every weakly extensional, acyclic (finite) digraph can be decorated injectively a` la Mostowski by finite sets so that its arcs mimic membership. We managed to have one sink decorated with ∅ by this injection. We likewise proved that a graph whatsoever admits a weakly extensional and acyclic orientation; consequently, and in view of what precedes, one can regard its edges as membership arcs, each deprived of the direction assigned to it by the orientation. These results will be enhanced in a forthcoming scenario, where every connected claw-free graph G will receive an extensional acyclic orientation and will, through such an orientation, be represented as a transitive set T so that the membership arcs between members of T will correspond to the edges of G.
arcs reflect the membership relation. Under this change of perspective, a fully
formal reconstruction of those results became affordable and, once carried out,
was certified correct with the Ref proof-checker [
Can we, with equal ease, formalize in Ref the Milaniˇc-Tomescu representation result per se? That result is the claim that for every connected claw-free graph G there exist a set νG ⊇ S νG and an injection f from the vertices of G onto νG such that {x, y} is an edge of G if and only if either f x ∈ f y or f y ∈ f x holds. The proof articulates as follows: 1. One shows that for any graph G = (V, E) as said, there is a D ⊆ V × V such that E = {x, y} : [x, y] ∈ D and (V, D) is an acyclic digraph which is extensional: i.e., no two vertices in V have the same out-neighbors. 2. One decorates vertices by putting f v = {f w : [v, w] ∈ D} `a la Mostowski, for all v ∈ V . Acyclicity ensures that this recursion makes sense; extensionality ensures the injectivity of f .
As a preparatory, simpler formalization task, we have proved with Ref that a graph G whatsoever admits a set νG and an injection f from the vertices of G onto νG such that {x, y} is an edge of G if and only if either f x ∈ f y or f y ∈ f x holds. We could not have insisted on the transitivity condition νG ⊇ S νG here, because we have nohow restrained G. The proof now articulates as follows: 10. For any G = (V, E), there is a D ⊆ V × V s.t. E = {x, y} : [x, y] ∈ D and (V, D) is an acyclic digraph which is weakly extensional: i.e., any two vertices that share the same out-neighbors have no out-neighbors. 20. We decorate vertices by putting: f v = {f w : [v, w] ∈ D } for each v ∈ V endowed with out-neighbors, f z = ∅ for one sink z, and f u = {V } ∪ V \ {u} for each sink u 6= z. (Notice that 20. subsumes 2. altogether, because an extensional digraph has exactly one sink.) 2
Ingredients of a Ref ’s scenario
What one submits to the Ref checker, to have its correctness verified, is a
scenario: namely, a script file consisting of definitions and of theorems endowed
with their proofs; a construct, named Theory , enables one to package
definitions and theorems into reusable proofware components. A variant of the
Zermelo-Fraenkel set theory, postulating global choice, regularity, and infinity,
underlies the logical armory of Ref: this is apparent from the fifteen or so
inference rules available in the proof-specification language (see [5, Sec. 3]), of
which only a few sprout directly from first-order predicate calculus, while most
embody some form of set-theoretic reasoning. Multi-level syllogistic [
Our figures offer a glimpse of the Ref’s language. Fig. 1 shows the definitions of graph-theoretic notions relevant to the proof-checking experiment on which Def acyclic: [Acyclicity] h∀w ⊆ V | w 6= ∅ → h∃t ∈ w | ∅ = {y ∈ w | [t, y] ∈ D} ii
Def xtens0: [Extensionality] h∀x ∈ V, y ∈ V, ∃z | ([x, z] ∈ D ↔ [y, z] ∈ D) → x = yi
Def xtens1: [Weak extensionality] WExtensional(V, D) ↔Def
Extensional V ∩ domain(D ∩ (V × V)), D ∩ (V × V) Def orien: [Orientation of a graph]
E ∩ {{x, y} : x ∈ V, y ∈ V\ {x}} = nnp[
Def Finite : [Finitude]
h∀g ∈ P(PF)\ {∅} , ∃m | g ∩ Pm = {m} i
h∀p ∈ F | p = hp[
Is map(F) & h∀p ∈ F, q ∈ F | p[
APPLY h i finiteImage s0 7→ f1, f(X) 7→ X[
Use def(domain) ⇒ false
Discharge ⇒ Auto
hf1i,→T svm2 ⇒ f1 = {[x, f1 x] : x ∈ domain(f1)}
APPLY h i finiteImage s0 7→ domain(f1), f(X) 7→ [x, f1 x] ⇒
Finite({[x, f1 x] : x ∈ domain(f1)})
nx[
Theory finiteImage s0, f(X)
Finite(s0) ⇒
Finite {f(x) : x ∈ s0} End finiteImage
Theory finiteInduction s0, P(S)
Finite(s0) & P(s0) ⇒ (finΘ)
h∀S | S ⊆ finΘ → Finite(S) & P(S) ↔ S = finΘ i
End finiteInduction The two Theorys in which our experiment culminates are shown in Fig. 5; the key theorem which makes the second of them derivable from the first was stated in Ref as follows:
Due to its centrality in our scenario, we wish to briefly sketch the proof of the orientability theorem just cited. Arguing by contradiction, suppose that there Theory finMostowskiDecoration(v0, d0)
v0 × v0 ⊇ d0 & v0 6= ∅ & Finite(v0) & Acyclic(v0, d0) & WExtensional(v0, d0) ⇒ (mskiΘ)
Svm(mskiΘ) & domain(mskiΘ) = v0
h∀w | w ∈ domain(d0) → mskiΘ w = nmskiΘ p[
e0 ⊆ {{x, y} : x ∈ v0, y ∈ v0\ {x}} & v0 6= ∅ & Finite(v0) ⇒ (wskiΘ)
Svm(wskiΘ) & domain(wskiΘ) = v0 & ∅ ∈ range(wskiΘ) h∀y | y ∈ range(wskiΘ) → Finite(y)i h∀x, y | {x, y} ⊆ v0 & wskiΘ x = wskiΘ y → x = yi h∀x, y | {x, y} ⊆ v0 → (wskiΘ y ∈ wskiΘ x ∨ wskiΘ x ∈ wskiΘ y) ↔ {x, y} ∈ e0 i h∀x | wskiΘ x ∩ range(wskiΘ) 6= ∅ → wskiΘ x ⊆ range(wskiΘ)i End finGraphRepr is a counterexample; then, exploiting the finiteness hypothesis, take a minimal counterexample v1, s1, e0. We are supposing that there is no acyclic, weakly extensional orientation of the graph v1, e0 ∩ {x, y} : x ∈ v1, y ∈ v1 \ {x} having s1 as a source; whereas, for every v0 ( v1, one can orient v0, e0 ∩ {x, y} : x ∈ v0, y ∈ v0 \ {x} in an acyclic and weakly extensional way, for any vertex t ∈ v0, so that t plays the role of a source. Let, in particular, v0 = v1 \ {s0}. Unless s1 is an isolated vertex, an acyclic and weakly extensional orientation of v0 exists that has as a source a chosen neighbor t1 of s1. However, that orientation could trivially be extended to the graph with vertices v1 so that s1 becomes a source; this contradiction shows that s1 cannot have neighbors in v1, which is also untenable: if so, any orientation for v0 would in fact work also as an orientation for v1 and, as such, would have s0 as a source.
The full Ref scenario can be seen at http://www2.units.it/eomodeo/wERS. pdf (cf. also http://www2.units.it/eomodeo/ClawFreeness.html). 4
Planned work on representing claw-free graphs The larger experiment we have in mind will associate with each connected clawfree graph G = (V, E) an injection f from V onto a transitive, hereditarily finite set νG so that {x, y} ∈ E if and only if either f x ∈ f y or f y ∈ f x.
The new notions entering into play can be rendered formally as follows: ClawFreeG(V, E)
Connected(E)
h∀ p | HerFin(S) ↔Def h∀w, x, y, z | {w, x, y, z} ⊆ V & {{w, y} , {y, x} , {y, z}} ⊆ E →
(x = z ∨ w ∈ {z, x} ∨ {x, z} ∈ E ∨ {z, w} ∈ E ∨ {w, x} ∈ E)i , ↔Def ∅ ∈/ E ∧
S p = E ∧ h∀b ∈ p, c ∈ p | S b ∩ S c 6= ∅ ↔ b = ci → p = {E}i , ↔Def Finite(S) & h∀x ∈ S | HerFin(x)i .
Here, the first definiens requires that no subgraph of (V, E) induced by four vertices has the shape of a ‘Y’. The second definiens requires that the set E of edges can nohow be split into multiple disjoint blocks so that no edge acts as a ‘bridge’ by sharing endpoints with edges in distinct blocks. Hereditary finitude is a recursive notion.
We aim at getting the analogue, shown in Fig. 6, of Theory finGraphRepr (cf. Fig. 5). For that, we must again exploit Theory finMostowskiDecoration; in addition, a key theorem will ensure the acyclic extensional orientability of a connected and claw-free graph: Theorem cClawFreeG2. Finite(V) & Connected(V, E) &
ClawFreeG(V, E) & E ⊆ {{x, y} : x ∈ V, y ∈ V\ {x}} →
h∃d ⊆ V × V | Orientates(d, V, E) & Acyclic(V, d) & Extensional(V, d)i. Theory herfinCCFGraphRepr(v0, e0) e0 ⊆ {{x, y} : x ∈ v0, y ∈ v0\ {x}} & Finite(v0)
Connected(v0, e0) & ClawFreeG(v0, e0) ⇒ (transΘ)
Svm(transΘ) & domain(transΘ) = v0 h∀x, y | {X, Y} ⊆ v0 & transΘ X = transΘ Y → X = Yi h∀x, y | {X, Y} ⊆ v0 →
(transΘ Y ∈ transΘ X ∨ transΘ X ∈ transΘ Y ↔ {X, Y} ∈ e0)i {y ∈ range(transΘ) | y 6⊆ range(transΘ)} = ∅ range(transΘ) 6= ∅ & HerFin(range(transΘ)) End herfinCCFGraphRepr
Another fact we must exploit is that every connected graph has a vertex whose removal (along with all edges incident to it) does not disrupt connectivity. The existence of such a non-cut vertex is easily proved for a tree. So, in order to cheaply achieve our goal, we will define
HankFree(T)
Is tree(T) ↔Def h∀e ⊆ T | e = ∅ ∨ h∃ a ∈ e | a 6⊆ S(e \ {a})ii , ↔Def Connected(T) ∧ HankFree(T) and—if only provisionally—recast the connectivity assumption, Connected(v0, e0), of Theory herfinCCFGraphRepr as the assumption that (v0, e0) has a ‘spanning tree’:
h∃t | Is tree(t) & St = v0 & (v0 = {arb(v0)} ∨ t ⊆ e0)i .
This eases things: for, any vertex with fewer than 2 incident edges in the spanning tree of a connected graph will be a non-cut vertex of the graph.