5 Compactness Theorem Theorem 8(finite proof). If T= UTn is a contradictory tableau from X, then for some m, Tm is a finite contradictory tableau from 2. In particular, if a Cst from 2 is a proof, it is finite It means a tableau proof is a finite sequence of trees. Otherwise we can imply contradiction that the tableau is not a tabeau proof With finite proof theorem, we have a type of compactness theorem by using completeness and soundness theore Theorem 9. a is a consequence of 2 if and only if a is a consequence of some finite subset of 2 Sketch. We apply completeness theorem first and get 2Ha. For any tableau proof must be finite, we can collect all proposition introduced from 2 and form a finite set 2o. The tableau also shows Eo Ha. We then apply soundness theorem and obtain Zo a. It is proved now However, compactness theorem can be directly proved. We have the following version Theorem 10( Compactness). Let 2= aili e w be an infinite set of a propositions. E is satisfiable if and only if every finite subset r of 2 is satisfiable Generally, if V1 and v2 satisfy >l and 22 respectively, it does not mean the union of two truth valuation would satisfy all propositions in two sets Sketch. Consider the tableau with root F(=a∧a) We already know that (a A a) is always false, which means that any truth valuation V always agrees with the root entry. If it is a finite tableau, every path of tableau is contradictory. It means that all propositions in 2 along a contradictory path is unsatisfiable. It is contradictory to every finite subset is satisfiable. So there is a infinite path in the tableau This compactness theorem transform a problem with infinite propositions to a infinite sequence of finite propositions 6 Circuit and Proposition Let's take 0, 1 as F, T respectively. We can use circuit gate to represent A, V and as and, or, not respectively. So given any proposition, we can design a circuit to compute the truth value with the specific inpu Example 1. Consider the circuit for the following propositions The circuit will be drawn in the future5 Compactness Theorem Theorem 8 (finite proof). If τ = ∪τn is a contradictory tableau from Σ, then for some m, τm is a finite contradictory tableau from Σ. In particular, if a CST from Σ is a proof, it is finite. It means a tableau proof is a finite sequence of trees.Otherwise we can imply contradiction that the tableau is not a tabeau proof. With finite proof theorem, we have a type of compactness theorem by using completeness and soundness theorem. Theorem 9. α is a consequence of Σ if and only if α is a consequence of some finite subset of Σ. Sketch. We apply completeness theorem first and get Σ ` α. For any tableau proof must be finite, we can collect all proposition introduced from Σ and form a finite set Σ0. The tableau also shows Σ0 ` α. We then apply soundness theorem and obtain Σ0 |= α. It is proved now. However, compactness theorem can be directly proved. We have the following version. Theorem 10 (Compactness). Let Σ = {αi |i ∈ ω} be an infinite set of a propositions. Σ is satisfiable if and only if every finite subset Γ of Σ is satisfiable. Generally, if V1 and V2 satisfy Σ1 and Σ2 respectively, it does not mean the union of two truth valuation would satisfy all propositions in two sets. Sketch. Consider the tableau with root F(¬α ∧ α). We already know that (¬α ∧ α) is always false, which means that any truth valuation V always agrees with the root entry. If it is a finite tableau, every path of tableau is contradictory. It means that all propositions in Σ along a contradictory path is unsatisfiable. It is contradictory to every finite subset is satisfiable. So there is a infinite path in the tableau. This compactness theorem transform a problem with infinite propositions to a infinite sequence of finite propositions. 6 Circuit and Proposition Let’s take 0, 1 as F, T respectively. We can use circuit gate to represent ∧, ∨ and ¬ as and,or,not respectively. So given any proposition, we can design a circuit to compute the truth value with the specific input. Example 1. Consider the circuit1 for the following propositions: 1The circuit will be drawn in the future. 3