index.md (4275B)
1 +++ 2 title = 'Proof systems and derivation' 3 +++ 4 # Proof systems and derivation 5 ## Proof systems 6 Hilbert systems: 7 - proof is sequence of numbered formulas 8 - every formula is: an axiom, or result of applying a derivation rule 9 10 Sufficient to have 2 axioms and a rule: 11 - K: φ → ψ → φ 12 - S: (φ → ψ → θ) → (φ → ψ) → (φ → θ) 13 - modus ponens: if φ and (φ → ψ), then ψ 14 15 Rules will be given, don't need to be memorized. 16 17 Admissible rule: 18 19  20 21 Proof system K is sound and complete with respect to all frames, ⊢K φ iff ⊨ φ. 22 23 Soundness and completeness results (**note:** the frame classes _need_ to be memorized) 24 - K sound and complete for all frames 25 - T sound and complete for all _reflexive_ frames 26 - T: K with □ p → p 27 - S4 sound and complete for all _reflexive-transitive_ frames 28 - S4: T with □ p → □ □ p 29 - S5 sound and complete for all frames with R an equivalence relation 30 - S5: S4 with ¬ □ p → □ ¬ □ p 31 32 ## Example of derivation 33 Give derivation in K of ◇ φ ∧ □ (φ → ψ) → ◇ ψ. 34 Same as example in book <abbr title='Modal Logic for Open Minds (Benthem)'>MLOM</abbr> page 52. 35 36 First, work backwards from the goal towards an axiom or tautology: 37 38 <pre> 39 ◇ φ ∧ □ (φ → ψ) → ◇ ψ ≡ □ (φ → ψ) → (◇ φ → ◇ ψ) [you can rewrite a conjunction as an implication] 40 ≡ □ (φ → ψ) → (¬ □ ¬ φ → ¬ □ ¬ ψ) [rewrite diamond to ¬ □ ¬] 41 ≡ □ (φ → ψ) → (□ ¬ ψ → □ ¬ φ) [rewrite contrapositive (¬ a → ¬ b) to (b → a)] 42 ≡ □ (φ → ψ) → □ (¬ ψ → ¬ φ) [box distribution over implication] 43 ≡ □ (φ → ψ) → □ (φ → ψ) [again contrapositive] 44 ≡ (φ → ψ) → (φ → ψ) [because if derivable (a → b), then derivable (□ a → □ b)] 45 </pre> 46 47 We arrive at a tautology. 48 49 Then you write it out in a Hilbert-style proof, starting with the tautology/axiom. 50 PROP means rewriting in propositional logic. 51 52 1. (φ → ψ) → (¬ ψ → ¬ φ). PROP. 53 2. □ (φ → ψ) → □ (¬ ψ → ¬ φ). DISTR, 1. 54 3. □ (p → q) → □ p → □ q. modal distribution (i.e., this is an axiom in K that we use) 55 4. □ (¬ ψ → ¬ φ) → □ ¬ ψ → □ ¬ φ. substitution, 3 (i.e., substitute stuff in the axiom). 56 5. □ (φ → ψ) → □ ¬ ψ → □ ¬ φ. PROP, 2, 4. 57 6. □ (φ → ψ) → ¬ ◇ ψ → ¬ ◇ φ. definition of ◇, □. 58 7. □ (φ → ψ) → ◇ φ → ◇ ψ. PROP, 6. 59 8. ◇ φ ∧ □ (φ → ψ) → ◇ ψ. PROP, 7. 60 61 <details> 62 <summary>Why you can rewrite a conjunction as an implication</summary> 63 64 You can safely rewrite a conjunction to an implication: (a ∧ b → c) ≡ a → (b → c). 65 Remember that implication is right-associative! 66 67 If you don't trust me, I didn't trust myself either so I made a truth table: 68 69 <table> 70 <thead> 71 <tr> 72 <th>a</th> 73 <th>b</th> 74 <th>c</th> 75 <th>b → c</th> 76 <th>a ∧ b</th> 77 <th>a → c</th> 78 <th>a ∧ b → c</th> 79 <th>b → (a → c)</th> 80 <th>a → (b → c)</th> 81 </tr> 82 </thead> 83 <tbody> 84 <tr> 85 <td>0</td> 86 <td>0</td> 87 <td>0</td> 88 <td>1</td> 89 <td>0</td> 90 <td>1</td> 91 <td>1</td> 92 <td>1</td> 93 <td>1</td> 94 </tr> 95 96 <tr> 97 <td>0</td> 98 <td>0</td> 99 <td>1</td> 100 <td>1</td> 101 <td>0</td> 102 <td>1</td> 103 <td>1</td> 104 <td>1</td> 105 <td>1</td> 106 </tr> 107 108 <tr> 109 <td>0</td> 110 <td>1</td> 111 <td>0</td> 112 <td>0</td> 113 <td>0</td> 114 <td>1</td> 115 <td>1</td> 116 <td>1</td> 117 <td>1</td> 118 </tr> 119 120 <tr> 121 <td>0</td> 122 <td>1</td> 123 <td>1</td> 124 <td>1</td> 125 <td>0</td> 126 <td>1</td> 127 <td>1</td> 128 <td>1</td> 129 <td>1</td> 130 </tr> 131 132 <tr> 133 <td>1</td> 134 <td>0</td> 135 <td>0</td> 136 <td>1</td> 137 <td>0</td> 138 <td>0</td> 139 <td>1</td> 140 <td>1</td> 141 <td>1</td> 142 </tr> 143 144 <tr> 145 <td>1</td> 146 <td>0</td> 147 <td>1</td> 148 <td>1</td> 149 <td>0</td> 150 <td>1</td> 151 <td>1</td> 152 <td>1</td> 153 <td>1</td> 154 </tr> 155 156 <tr> 157 <td>1</td> 158 <td>1</td> 159 <td>0</td> 160 <td>0</td> 161 <td>1</td> 162 <td>0</td> 163 <td>0</td> 164 <td>0</td> 165 <td>0</td> 166 </tr> 167 168 <tr> 169 <td>1</td> 170 <td>1</td> 171 <td>1</td> 172 <td>1</td> 173 <td>1</td> 174 <td>1</td> 175 <td>1</td> 176 <td>1</td> 177 <td>1</td> 178 </tr> 179 </tbody> 180 </table> 181 182 You see that the right three columns all have the same values, so semantically the formulas are the same. 183 184 </details> 185