Definition 6(Modus Ponens). From a and a-,B, we can infer B. This rule is written as follows a→ aββ Now we can define Hilbert proof system Definition 7. Let 2 be a set of propositions 1. A proof from 2 is a finite sequence a1, a2, .. an such that for each i n either (a)a; is a member of∑ (b)ai is an ariom (c)ai can be inferred from some of previous a, by an application of a rule of inference 2. a is provable from∑,∑hra, if there is a proof a1,a2,…,, an from∑ where an=a A proof of a is simply a proof from the empty set 0; a is provable if it is provable from 0 Example 6. Prove the following statements 1.(a→B)→(a→a) 2.{a}hH(-→a)→B) The first can also be proved by tableau proof system. The way to prove the second would not be introduced until the next class. However, you can experience the difference between these two of systems Exercises 1. If a is tableau refutable, then a is unsatisfiable 2. If a is unsatisfiable, then there is a tableau refutation of a 3. Prove that all axioms are valid in Hilbert proof system 4.Is(a→B)→(a→)→(a→(→) valid? Otherwise, construct a truth valuation which make it falseDefinition 6 (Modus Ponens). From α and α → β, we can infer β. This rule is written as follows: α α → β β Now we can define Hilbert proof system. Definition 7. Let Σ be a set of propositions. 1. A proof from Σ is a finite sequence α1, α2, . . . , αn such that for each i ≤ n either: (a) αi is a member of Σ. (b) αi is an axiom; or (c) αi can be inferred from some of previous αj by an application of a rule of inference. 2. α is provable from Σ, Σ ⊢H α, if there is a proof α1, α2, . . . , αn from Σ where αn = α. 3. A proof of α is simply a proof from the empty set 0; α is provable if it is provable from 0. Example 6. Prove the following statements: 1. (α → β) → (α → α). 2. {¬α} ⊢H ((¬β → α) → β). The first can also be proved by tableau proof system. The way to prove the second would not be introduced until the next class. However, you can experience the difference between these two proof systems. Exercises 1. If α is tableau refutable, then α is unsatisfiable. 2. If α is unsatisfiable, then there is a tableau refutation of α. 3. Prove that all axioms are valid in Hilbert proof system. 4. Is ((α → β) → (α → γ)) → (α → (β → γ)) valid? Otherwise, construct a truth valuation which make it false. 4