Reasoning about connectivity without paths? Alberto Casagrande Eugenio Omodeo acasagrande@units.it eomodeo@units.it Dep. of Mathematics and Geosciences University of Trieste Trieste, Italy Abstract. In graph theory connectivity is stated, prevailingly, in terms of paths. While exploiting a proof assistant to check formal reasoning about graphs, we chose to work with an alternative characterization of connectivity: for, within the framework of the underlying set theory, it requires virtually no preparatory notions. We say that a graphs devoid of isolated vertices is connected if no subset of its set of edges, other than the empty set and the set of all edges, is vertex disjoint from its complementary set. Before we can work with this notion smoothly, we must prove that every connected graph has a non-cut vertex, i.e., a vertex whose removal does not disrupt connectivity. This paper presents such a proof in accurate formal terms and copes with hypergraphs to achieve greater generality. 1 Introduction Connectivity plays a crucial role not only in graph theory, but also in topology. The number of connected components of a graph is a topological invariant, it corresponds to the multiplicity of the eigenvalue 0 in the Laplacian matrix that represents the graph, and, in the recent years, it has been related to the number of claw-free subgraphs of the graph itself [1]. Because of the ubiquity of this notion, it deserves an autonomous and insightful treatment in a large scale formalization effort, such as the one envisioned in [8] or in [6]. Non-cut vertices are vertices whose removal preserves the graph connectivity. The notion of connectivity is traditionally given in term of paths, and in such terms one proves that any graph contains non-cut vertices. These vertices are largely used in inductive proofs over connected graphs: the pattern is to apply the inductive hypothesis to a graph deprived of a non-cut vertex and, then, to prove that the investigated property is retained when the vertex is reinstated. While formally defining the notion of path is not really a problem, from a foundational point of view, it appears to be an out-of-focus effort in this context: it would in fact bring into play notions (e.g., natural numbers) which are barely related to the theme of discourse. ? This work has been partially supported by Istituto Nazionale di Alta Matematica (INdAM). 93 A.Casagrande et al. Reasoning about connectivity without paths This paper exploits a path-free notion of connectivity to formally prove that connected undirected hypergraphs are always endowed with non-cut vertices. Our immediate motivation for undertaking this study on connectivity is a formalization task that has been successfully carried out recently with the assistance of the proof checker Referee/Ætnanova [6]: as reported in [5], taking advantage of the Milanič and Tomescu representation theorem for connected claw-free graphs [4], we could achieve with relative ease the proof that any such graph owns a near-perfect matching and has a Hamiltonian cycle in its square. We took it for granted that every connected graph has a spanning tree. This left us with a proof obligation, and since the existence of a spanning tree plainly reduces to the proof that every connected graph has a non-cut vertex, we are now beginning to fill the gap, with the formalization task on which we will report below. This paper is organized as follows: Section 2 introduces the notation and all the needed notions. Section 3 formalizes the result aimed at and splits the proof of it into multiple steps that are detailed in Sections 3.1, 3.2, and 3.3 ( some basic properties and technical lemmas are proved in the appendix). Finally, Section 4 draws our conclusions and suggests future work. 2 Preliminaries We work with in the Zermelo-Fraenkel set theory (ZF) and all the notions treated in this paper are defined through it. Besides the standard Boolean propositional functions (i.e., ∧, ¬), the used formal language provides intersection (∩), union (∪), and difference (\) over sets as well as both the membership (∈) and inclusion (⊇) relations. From a formal point of view, the Boolean functions ∨ and → and the relations over sets <, ), ⊆, (, =, and , are shortcuts for non-atomic formulæ whose semantics is the standard one. While the notion of cardinality of a set is not formally included in the adopted language, it is worthwhile to introduce the relation |·|≥n that associates each finite set with the number of elements belonging to it. This relation is not really necessary, but it enables more natural definitions for the subsequent notions. The relation |·|≥n is defined as: ( > if n = 0 |S|≥n D ∃v ∈ S |S \ {v}|≥n−1 otherwise It is easy to see that, for any natural number n ∈ N and any set S, |S|≥n holds if and only if |S| ≥ n. We characterize finitude as proposed by Tarski [7]: a set S is finite if and only if every not empty class of subsets of S contains an element which is minimal with respect to ⊆. This clue is captured by the following definition Finite (S) D ∀P ∈ ℘(℘(S)) \ {∅} ∃M ℘(M) ∩ P = {M}. Tarski himself proved that if S is finite then every not empty class of subsets of S contains also a maximal element [7]. The basic notions of (hyper)graph, edge, and node are defined as follows. 94 A.Casagrande et al. Reasoning about connectivity without paths Definiton 1 An edge is a finite set endowed with at least two elements. A hypergraph G is a finite set of edges, i.e., Graph (G) D Finite (G) ∧ ∀e ∈ G |e|≥2 ∧ Finite (e) . The elements of the edges of G are called nodes, or vertices, of G. By standard terminology, the word graph refers to hypergraphs whose edges have cardinality 2. However, we take the freedom to abbreviate “hypergraph” into “graph” because this work deals exclusively with the more general notion. In accordance with the literature (e.g., see [2, 3]), our definition does not allow graphs to have self-loops, namely singleton edges, and it explicitly requires that each of the edges contains at least 2 distinct elements. Any subset of a graph is a graph. Lemma 1 P ⊆ G ∧ Graph (G) → Graph (P) Proof. The claim follows directly from the definition of Graph (·). Let Nodes (G), Cov (G, P), and Contains (G, v) represent the set of nodes of G, the set of edges in G that share nodes with any edge in P, and the set of edges in G that contain the node v. More formally, def [ def Nodes (G) = e Cov (G, P) = {e ∈ G | e ∩ Nodes (P) , ∅} e∈G def Contains (G, v) = {e ∈ G | v ∈ e} If Contains (G, v) is a singleton, then v is said to be a boundary vertex. f f f a b a b a b g g g c c c h h h d e d e d e (a) A graph P ⊆ G (b) Cov (G, P) (c) Contains (G, a) Fig. 1: In above figures, ovals represent the elements of G. If, for every nonnull set P ( G, P shares some nodes with the graph G \ P, then G is said to be connected (in short, Conn (G)). Conn (G) D Graph (G) ∧ ∀P (∅ ( P ( G → Nodes (P) ∩ Nodes (G \ P) , ∅) If the graph G is connected and G \ {e} is not connected, then e is said to be a cutting edge. 95 A.Casagrande et al. Reasoning about connectivity without paths f a b c d e Fig. 2: Let G and P be {{a, b}, {a, f }, {c, d, e}, {d, e}} and {{a, b}, {a, f }}, respectively. The graph G is not connected as Nodes (P) ∩ Nodes (G \ P) is empty and P ( G. Let us notice that it is not always the case that by removing a node v from all edges of a graph G we get a graph. As a matter of fact, some of the edges of G that contain v may have cardinality 2. If we remove v from such edges, we obtain sets whose cardinality is 1 and, by definition of edge, these are not edges. For instance, if G contains an edge {a, b} and v is a, then {a, b} \ {a} is {b} which is not an edge because has cardinality 1. Filter (G, v) is the set obtained by first removing v from all edges of G and then filtering out all the resulting sets whose cardinality is less than 2. Since all the elements of Filter (G, v) have cardinality 2 at least, Filter (G, v) is a graph by definition of graph. def Filter (G, v) = {e \ {v} | e ∈ G ∧ |e \ {v}|≥2 } Notice that, if {v, w} is the only edge in G that contains w, then w does not be- long to Nodes (Filter (G, v)). When we write Nodes (G), Cov (G, P), Contains (G, v), or Filter (G, v), we implicitly assume that both of G and P are graphs. Let G and v be a graph and a node, respectively. We define Lost (G, v) to be the set of nodes of G that are not nodes of Filter (G, v) and differ from v. def Lost (G, v) = Nodes (G) \ (Nodes (Filter (G, v)) ∪ {v}) If Lost (G, v) is nonnull, then we say that v is a losing vertex of G and all of its elements are said to be lost by v. Whenever G is connected and either Filter (G, v) is not connected or some of the nodes in G other than v do not belong to Filter (G, v), v is a cut vertex of G (Cutting (G, v) holds). Cutting (G, v) DConn (G) ∧ |G|≥2 ∧ (¬Conn (Filter (G, v)) ∨ Lost (G, v) , ∅) We call non-cut vertex any vertex that is not a cut vertex. 3 Hypergraphs have non-cut vertices Our goal is to provide a proof that every connected hypergraph contains a non-cut vertex. This is encoded by the following corollary. 96 A.Casagrande et al. Reasoning about connectivity without paths f a b b f a b c c d e d e d e (a) A graph G (b) Filter (G, a) (c) Filter (G, c) Fig. 3: The property Cutting (G, v) holds whenever Filter (G, v) is not con- nected or it contains fewer nodes than Nodes (G) \ {v}. Both Cutting (G, a) and Cutting (G, c) do hold since Filter (G, a) lost the node f (see Fig. 3b) and Filter (G, c) is not connected (see Fig. 3c).  Corollary 1 Conn (G) → G = ∅ ∨ ∃v ∈ Nodes (G) ¬Cutting (G, v) We split the proof of above corollary into the proofs of two statements: (1) if G has a losing vertex, then G has is a non-cut vertex (see Section 3.1); (2) any connected hypergraph G contains a node v such that Filter (G, v) is connected (see Section 3.3). By definition of Cutting (·), this suffices to yield the claim of Corollary 1. 3.1 Losing vertices yield non-cut vertices In this section, we prove that, if G has a losing vertex, then it has a non-cut vertex too. The following theorem formalizes this statement. Theorem 1 (Graph (G) ∧ Lost (G, v) , ∅) → ∃v0 ∈ Nodes (G) ¬Cutting (G, v0 ) First of all we need to prove that v is a losing vertex if and only if there exists a vertex lost by v such that Contains (G, v0 ) = {{v, v0 }}. By definition of Filter (·), Filter (G, v) contains all the set e \ {v} such that e is an edge of G and e \ {v} has at least cardinality 2. Hence, v0 , v is a node of G and it is not a node of Filter (G, v) if and only if there exists an edge e ∈ G such that |e \ {v}| < 2. Since e has at least cardinality 2 by definition of Graph (·), we can conclude that e equals {v, v0 }. Lemma 2 Graph (G) → (v0 ∈ Lost (G, v) ↔ Contains (G, v0 ) = {{v, v0 }}) Proof. (→) By definition of Nodes (·), if v0 ∈ Nodes (G), then there exists e ∈ G such that v0 ∈ e. Analogously, if v0 < Nodes (Filter (G, v)), then v0 < e0 for all e0 ∈ Filter (G, v). However, Filter (G, v) = {e \ {v} | e ∈ G ∧ |e \ {v}|≥2 } by definition. Hence, if v0 < Nodes (Filter (G, v)), either v0 < e \ {v} or |e \ {v}| < 2 for all e ∈ G and, if v0 < Nodes (Filter (G, v)) and v0 ∈ Nodes (G), then either v0 = v or |e \ {v}| < 2 for all e ∈ G such that v0 ∈ e. Since |e|≥2 by definition of Graph (·) and v0 ∈ Nodes (G) \ (Nodes (Filter (G, v)) ∪ {v}) holds by hypothesis, e = {v, v0 } for all e ∈ G such that v0 ∈ e. Moreover, {v, v0 } ∈ G because if v0 ∈ Nodes (G) \ (Nodes (Filter (G, v)) ∪ {v}), then v0 ∈ Nodes (G) and there exists e ∈ G such that v0 ∈ e. By definition of Contains (·), it follows that Contains (G, v0 ) = {{v, v0 }}. 97 A.Casagrande et al. Reasoning about connectivity without paths (←) Let us assume that Contains (G, v0 ) = {{v, v0 }}. By definition of Graph (·), if e ∈ G, then |e|≥2 . By definition of Contains (·), Contains (G, v0 ) ⊆ G and, thus, {v, v0 } ∈ G and v , v0 . Moreover, v0 ∈ Nodes (G) by definition of Nodes (·) and v0 < e for all e ∈ G \ {{v, v0 }} by definition of Contains (·). By definition of Filter (·), Filter (G, v) is the set {e\{v} | e ∈ G∧|e \ {v}|≥2 }. Since Contains (G, v0 ) = {{v, v0 }} by hypothesis, if |e \ {v}|≥2 holds, then v0 < e. Thus, v0 belongs neither to Filter (G, v) nor to Filter (G, v)∪{v} because v , v0 and v0 ∈ Nodes (G)\(Filter (G, v)∪{v}). u t Our next step is to prove that any boundary vertex is non-cut. Since v belongs to a single edge, for every subset P of G, either v ∈ Nodes (P) and v < Nodes (G \ P) or v < Nodes (P) and v ∈ Nodes (G \ P). In either case, if the set Nodes (P) ∩ Nodes (G \ P) is nonnull, so is (Nodes (P) ∩ Nodes (G \ P)) \ {v}. If G is connected, either G \ e is empty or v0 belongs to another edge of G. In the former case, G \ e is connected. In the latter, Nodes (G) \ {v} = Nodes (G \ e) and G \ e must be connected. Thus, if G is connected and v is contained exclusively by an edge e whose cardinality is 2, then G \ e is still connected. Lemma 3 (Conn (G) ∧ Contains (G, v) = {{v, v0 }}) → Conn (G \ Contains (G, v)) Proof. Let us assume that there exist G0 , v0 , and v00 such that both the for- mulæ Conn (G0 ) and Contains (G0 , v0 ) = {{v0 , v00 }} hold, while the formula Conn (G0 \ Contains (G0 , v0 )) does not. By definition of Conn (·), there exists a nonnull set P0 such that P0 is a proper subset of G0 \ Contains (G0 , v0 ) and Nodes (P0 ) ∩ Nodes ((G0 \ Contains (G0 , v0 )) \ P0 ) = ∅. Thus, the set Nodes (P0 ) ∩ Nodes ((G0 \ P0 ) \ Contains (G0 , v0 )) is empty. However, the formula Conn (G0 ) holds and, since P0 is also a subset of G0 , Nodes (P0 ) ∩ Nodes (G0 \ P0 ) must be not empty by definition of Conn (·). By writing G0 \ P0 as the union of (G0 \ P0 ) \ Contains (G0 , v0 ) and (G0 \ P0 ) ∩ Contains (G0 , v0 ), we infer that Nodes (P0 ) ∩ (Nodes ((G0 \ P0 ) \ Contains (G0 , v0 ))) ∪ Nodes ((G0 \ P0 ) ∩ Contains (G0 , v0 ))) is nonnull by Lemma 10. Hence, the set Nodes ((G0 \ P0 ) ∩ Contains (G0 , v0 )) ∩ Nodes (P0 ) , ∅, Nodes ((G0 \ P0 ) ∩ Contains (G0 , v0 )) , ∅, and, by the definition of Nodes (·), (G0 \ P0 ) ∩ Contains (G0 , v0 ) , ∅. Since Contains (G0 , v0 ) = {{v0 , v00 }}, {v0 , v00 } ∈ G0 \ P0 and {v0 , v00 } < P0 . However, P0 ⊆ G0 and Contains (G0 , v0 ) = {e ∈ G0 | v0 ∈ e} = {{v0 , v00 }}; therefore Contains (P0 , v0 ) = ∅, and v0 < Nodes (P0 ). More- over, (G0 \ P0 ) ∩ Contains (G0 , v0 ) must be subset of {{v0 , v00 }} and, by Lemma 9,   Nodes ((G0 \ P0 ) ∩ Contains (G0 , v0 )) is subset of Nodes {{v0 , v00 }} which is {v0 , v00 } by the definition of Nodes (·). The set Nodes ((G0 \ P0 ) ∩ Contains (G0 , v0 )) ∩ Nodes (P0 ) is nonnull; therefore it must equal {v00 }, and v00 belongs to Nodes (P0 ). It follows that: Nodes (P0 ∪ Contains (G0 , v0 )) = = Nodes (P0 ) ∪ Nodes (Contains (G0 , v0 )) By Lemma 10   = Nodes (P0 ) ∪ Nodes {{v0 , v00 }} By hypothesis = Nodes (P0 ) ∪ {v0 , v00 } By definition of Nodes (·) = Nodes (P0 ) ∪ {v0 } Because v0 < Nodes (P0 ) 98 A.Casagrande et al. Reasoning about connectivity without paths and, thus, Nodes (G0 \ (P0 ∪ Contains (G0 , v0 ))) ∩ Nodes (P0 ∪ Contains (G0 , v0 )) is equal to both the sets Nodes ((G0 \ Contains (G0 , v0 )) \ P0 ))∩(Nodes (P0 )∪{v0 }) and Nodes ((G0 \ Contains (G0 , v0 )) \ P0 )) ∩ {v0 }. However, G0 \ Contains (G0 , v0 ) is equal to the set {e ∈ G0 | v0 < e} by definition of Contains (·). Hence, v0 does not belong to Nodes (G0 \ Contains (G0 , v0 )) by definition of Nodes (·) and it does not also belong to Nodes (G0 \ Contains (G0 , v0 ) \ P0 ) by Lemma 9. Thus, the set Nodes (G0 \ Contains (G0 , v0 ) \ P0 ) ∩ {v0 } is empty, so is the set Nodes (G0 \ (Contains (G0 , v0 ) ∪ P0 ))∩Nodes (P0 ∪ Contains (G0 , v0 )), and the for- mula Conn (G0 ) does not hold by definition of Conn (·). Since this last statement contradicts our assumptions, the claim must hold. t u Lemma 3 allows us to prove that whenever a vertex v belongs to a single edge e of G, G filtered w.r.t. v is still connected. As a matter of fact, Filter (G, v) contains all the set e0 \ {v} that have at least cardinality 2. Since v belongs only to e, if e \ {v} is still an edge, i.e., it contains at least two nodes, the proof is straightforward because Nodes (G) \ {v} = Nodes (Filter (G, v)) and, thus, because of the above remarks, Filter (G, v) is connected. If, instead, e \ {v} is not an edge, then there exists a node v0 of G such that e = {v, v0 } and Contains (G, v) = {{v, v0 }}. As a matter of fact, since G is connected either G\e is empty or v0 belongs to another edge of G. In the former case, G \ e is connected. In the latter, Nodes (G) \ {v} = Nodes (G \ e) and, because of the above remarks, G \ e = Filter (G, v) must be connected. f a b f a a b c c c d e d e d e  (a) A graph G (b) Filter (G, b) (c) Filter G, f Fig. 4: If the set Contains (G, v) is a singleton and the hypergraph G is connected, the hypergraph Filter (G, v) is connected and v is a non-cut vertex. Lemma 4 (Conn (G) ∧ Contains (G, v) = {e}) → Conn (Filter (G, v)) Proof. By definition, the set Filter (G, v) is equal to {e0 \ {v} | e0 ∈ G ∧ |e0 \ {v}|≥2 }. Since Contains (G, v) = {e}, Filter (G, v) = (G \ {e}) ∪ {e \ {v}| |e \ {v}|≥2 }. There are two cases: |e \ {v}|≥2 does not hold or it does. In the former case, since |e|≥2 by definition of Graph (·), v ∈ e, there exists a v0 such that e = {v, v0 }, and Filter (G, v) = G \ {e}. The claim follows from Lemma 3. If, otherwise, |e \ {v}|≥2 holds, then Filter (G, v) = (G \ {e}) ∪ {e \ {v}}. Let us assume that there exist G0 , v0 , and e0 such that both the formulæ Conn (G0 ) ∧ Contains (G0 , v0 ) = {e0 } and ¬Conn (Filter (G0 , v0 )) hold. By definition of Conn (·), Nodes (G0 \ P) ∩ Nodes (P) , ∅ for all P such that ∅ ( P ( G0 . Since ¬Conn (Filter (G0 , v0 )) 99 A.Casagrande et al. Reasoning about connectivity without paths holds, there exists a P0 such that ∅ ( P0 ( (G0 \ {e0 }) ∪ {e0 \ {v0 }} = Filter (G0 , v0 ) such that Nodes (P0 ) ∩ Nodes (Filter (G0 , v0 ) \ P0 ) is empty. Let be P1 be one of P0 and Filter (G0 , v0 ) \ P0 such that e0 \ {v0 } < P1 . Of course, Nodes (P1 ) ∩ Nodes (Filter (G0 , v0 ) \ P1 ) = ∅ and P1 ⊆ Filter (G0 , v0 ) \ {e0 \ {v0 }} ⊆ G0 . The set Filter (G0 , v0 )\P1 is equal to ((G0 \{e0 })\P1 )∪{e0 \{v0 }} and to ((G0 \P1 )\{e0 })∪{e0 \ {v0 }}. Thus, Nodes (Filter (G0 , v0 ) \ P1 ) and Nodes (G0 \ P1 ) \ {v0 } are the same set by the definition of Nodes (·) and Nodes (G0 \ P1 ) ∩ Nodes (P1 ) ⊆ {v0 }. However, v0 does not belong to Nodes (Filter (G0 , v0 )), by definition of both Nodes (·) and Filter (G0 , v0 ), and P1 ( Filter (G0 , v0 ). Hence, by Lemma 9, v0 < Nodes (P1 ) and Nodes (G0 \ P1 ) ∩ Nodes (P1 ) = ∅. Thus, Conn (G0 ) does not hold by definition of Conn (·). This contradicts our assumptions and proves the claim. t u According to the definition of Cutting (·), Cutting (G, v) holds if and only if G is connected, G contains at least two edges, and either there exists a node v0 , v of G that is not a node of Filter (G, v) or Filter (G, v) is not connected. If v is a boundary vertex and G is connected, Filter (G, v) must be connected too by Lemma 4. It follows that, under the above conditions, Cutting (G, v) holds if and only if G is connected, G contains at least two edges, and there exists a node v0 , v of G that is not a node of Filter (G, v). However, the latter condition holds if and only if Contains (G, v0 ) = {{v, v0 }} by Lemma 2. Thus, Conn (G \ Contains (G, v)) holds by Lemma 3 and Conn (Filter (G, v)). It follows that if v is a boundary vertex of G, then v is a non-cut edge. Lemma 5 Contains (G, v) = {e} → ¬Cutting (G, v) Proof. Let us assume that there exist G0 , v0 , and e0 such that Contains (G0 , v0 ) is {e} and the formula Cutting (G0 , v0 ) holds. By definition of Cutting (·), both the formulæ ¬Conn (Filter (G0 , v0 )) ∨ Nodes (Filter (G0 , v0 )) ∪ {v0 } ( Nodes (G0 ) and Conn (G0 ) ∧ |G0 |≥2 hold. However, Conn (Filter (G0 , v0 )) must hold by Lemma 4. It follows that Nodes (Filter (G0 , v0 )) ∪ {v0 } ( Nodes (G0 ), there exists a v1 ∈ Nodes (G0 ) \ Nodes (Filter (G0 , v0 )) ∪ {v0 }, and, by Lemma 2, Contains (G0 , v1 ) = {{v0 , v1 }}. Since Contains (G0 , v0 ) = {e0 }, from definition of Contains (·) it follows S the same edge and, by Lemma 12, the set Cov (G0 , {e0 }) that e0 and {v0 , v1 } are is equal to the set ( v∈Nodes(e0 ) Contains (G0 , v)), which is {e0 } by definition of Nodes (·). By Lemma 13, Nodes ({e0 }) ∩ Nodes (G0 \ {e0 }) is empty and Conn (G0 ) does not hold by definition of Conn (·). Since this contradicts our assumptions, the claim must hold. t u As a direct consequence of Lemma 2 and Lemma 5, if G has a vertex v0 , v which is not a vertex of Filter (G, v), G has a non-cut vertex too. Proof of Theorem 1. If Nodes (Filter (G, v)) ∪ {v} is a proper subset of Nodes (G), then the set Lost (G, v) is nonnull and it contains a vertex a v0 . By Lemma 2, the set Contains (G, v0 ) is equal to {{v, v0 }} and, by Lemma 5, ¬Cutting (G, v0 ). t u 100 A.Casagrande et al. Reasoning about connectivity without paths 3.2 Not all graphs Filter (G, v) are disconnected This section proves that if G is connected, then it contains a node v such that Filter (G, v) is connected too. Theorem 2 Conn (G) → (G = ∅ ∨ ∃v ∈ Nodes (G) Conn (Filter (G, v))) First of all, let us prove that, for any nonnull set P which is a proper subset of G and such that none of the nodes of P is a node of Filter (G, v) \ P and for any edge e ∈ G, either e does not contain any node of P or e does not contain any node of Filter (G, v) \ P. Namely, if Filter (G, v) is partitioned into two disconnected subgraphs (i.e., P and Filter (G, v) \ P), none of the edges of G “touches” both of these graphs. This is due to the fact that, besides vertices lost by v, which are boundary vertices by Lemma 2, only v belongs to Nodes (G) and not to Nodes (Filter (G, v)). Since Filter (G, v) is disconnected, both e \ Nodes (P) and e \ Nodes (Filter (G, v) \ P) are subsets of Lost (G, v) ∪ {v} for each e ∈ G. Thus, either e ∩ Nodes (P) or e ∩ Nodes (Filter (G, v) \ P) must be empty. Lemma 6 (Graph (G) ∧ P ⊆ Filter (G, v) ∧ Nodes (P) ∩ Nodes (Filter (G, v) \ P) = ∅) → ∀e ∈ G(e ∩ Nodes (P) = ∅ ∨ e ∩ Nodes (Filter (G, v) \ P) = ∅) Proof. Let us assume that there exist G0 , P0 , v0 , and e0 such that both the formulæ Graph (G0 )∧P0 ⊆ Filter (G0 , v0 )∧Nodes (P0 )∩Nodes (Filter (G0 , v0 ) \ P0 ) = ∅ and e0 ∩ Nodes (Filter (G0 , v0 ) \ P0 ) , ∅ ∧ e0 ∩ Nodes (P0 ) , ∅ ∧ e0 ∈ G0 hold. Either (a) v0 < e0 or (b) v0 ∈ e0 holds. In the former case e0 ∈ Filter (G0 , v0 ), by definition of Filter (·) and Graph (·), and we get a contradiction by Lemma 11. Hence, case (b) must hold. By our assumptions, there exist v1 ∈ e0 ∩ Nodes (Filter (G0 , v0 ) \ P0 ) and v2 ∈ e0 ∩ Nodes (P0 ). Since Nodes (Filter (G0 , v0 ) \ P0 ) ∩ Nodes (P0 ) is empty, v1 , v2 and {v0 , v1 , v2 } ⊆ e0 . Moreover, v0 < Nodes (Filter (G0 , v0 )) by defi- nition of Filter (·) and, since P0 ⊆ Filter (G0 , v0 ), v0 < Nodes (P0 ) and v0 < Nodes (Filter (G0 , v0 ) \ P0 ) by Lemma 9. It follows that v0 , v1 and v0 , v2 , e1 = e0 \ {v0 } belongs to Filter (G0 , v0 ) by definition of Filter (·), and |e1 |≥2 . Since both e1 ∩ Nodes (P0 ) and e1 ∩ Nodes (Filter (G0 , v0 ) \ P0 ) are nonnull by construc- tion and P0 ⊆ Filter (G0 , v0 ), Nodes (P0 ) ∩ Nodes (Filter (G0 , v0 ) \ P0 ) is nonnull by Lemma 11. This contradict our assumptions, hence the claim must hold. u t In the light of the above considerations, it is easy to see also that, if G is connected and Lost (G, v) is empty, then v is the only vertex in both of the graphs Cov (G, P) and Cov (G, Filter (G, v) \ P). Lemma 7 (Lost (G, v) = ∅ ∧ Conn (G) ∧ v ∈ Nodes (G) ∧ ∅ ( P ( Filter (G, v) ∧ Nodes (P) ∩ Nodes (Filter (G, v) \ P) = ∅) → Nodes (Cov (G, P)) ∩ Nodes (Cov (G, Filter (G, v) \ P)) = {v} Proof. By the definition of Conn (·), Graph (G) holds. By the definition of Lost (·), if Lost (G, v) = ∅, then Nodes (Filter (G, v)) ⊇ Nodes (G) \ {v}. By Lemma 15, Nodes (Filter (G, v)) ⊆ Nodes (G)\{v}, hence Nodes (G)\{v} = Nodes (Filter (G, v)) and, by Lemma 16, Cov (G, P) ∪ Cov (G, Filter (G, v) \ P) = G. Since Nodes (P) ∩ 101 A.Casagrande et al. Reasoning about connectivity without paths Nodes (Filter (G, v) \ P) = ∅ for all nonnull P that is also a proper subset of Filter (G, v), Cov (G, P) ∩ Cov (G, Filter (G, v) \ P) = ∅ by Lemma 17. As a conse- quence, Cov (G, Filter (G, v) \ P) is equal to G\Cov (G, P) and Nodes (Cov (G, P))∩ Nodes (Cov (G, Filter (G, v) \ P)) , ∅. By the definitions of Nodes (·) and Cov (·), v0 belongs to Nodes (Cov (G, P)) ∩ Nodes (Cov (G, Filter (G, v) \ P)) if and only if there exist e, e0 ∈ G such that e ∩ Nodes (P) and e0 ∩ Nodes (Filter (G, v) \ P) are nonnull and v0 ∈ e∩e0 . Since e, e0 ∈ G, e∩e0 is equal to (e∩e0 )∩Nodes (G) by the def- inition of Nodes (·). Moreover v ∈ Nodes (G) by hypothesis, hence, Nodes (G) is equal to Nodes (Filter (G, v)) ∪ {v} and to Nodes (Filter (G, v) \ P) ∪ Nodes (P) ∪ {v} by Lemma 10. Thus, v0 ∈ e ∩ e0 if and only if either (a) v0 ∈ e ∩ (e0 ∩ Nodes (P)), (b) v0 ∈ e0 ∩ (e ∩ Nodes (Filter (G, v) \ P)), or (c) v0 ∈ (e ∩ e0 ) ∩ {v}. However, due to Lemma 6, e0 ∩ Nodes (P) and e ∩ Nodes (Filter (G, v) \ P) must be empty and both cases (a) and (b) are not possible. It follows that the claim holds. t u By Lemma 2 and Lemma 4, if G is connected and Lost (G, v) is nonnull, then there exists a v0 such that Filter (G, v0 ) is connected. In order to prove Theorem 2 we are left to prove that, whenever G is connected and Lost (G, v) is empty, there exists a v0 such that Filter (G, v0 ) is connected. Q0 ∩ (Filter (G0 , v∗ ) \ Q∗ ) Q∗ v∗ v0 C∗ Filter (G0 , v0 ) \ Q0 Fig. 5: A graphical sketch of the proof of Theorem 2. Let us assume by contradiction that the set Filter (G, v) is not connected for all v ∈ Nodes (G). From the finiteness of G, we can deduce that, for every vertex v of G, there exists a subset of Filter (G, v) ∩ G that is maximal and connected. Let us call it Cv and let C be the set of all these Cv ’s. Since G is finite, so is C and, then, there exists a graph C∗ in C that is maximal. Let v∗ be such that C∗ is subset of Filter (G, v∗ ) ∩ G. Since Filter (G, v∗ ) is disconnected, there exists a nonnull Q∗ that is a proper subset of Filter (G, v∗ ) such that Nodes (Q∗ ) ∩ Nodes (Filter (G, v∗ ) \ Q∗ ) is empty, C∗ ⊆ Q∗ , and Q∗ is minimal. However, none of the edges of G goes from Q∗ to Filter (G, v∗ ) \ Q∗ . Hence, for any node v0 of 102 A.Casagrande et al. Reasoning about connectivity without paths Filter (G, v∗ ) \ Q∗ and for any edge e of Contains (G, v0 ), e does not share any nodes with Q∗ . Hence, Cov (G0 , C∗ ) is connected. Moreover, since Filter (G, v0 ) is not connected either and Contains (G, v∗ ) must share some nodes with Q∗ , there exists a nonnull Q0 that is a proper subset of Filter (G, v0 ) such that Nodes (Q0 ) ∩ Nodes (Filter (G, v0 ) \ Q0 ) is empty and Q∗ ( Q0 . Since Contains (G, v∗ ) must share some nodes with Q∗ and Q∗ is the minimal set that contains C∗ , C∗ must be a proper subset of Cov (G0 , C∗ ). This contradicts our assumptions and, thus, there must exist a v ∈ Nodes (G) such that Filter (G, v) is connected. Proof of Theorem 2. As a preamble, notice that if Conn (G) and Lost (G, v) , ∅ hold together, they imply, respectively, that G is a graph and that there is a v0 ∈ Lost (G, v); hence Contains (G, v0 ) = {{v, v0 }} holds by Lemma 2, and Conn (Filter (G, v0 )) holds by Lemma 4. Arguing by contradiction, suppose then that a G0 exists satisfying Conn (G0 ), ∀v ∈ Nodes (G0 ) ¬Conn (Filter (G0 , v)), ∀v ∈ Nodes (G0 ) Lost (G0 , v) = ∅, and G0 , ∅. Since Nodes (Filter (G0 , v0 )) ⊆ Nodes (G0 ) \ {v} holds for all v, by Lemma 15, in view of the definition of Lost (·) we get Nodes (Filter (G0 , v)) = Nodes (G0 ) \ {v} for all v. Let C be the set {P ⊆ G0 | ∃v ∈ Nodes (G0 ) P ⊆ Filter (G0 , v) ∧ Conn (P)}. From the finiteness of G0 , we get the finiteness of C and hence the existence of an inclusion-maximal C∗ ∈ C; thus, for no v ∈ Nodes (G0 ) there exists any P ⊆ Filter (G0 , v) ∩ G0 such that Conn (P) and C∗ ( P. The set C∗ is empty if and only if Filter (G0 , v) ∩ G0 is empty for all v ∈ Nodes (G0 ), because Conn ({e}) holds for all e ∈ G0 ; ac- cordingly, by Lemma 21, if C∗ = ∅ then Conn (Filter (G0 , v)) holds for all v ∈ Nodes (G0 ). However, this would contradict our assumptions; hence C∗ , ∅ necessarily holds. It follows from C∗ ∈ C that a v∗ ∈ Nodes (G0 ) such that C∗ ⊆ Filter (G0 , v∗ ) must exist. Moreover, since Conn (Filter (G0 , v)) does not hold for any v ∈ Nodes (G0 ), a Q∗ must exist such that ∅ ( Q∗ ( Filter (G0 , v∗ ) and Nodes (Q∗ ) ∩ Nodes (Filter (G0 , v∗ ) \ Q∗ ) = ∅ by the definition of Conn (·). How- ever, C∗ is a subset of Filter (G0 , v∗ ) by construction; thus, by Lemma 18, either C∗ ⊆ Q∗ or C∗ ⊆ Filter (G0 , v∗ ) \ Q∗ holds. Since Filter (G0 , v∗ ) \ (Filter (G0 , v∗ ) \ Q∗ ) equals Q∗ and Nodes (Filter (G0 , v∗ ) \ Q∗ ) ∩ Nodes (Q∗ ) = ∅ if and only if the set Nodes (Filter (G0 , v∗ ) \ (Filter (G0 , v∗ ) \ Q∗ )) ∩ Nodes (Filter (G0 , v∗ ) \ Q∗ ) is empty, we can assume without loss of generality that C∗ ⊆ Q∗ . By the definition of Filter (·), it holds that v∗ < Nodes (Filter (G0 , v∗ )) and, therefore, v∗ < Nodes (Q∗ ). By Lemma 16, G0 = Cov (G0 , Q∗ ) ∪ Cov (G0 , Filter (G0 , v∗ ) \ Q∗ ), while Cov (G0 , Filter (G0 , v∗ ) \ Q∗ )∩Cov (G0 , Q∗ ) = ∅ by Lemma 17. It follows that Cov (G0 , Filter (G0 , v∗ ) \ Q∗ ) equals G0 \ Cov (G0 , Q∗ ) and Nodes (Cov (G0 , Q∗ )) ∩ Nodes (Cov (G0 , Filter (G0 , v∗ ) \ Q∗ )) = {v∗ } by Lemma 7. Therefore we have v∗ ∈ Nodes (Cov (G0 , Q∗ )), whence Conn (Cov (G0 , Q∗ )), by Lemma 19. Since ∅ ( C∗ ⊆ Q∗ ( Filter (G0 , v∗ ), C∗ ( Cov (G0 , Q∗ ) by Lemma 9, Filter (G0 , v∗ ) \ Q∗ is nonnull, and so is Cov (G0 , Filter (G0 , v∗ ) \ Q∗ ) = G0 \ Cov (G0 , Q∗ ) by Lemma 14. From Graph (G0 ) it follows that there are no singletons in G0 . Hence, there exists a v1 ∈ Nodes (G0 \ Cov (G0 , Q∗ )) \ {v∗ } by the definition of Nodes (·). As a conse- quence of Lemma 20, we get Cov (G0 , Q∗ ) ⊆ Filter (G0 , v1 ), which contradicts the assumed maximality of Cv∗ in C. This contradiction proves our claim. t u 103 A.Casagrande et al. Reasoning about connectivity without paths 3.3 Every graph has a non-cut vertex Corollary 1 is a a direct consequence of Theorem 1 and Theorem 2. Proof of Corollary 1. Suppose that there exists a graph G0 such that Conn (G0 ), G0 , ∅, and ∀v ∈ Nodes (G0 ) Cutting (G0 , v) hold. By definition of Cutting (·), the formula Conn (G0 ) ∧ |G0 |≥2 holds and, for all v ∈ Nodes (G0 ), either the set Lost (G0 , v) is nonnull or Conn (Filter (G0 , v)) does not hold. If Lost (G0 , v) is nonnull, then there exists a v0 ∈ Lost (G0 , v) such that ¬Cutting (G0 , v0 ) holds, by Theorem 1, and we get a contradiction. Hence, it must be the case that the formula Conn (G0 ) holds, Lost (G0 , v) is empty, while Conn (Filter (G0 , v)) does not hold for any v ∈ Nodes (G0 ). However, by Theorem 2, there must exists a v0 ∈ Nodes (G0 ) such that Conn (Filter (G0 , v0 )) holds. This is the sought contradiction which proves our claim. t u 4 Conclusions This paper tackles the proof of a property of connected hypergraphs: every hypergraph has non-cut vertices. While this result is not new at all, the novelty of our work lies in the absence of the notion of path. As a matter of fact, we define as connected only those graphs whose edges cannot be parted into two nonnull subgraphs that do not share nodes. This approach has some relevance from a foundational point of view as it proves that paths are not necessary to identify non-cut vertices. Since our proof is based on the ZF theory and it is complete down to the details, we plan to both verify its correctness by means of the proof checker Referee/Ætnanova [6] and to include these results in its scenarios on graphs (see, e.g., [5]). Documentation about these new experiments will be made available at http://aetnanova.units.it/scenarios/NonCutVertices/. References 1. G.-B. Chae, E. M. Palmer, and R. W. Robinson. Counting labeled general cubic graphs. Discrete Mathematics, 307(23):2979–2992, 2007. 2. T. H. Cormen, C. E. Leiserson, R. L. Rivest, C. Stein, et al. Introduction to algorithms, volume 2. MIT press Cambridge, 2001. 3. M. C. Golumbic. Algorithmic graph theory and perfect graphs, volume 57. Elsevier, 2004. 4. M. Milanič and A. I. Tomescu. Set Graphs. I. Hereditarily Finite Sets and Extensional Acyclic Orientations. Discrete Applied Mathematics, 161(4-5):677–690, 2013. 5. E. G. Omodeo and A. I. Tomescu. Set Graphs. III. Proof Pearl: Claw-Free Graphs Mirrored into Transitive Hereditarily Finite Sets. Journal of Automated Reasoning, 52(1):1–29, 2014. 6. J. T. Schwartz, D. Cantone, and E. G. Omodeo. Computational Logic and Set Theory – Applying formalized Logic to Analysis. Springer, 2011. Foreword by Martin Davis. 7. A. Tarski. Sur les ensembles finis. Fundamenta Mathematicae, 6(1):45–95, 1924. 8. F. Wiedijk. The QED Manifesto revisited. Studies in Logic, Grammar and Rhetoric, 10(23):121–133, 2007. 104 A.Casagrande et al. Reasoning about connectivity without paths A Basic Properties Lemma 8 ∃e (e ∈ G ∧ v ∈ e) ↔ v ∈ Nodes (G) S Proof. (←) By the definition of Nodes (·), Nodes (G) = e∈G e. Hence, if v ∈ Nodes (G), there should exists a e0 ∈ G such that v ∈Se0 . (→) By the definition of Nodes (·), Nodes (G) = e∈G e. Hence, if there exists a e0 such that e0 ∈ G ∧ v ∈ e0 , then v ∈ Nodes (G). t u Lemma 9 P ⊆ G → Nodes (P) ⊆ Nodes (G) Proof. By Lemma 8, if v ∈ Nodes (P), then there exists e ∈ P such that v ∈ e. Since P ⊆ G by hypothesis, e ∈ G and, by Lemma 8, v ∈ Nodes (G). t u Lemma 10 Nodes (P ∪ Q) = Nodes (P) ∪ Nodes (Q) Proof. (⊇) Since P ⊆ P ∪ Q, by Lemma 9, Nodes (P) ⊆ Nodes (P ∪ Q). Analo- gously, we get that Nodes (Q) ⊆ Nodes (P ∪ Q). Hence, Nodes (Q) ∪ Nodes (P) ⊆ Nodes (P ∪ Q) ∪ Nodes (P ∪ Q) = Nodes (P ∪ Q). (⊆) By Lemma 8, if v ∈ Nodes (P ∪ Q) then there exists a e ∈ P ∪ Q such that v ∈ e. Hence, e belongs to either P or Q. If e ∈ P, then v ∈ Nodes (P) by Lemma 8. Symmetrically, if e ∈ Q, then v ∈ Nodes (Q) by Lemma 8. Thus, if v ∈ Nodes (P ∪ Q), then v ∈ Nodes (P) ∪ Nodes (Q). t u Lemma 11 P ⊆ G → (Nodes (P) ∩ Nodes (G \ P) = ∅ ↔ ∀e ∈ G(e ∩ Nodes (P) = ∅ ∨ e ∩ Nodes (G \ P) = ∅)) S Proof. By the definition of Nodes (·), Nodes (G) = e∈G e. Thus, Nodes (P) ∩ Nodes (G \ P) = ∅ if and only if both e ∩ Nodes (P) and e0 ∩ Nodes (G \ P) are empty for all e ∈ G \ P and for all e0 ∈ P. However, if P ⊆ G, then (G \ P) ∪ P is equal to G. Thus, if P ⊆ G, then Nodes (P) ∩ Nodes (G \ P) = ∅ if and only if ∀e ∈ G (e ∩ Nodes (P) = ∅ ∨ e ∩ Nodes (G \ P) = ∅). t u S Lemma 12 Cov (G, P) = v∈Nodes(P) Contains (G, v) S Proof. We prove that e ∈ Cov (G, P) if and only if e ∈ v∈Nodes(P) Contains (G, v). By definition of Cov (·), e ∈ Cov (G, P) if and only if and only if e ∈ G and e ∩ Nodes (P) , ∅. Hence, e ∈ Cov (G, P) if and only if there exists a v ∈ Nodes (P) and a e ∈ G such that v ∈ e. By definition of Contains (·), e ∈ Contains (G, v) if and only if v ∈ e and e ∈ G. Thus, e ∈ Cov (G, P) if and only if there exists a v ∈ Nodes (P) such that e ∈ Contains (G, v). The thesis follows directly. t u Lemma 13 Cov (G, P) ⊆ P ↔ Nodes (G \ P) ∩ Nodes (P) = ∅ Proof. By the definition of Cov (·), Cov (G, P) is equal to {e ∈ G | e ∩ Nodes (P) , ∅}. S (G, P) ⊆ P if and only if e ∩ Nodes (P) = ∅ for all e ∈ G \ P and if and Hence, Cov only if ( e∈G\P e) ∩ Nodes (P) = ∅. By definition of Nodes (·), this is equivalent to Nodes (G \ P) ∩ Nodes (P) = ∅ and, thus, the thesis holds. t u 105 A.Casagrande et al. Reasoning about connectivity without paths Lemma 14 Nodes (P) ⊆ Nodes (G) ∧ Nodes (P) , ∅ → Cov (G, P) , ∅ Proof. Let us assume that there exist G0 and P0 such that both Nodes (P0 ) ⊆ Nodes (G0 )∧Nodes (P0 ) , ∅ and Cov (G0 , P0 ) = ∅ hold. Since Cov (G0 , P0 ) is equal to {e ∈ G0 | e ∩ Nodes (P0 ) , ∅} by the definition of Cov (·), Cov (G0 , P0 ) = ∅ if and only if Nodes (G0 )∩Nodes (P0 ) is empty. However, from Nodes (P0 ) ⊆ Nodes (G0 ), we deduce that Nodes (G0 ) ∩ Nodes (P0 ) and Nodes (P0 ) are the same set and, from Nodes (P0 ) , ∅, we get that Nodes (G0 ) ∩ Nodes (P0 ) is not empty. This leads to a contradiction and proves our goal. t u Lemma 15 Nodes (Filter (G, v)) ⊆ Nodes (G) \ {v} S Proof. By the definition of Nodes (·), if Nodes (Filter (G, v)) = e0 ∈Filter(G,v) e0 . However, by the definition of Filter (·), e0 ∈ Filter (G, v) if any only if there exists a e ∈ G such that e0 = e \ {v} and |e \ {v}|≥2 . Thus, Nodes (Filter (G, S S v)) = e∈G | |e\{v}| S ≥2  e \ V. Since {e ∈ G | |e \ {v}|≥2 } ⊆ G, Nodes (Filter (G, V)) ⊆ e∈G e \ {v} = e∈G e \ {v}. Hence, by the definition of Nodes (·), Nodes (Filter (G, v)) ⊆ Nodes (G) \ {v}. t u B Auxiliary Lemmas Lemma 16 (Graph (G) ∧ Nodes (Filter (G, v)) = Nodes (G) \ {v} ∧ P ⊆ Filter (G, v)) → Cov (G, P) ∪ Cov (G, Filter (G, v) \ P) = G Proof. Let us assume that there exist G0 , P0 , and v0 such that both the for- mulæ Graph (G0 )∧Nodes (Filter (G0 , v0 )) = Nodes (G0 )\{v0 }∧P0 ⊆ Filter (G0 , v0 ) Cov (G0 , P0 ) ∪ Cov (G0 , Filter (G0 , v0 ) \ P0 ) , G0 hold. By the definition of Cov (·), Cov (G0 , P) is the set {e ∈ G0 | e ∩ Nodes (P) , ∅}. Thus, Cov (G0 , P) ⊆ G0 and Cov (G0 , P0 ) ∪ Cov (G0 , Filter (G0 , v0 ) \ P0 ) ⊆ G0 . However, Cov (G0 , P0 ) ∪ Cov (G0 , Filter (G0 , v0 ) \ P0 ) , G0 by assumption, hence, there exists a e0 ∈ G0 that belongs to neither Cov (G0 , P0 ) nor Cov (G0 , Filter (G0 , v0 ) \ P0 ). By the defi- nition of Cov (·), e0 ∩ Nodes (P0 ) = ∅ and e0 ∩ Nodes (Filter (G0 , v0 ) \ P0 ) = ∅. Thus e0 ∩(Nodes (P0 )∪Nodes (Filter (G0 , v0 ) \ P0 )) = ∅ and e0 ∩Nodes (Filter (G0 , v0 )) is empty by Lemma 10. Since Nodes (Filter (G0 , v0 )) = Nodes (G0 ) \ {v0 } by assump- tion, e0 ∩ (Nodes (G0 ) \ {v0 }) is empty and e0 ∩ Nodes (G0 ) ⊆ {v0 }. By definition of Nodes (·), e0 ⊆ Nodes (G0 ). Thus, e0 ∩ Nodes (G0 ) = e0 and e0 ⊆ {v0 }. However, this contradicts |e0 |≥2 which must hold because of the definition of Graph (·). The claim of this lemma follows readily. t u Lemma 17 (Graph (G) ∧ Nodes (Filter (G, v) \ P) ∩ Nodes (P) = ∅ ∧ P ⊆ Filter (G, v)) → Cov (G, P) ∩ Cov (G, Filter (G, v) \ P) = ∅ Proof. By Lemma 6, either e ∩ Nodes (P) or e ∩ Nodes (Filter (G, v) \ P) are empty for all e ∈ G. By the definition of Cov (·), it follows that either e < Cov (G, P) or e < Cov (G, Filter (G, v) \ P) for all e ∈ G. Thus, Cov (G, P) ∩ Cov (G, Filter (G, v) \ P) is empty and the claim holds. t u 106 A.Casagrande et al. Reasoning about connectivity without paths Lemma 18 (Nodes (Q) ∩ Nodes (G \ Q) = ∅ ∧ P ⊆ G ∧ Conn (P)) → (P ⊆ G \ Q ∨ P ⊆ Q) Proof. Let us assume that there exist G0 , P0 , and Q0 such that both the formulæ Nodes (Q0 )∩Nodes (G0 \ Q0 ) = ∅∧P0 ⊆ G0 ∧Conn (P0 ) and P0 * G0 \Q0 ∧P0 * Q0 hold. Hence, there exist an e0 ∈ P0 that does not belong to G0 \ Q0 and an e1 ∈ P0 that does not belong to Q0 . It follows that both the sets P0 \ Q0 and P0 \ (G0 \ Q0 ) are nonnull. Since P0 ⊆ G0 , e0 belongs to Q0 . Thus, P0 \ Q0 is a nonnull set that is also proper subset of P0 . By definition of Conn (·), Conn (P0 ) holds if and only if the set Nodes (P0 \ S) ∩ Nodes (S) is nonnull for all not empty S that are also proper subsets of P0 . In particular, the set Nodes (P0 \ (P0 \ Q0 ))∩Nodes (P0 \ Q0 ) is nonnull. Thus, ∅ (Nodes (P0 \ (P0 \ Q0 )) ∩ Nodes (P0 \ Q0 ) =Nodes (P0 ∩ Q0 ) ∩ Nodes (P0 \ Q0 ) ⊆Nodes (Q0 ) ∩ Nodes (P0 \ Q0 ) Since P0 ∩ Q0 ⊆ P0 , by Lemma 9 ⊆Nodes (Q0 ) ∩ Nodes (G0 \ Q0 ) Since P0 ⊆ G0 , by Lemma 9 This contradicts our assumptions and proves the claim. t u Lemma 19 (Conn (P ∪ Q) ∧ Nodes (P) ∩ Nodes (Q) = {v}) → Conn (P) Proof. Let us assume that there exist P0 , Q0 and v0 such that both the formulæ Conn (P0 ∪ Q0 ) ∧ Nodes (P0 ) ∩ Nodes (Q0 ) = {v0 } and ¬Conn (P0 ) hold. By def- inition of Conn (·), there exists a P1 such that ∅ ( P1 ( P0 and Nodes (P1 ) ∩ Nodes (P0 \ P1 ) is empty. Furthermore, {v0 } =Nodes (P0 ) ∩ Nodes (Q0 ) By assumption =Nodes ((P0 \ P1 ) ∪ P1 ) ∩ Nodes (Q0 ) Since P1 ⊆ P0 = (Nodes (P0 \ P1 ) ∪ Nodes (P1 )) ∩ Nodes (Q0 ) By Lemma 10 = (Nodes (P0 \ P1 ) ∩ Nodes (Q0 )) ∪ (Nodes (P1 ) ∩ Nodes (Q0 )) Thus, either v0 ∈ Nodes (P0 \ P1 ) ∩ Nodes (Q0 ) or v0 ∈ Nodes (P1 ) ∩ Nodes (Q0 ). Since Nodes (P0 \ P1 ) ∩ Nodes (P1 ) = ∅, either v0 < Nodes (P0 \ P1 ) or v0 < Nodes (P1 ). Moreover, (Nodes (P0 \ P1 ) ∩ Nodes (Q0 )) ∪ (Nodes (P1 ) ∩ Nodes (Q0 )) is equal to {v0 }, hence, one of the two sets Nodes (P0 \ P1 ) ∩ Nodes (Q0 ) and Nodes (P1 ) ∩ Nodes (Q0 ) is empty. Let be P2 be such that P2 ∈ {P1 , P0 \ P1 } and Nodes (P2 ) ∩ Nodes (Q0 ) is empty. Since ∅ ( P1 ( P0 , P2 is nonnull, it is a proper subset of P0 and (P0 \ P2 ) ∪ P2 = P0 . Moreover, P1 = P0 \ (P0 \ P1 ) and, hence, Nodes (P2 ) ∩ Nodes (P0 \ P2 ) = Nodes (P1 ) ∩ Nodes (P0 \ P1 ) = ∅ is empty. By the definition of Nodes (·), Nodes (P0 ) ∩ Nodes (Q0 ) = {v0 } if and only if e ∩ e0 ⊆ {v0 } for all e ∈ P0 and for all e0 ∈ Q0 . Hence, |e ∩ e0 |≥2 does not hold and, by the defi- nition of Graph (·), this means that P0 ∩ Q0 = ∅. Since P2 ( P0 , P2 ∩ Q0 ⊆ P0 ∩ Q0 107 A.Casagrande et al. Reasoning about connectivity without paths and P2 ∩ Q0 is empty. It follows that ∅ =(Nodes (P2 ) ∩ Nodes (P0 \ P2 ))∪ (Nodes (P2 ) ∩ Nodes (Q0 )) =Nodes (P2 ) ∩ (Nodes (P0 \ P2 ) ∪ Nodes (Q0 )) =Nodes (P2 ) ∩ Nodes ((P0 \ P2 ) ∪ Q0 ) By Lemma 10 =Nodes (P2 ) ∩ Nodes ((P0 ∪ Q0 ) \ P2 ) Since Q0 ∩ P2 = ∅ By the definition of Conn (·), Conn (P0 ∪ Q0 ) does not hold. This contradicts our assumptions and prove the claim. t u Lemma 20 (Graph (P ∪ Q) ∧ Nodes (P) ∩ Nodes (Q) = {v}) → ∀v0 ∈ Nodes (Q) \ {v} (P ⊆ Filter (P ∪ Q, v0 )) Proof. By definition of Filter (·), Filter (P ∪ Q, v0 ) ={e \ {v0 } | e ∈ (P ∪ Q) ∧ |e \ {v0 }|≥2 } ={e \ {v0 } | e ∈ P ∧ |e \ {v0 }|≥2 } ∪ {e \ {v0 } | e ∈ Q ∧ |e \ {v0 }|≥2 } Since v0 ∈ Nodes (Q) \ {v} and Nodes (P) ∩ Nodes (Q) = {v}, then v0 < Nodes (P). By definition of Nodes (·), it follows that v0 < e and e = e \ {v0 } for any e ∈ P. Thus, Filter (P ∪ Q, v0 ) ={e| e ∈ P ∧ |e|≥2 } ∪ {e \ {v0 } | e ∈ Q ∧ |e \ {v0 }|≥2 } =P ∪ {e \ {v0 } | e ∈ Q ∧ |e \ {v0 }|≥2 } The claim readily follows from the last equation. t u Lemma 21 (Graph (G) ∧ ∀v ∈ Nodes (G) Filter (G, v) ∩ G = ∅) → ∀v ∈ Nodes (G) Conn (Filter (G, v)) Proof. The graph Filter (G, v) ∩ G is empty for all v ∈ Nodes (G) if and only if Contains (G, v) = G for all v ∈ Nodes (G), i.e., every edge of G contains all nodes of G. It follows that G is a singleton and that each Filter (G, v) is either empty or a singleton; hence, by the definition of Conn (·), Conn (Filter (G, v)) holds for all v ∈ Nodes (G). The claim follows readily. t u 108