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.
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 [
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).
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 [
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.
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 formulae 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: |S|≥n D (
> if n = 0 ∃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 setS 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.
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 [
Any subset of a graph is a graph.
Proof. The claim follows directly from the definition of Graph (·).
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,
Nodes (G) d=ef [ e
Cov (G, P) d=ef {e ∈ G | e ∩ Nodes (P) , ∅}
Contains (G, v) d=ef {e ∈ G | v ∈ e} f a d c b e e∈G g h
(a) A graph P ⊆ G (b) Cov (G, P) (c) Contains (G, a) If the graph G is connected and G \ {e} is not connected, then e is said to be a cutting edge.
f a d c b e a
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.
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.
Filter (G, v) d=ef {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 belong 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.
the set of nodes of G that are not nodes of Filter (G, v) and differ from v.
Lost (G, v) d=ef Nodes (G) \ (Nodes (Filter (G, v)) ∪ {v})
elements are said to be lost by v.
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
Our goal is to provide a proof that every connected hypergraph contains a non-cut vertex. This is encoded by the following corollary. f a d c b e d c b e f a d b e
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}}. (←) 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 ofContains (·). By definition ofFilter (·), 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}). tu
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 formulae 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 ofConn (·). 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). Moreover, (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}} = Nodes (P0) ∪ {v0, v00} = Nodes (P0) ∪ {v0} By hypothesis By definition of Nodes (·)
contradicts our assumptions, the claim must hold. 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 formula Conn (G0) does not hold by definition ofConn (·). Since this last statement tu
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
f a d c b e a d c e a d c b e 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 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)) 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
of Conn (·). This contradicts our assumptions and proves the claim. Nodes (G0 \ P1) ∩ Nodes (P1) = ∅. Thus, Conn (G0) does not hold by definition tu
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.
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 that if v is a boundary vertex of G, then v is a non-cut edge. 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 Lemma 5 Contains (G, v) = {e} → ¬Cutting (G, v) the claim must hold. is equal to the set (S
{e} and the formula Cutting (G0, v0) holds. By definition of Cutting (·), both the formulae ¬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 that e0 and {v0, v1} are the same edge and, by Lemma 12, the set Cov (G0, {e0}) 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, v∈Nodes(e0) Contains (G0, v)), which is {e0} by definition of tu
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). tu 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
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) = ∅)
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 definition 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 construction 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. tu
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 ofConn (·), Graph (G) holds. By the definition ofLost (·), 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) ∩
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 consequence, 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 definition 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. tu
Q∗ C∗ Q0 ∩ (Filter (G0, v∗) \ Q∗) v0 Filter (G0, v0) \ Q0
all v ∈ Nodes (G). From the finiteness ofG, 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
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 there must exist a v ∈ Nodes (G) such that Filter (G, v) is connected. be a proper subset of Cov (G0, C∗). This contradicts our assumptions and, thus, 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
C 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 ofC and hence the existence of an inclusion-maximal ∗ ∈ 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; accordingly, by Lemma 21, if C
∗ = ∅ then Conn (Filter (G0, v)) holds for all v ∈
necessarily holds. It follows from C ∗ ∈
C that a v∗ ∈
∗ , ∅ C 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 (·). However, C∗ is a subset of Filter (G0, v∗) by construction; thus, by Lemma 18, either ∗ ⊆ Q∗ or C
∗ ⊆ Filter (G0, v∗) \ Q∗ holds. Since Filter (G0, v∗) \ (Filter (G0, v∗) \ is empty, we can assume without loss of generality that C 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∗) ∗ ⊆ 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.
assumed maximality of Cv∗ in C. This contradiction proves our claim. a v1 ∈ Nodes (G0 \ Cov (G0, Q∗)) \ {v∗} by the definition of Nodes (·). As a consequence of Lemma 20, we get Cov (G0, Q∗) ⊆ Filter (G0, v1), which contradicts the tu 3.3
Every graph has a non-cut vertex Corollary 1 is a a direct consequence of Theorem 1 and Theorem 2. contradiction which proves our claim.
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 tu 4
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., [
Discrete Mathematics, 307(23):2979–2992, 2007.
volume 2. MIT press Cambridge, 2001. 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.
Lemma 8 ∃e (e ∈ G ∧ v ∈ e) ↔ v ∈ Nodes(G) P ⊆ G by hypothesis, e ∈ G and, by Lemma 8, v ∈ Nodes(G).
Proof. By Lemma 8, if v ∈ Nodes(P), then there exists e ∈ P such that v ∈ e. Since Lemma 10 Nodes(P ∪ Q) = Nodes(P) ∪ Nodes(Q) a e0 such that e0 ∈ G ∧ v ∈ e0, then v ∈ Nodes(G).
Nodes(G), there should exists a e0 ∈ G such that v ∈ e0.
Proof. (←) By the definition of Nodes(·), Nodes(G) = Se∈G e. Hence, if v ∈ (→) By the definition ofNodes(·), Nodes(G) = Se∈G e. Hence, if there exists Nodes(G \ P) ∩ Nodes(P) = ∅ and, thus, the thesis holds.
Proof. BythedefinitionofCov(·),Cov(G,P)isequalto{e ∈ G|e∩Nodes(P) , ∅}. Hence, Cov(G,P) ⊆ P if and only if e ∩ Nodes(P) = ∅ for all e ∈ G \ P and if and only if (S e∈G\P e) ∩ Nodes(P) = ∅. By definition ofNodes(·), this is equivalent to Nodes(P ∪ Q) ∪ Nodes(P ∪ Q) = Nodes(P ∪ Q).
Proof. (⊇) Since P ⊆ P ∪ Q, by Lemma 9, Nodes(P) ⊆ Nodes(P ∪ Q). Analogously, we get that Nodes(Q) ⊆ Nodes(P ∪ Q). Hence, Nodes(Q) ∪ Nodes(P) ⊆ (⊆) 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).
Lemma 11 P ⊆ G → (Nodes(P) ∩ Nodes(G \ P) = ∅ ↔
∀e ∈ G(e ∩ Nodes(P) = ∅ ∨ e ∩ Nodes(G \ P) = ∅)) Proof. By the definition of Nodes(·), Nodes(G) = S e∈G e. Thus, Nodes(P) ∩ Nodes(G \ P) = ∅ if and only if both e ∩ Nodes(P) and e0 ∩ Nodes(G \ P) are ∀e ∈ G (e ∩ Nodes(P) = ∅ ∨ e ∩ Nodes(G \ P) = ∅).
Lemma 12 Cov(G,P) = Sv∈Nodes(P) Contains(G,v) 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 Proof. We prove that e ∈ Cov(G,P) if and only if e ∈ S 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 ofContains(·), 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. Lemma 13 Cov(G,P) ⊆ P ↔ Nodes(G \ P) ∩ Nodes(P) = ∅ tu tu tu tu tu tu
Lemma 14 Nodes (P) ⊆ Nodes (G) ∧ Nodes (P) , ∅ → Cov (G, P) , ∅ to a contradiction and proves our goal.
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 ofCov (·), 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
S {v} =
S Nodes (G) \ {v}.
Proof. By the definition of Nodes (·), if Nodes (Filter (G, v)) = S 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, v)) = e∈G | |e\{v}|≥2 e \ V. Since {e ∈ G | |e \ {v}|≥2} ⊆ G, Nodes (Filter (G, V)) ⊆ S e∈G e \ e∈G e \ {v}. Hence, by the definition of Nodes (·), Nodes (Filter (G, v)) ⊆ B
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
mulae
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 ofCov (·), Cov (G0, P) is the set {e ∈ G0 | e ∩ Nodes (P) , ∅}. Thus, Cov (G0, P) ⊆ 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 G0 The claim of this lemma follows readily. that belongs to neither Cov (G0, P0) nor Cov (G0, Filter (G0, v0) \ P0). By the definition 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 assumption, 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 (·). Lemma 17 (Graph (G) ∧ Nodes (Filter (G, v) \ P) ∩ Nodes (P) = ∅ ∧
P ⊆ Filter (G, v)) → Cov (G, P) ∩ Cov (G, Filter (G, v) \ P) = ∅ is empty and the claim holds.
Proof. By Lemma 6, either e ∩ Nodes (P) or e ∩ Nodes (Filter (G, v) \ P) are empty for all e ∈ G. By the definition ofCov (·), 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) tu tu tu tu
Lemma 18 (Nodes (Q) ∩ Nodes (G \ Q) = ∅ ∧ P ⊆ G ∧ Conn (P)) → (P ⊆ G \ Q ∨ P ⊆ Q) is nonnull. Thus,
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) ∅ (Nodes (P0 \ (P0 \ Q0)) ∩ Nodes (P0 \ Q0) =Nodes (P0 ∩ Q0) ∩ Nodes (P0 \ Q0) ⊆Nodes (Q0) ∩ Nodes (P0 \ Q0) ⊆Nodes (Q0) ∩ Nodes (G0 \ Q0) Since P0 ∩ Q0 ⊆ P0, by Lemma 9 Since P0 ⊆ G0, by Lemma 9 This contradicts our assumptions and proves the claim. tu Lemma 19 (Conn (P ∪ Q) ∧ Nodes (P) ∩ Nodes (Q) = {v}) → Conn (P) Nodes (P0 \ P1) is empty. Furthermore,
Conn (P0 ∪ Q0) ∧ Nodes (P0) ∩ Nodes (Q0) = {v0} and ¬Conn (P0) hold. By definition of Conn (·), there exists a P1 such that ∅ ( P1 ( P0 and Nodes (P1) ∩ {v0} =Nodes (P0) ∩ Nodes (Q0) =Nodes ((P0 \ P1) ∪ P1) ∩ Nodes (Q0) = (Nodes (P0 \ P1) ∪ Nodes (P1)) ∩ Nodes (Q0) = (Nodes (P0 \ P1) ∩ Nodes (Q0)) ∪ (Nodes (P1) ∩ Nodes (Q0))
By assumption Since P1 ⊆ P0 By Lemma 10 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 definition of Graph (·), this means that P0 ∩ Q0 = ∅. Since P2 ( P0, P2 ∩ Q0 ⊆ P0 ∩ Q0 and P2 ∩ Q0 is empty. It follows that ∅ =(Nodes (P2) ∩ Nodes (P0 \ P2))∪ assumptions and prove the claim.
By the definition ofConn (·), Conn (P0 ∪ Q0) does not hold. This contradicts our 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 ofNodes (·), 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.
Lemma 21 (Graph (G) ∧ ∀v ∈ Nodes (G) Filter (G, v) ∩ G = ∅) → ∀v ∈ Nodes (G) Conn (Filter (G, v)) v ∈ Nodes (G). The claim follows readily.
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 ofConn (·), Conn (Filter (G, v)) holds for all tu