It is easy to know that the maximal satisfiable set of propositions can only contain A's and C's statement. Then we can imply that B would be the murder. Example 4. Consider the pigeonhole principle: f: n+,n, 3i,j, f(i)=f(), where0<i<j< Solution: let Pij means f(i)=j. Then we can describe everywhere defined property as a1=^0≤i≤nVo≤j<nPij and we can describe single value as ≤nA0≤j≠k<n=(D万∧pk) Now we can describe pigeonhole principle as (a1Aa2)A(Vo≤i<j≤nVo≤k<n(PkAp3,k) Remark: This form of pigeonhole is much harder to recognize than its original version. However, it is described by a much more rigid language compared with our natural language, which could result in ambiguities In fact, mathematical logic can be applied into program verification, model checking, and such other applications. European Space Agency only uses software which has gotten through program eriocaulon 8 Application of Compactness Theorem Compactness theorem is a very important result in mathematical logic. It establishes a connection Example 5. Given an infinite planar graph. If its every finite subgraph is k-colorable, then the graph itself is also k-colorable A graph is G=< V, E > where V is the set of vertices and E c v2 is the set of all edges.If (a, b)EE, it is denoted as a Eb sometimes. G is k-colorable if V can be decomposed into k-color classes V= C1U U. U Ck, where Cif0 and CinCi=0 if i*j. It is obvious(a, b)E if a,b∈C A finite subgraph is k-colorable. It means there is a k-colorable graph Go = Vo, Eo>, where Vo cv is a finite set and Eo C E is the set determined by vo Proof. Let Pa i represent vertex a is colored with i. We can formulate a graph which is k-colorable with the following propositions 1. Pa1 Vpa. 2V..VPa.k, for every a E V. It means every vertex could be colored with at least one of k colors 2.-(PaiA∧pa),1≤i<j≤ k for alleY. It means CinC=0.It is easy to know that the maximal satisfiable set of propositions can only contain A’s and C’s statement. Then we can imply that B would be the murder. Example 4. Consider the pigeonhole principle: f : n + → n, ∃i, j, f(i) = f(j), where 0 ≤ i < j ≤ n. Solution: let pij means f(i) = j. Then we can describe everywhere defined property as α1 = ∧0≤i≤n ∨0≤j<n pij and we can describe single value as α1 = ∧0≤i≤n ∧0≤j̸=k<n ¬(pij ∧ pik) Now we can describe pigeonhole principle as φ = (α1 ∧ α2) ∧ (∨0≤i<j≤n ∨0≤k<n (pik ∧ pj,k)) Remark: This form of pigeonhole is much harder to recognize than its original version. However, it is described by a much more rigid language compared with our natural language, which could result in ambiguities. In fact, mathematical logic can be applied into program verification, model checking, and such other applications. European Space Agency only uses software which has gotten through program verification. 8 Application of Compactness Theorem Compactness theorem is a very important result in mathematical logic. It establishes a connection between infinity and finitude. Example 5. Given an infinite planar graph. If its every finite subgraph is k-colorable, then the graph itself is also k-colorable. A graph is G =< V, E >, where V is the set of vertices and E ⊆ V 2 is the set of all edges. If (a, b) ∈ E, it is denoted as aEb sometimes. G is k-colorable if V can be decomposed into k-color classes V = C1 ∪ C2 ∪ · · · ∪ Ck, where Ci ̸= ∅ and Ci ∩ Cj = ∅ if i ̸= j. It is obvious (a, b) ̸∈ E if a, b ∈ Ci . A finite subgraph is k-colorable. It means there is a k-colorable graph G0 =< V0, E0 > , where V0 ⊂ V is a finite set and E0 ⊂ E is the set determined by V0. Proof. Let pa,i represent vertex a is colored with i. We can formulate a graph which is k-colorable with the following propositions. 1. pa,1 ∨ pa,2 ∨ · · · ∨ pa,k, for every a ∈ V . It means every vertex could be colored with at least one of k colors. 2. ¬(pa,i ∧ pa,j ), 1 ≤ i < j ≤ k for all a ∈ V . It means Ci ∩ Cj = ∅. 5