propositional-logic.html (7073B)
1 <html> 2 <head> 3 <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/highlight.min.js"></script> 4 <script type="text/javascript" async src="https://cdn.jsdelivr.net/gh/mathjax/MathJax@2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script> 5 <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/9.15.6/styles/default.min.css"> 6 <link rel="Stylesheet" type="text/css" href="style.css" /> 7 <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> 8 <script> 9 document.addEventListener('DOMContentLoaded', function() { 10 document.querySelectorAll('pre.code').forEach(function(item) { 11 hljs.highlightBlock(item) 12 }) 13 }); 14 </script> 15 <title>propositional-logic</title> 16 </head> 17 <body> 18 <style type="text/css"> 19 nav a { 20 text-align: left; 21 } 22 nav #name { 23 text-align: right; 24 float: right; 25 font-style: italic; 26 } 27 </style> 28 <nav> 29 <a href="index.html">Index</a> 30 <span id="name">Alex Balgavy</span> 31 </nav> 32 <hr> 33 <div class="content"> 34 35 <div id="Propositional logic"><h2 id="Propositional logic" class="header"><a href="#Propositional logic">Propositional logic</a></h2></div> 36 <div id="Propositional logic-Notation review"><h3 id="Notation review" class="header"><a href="#Propositional logic-Notation review">Notation review</a></h3></div> 37 <ul> 38 <li> 39 <code>A, B, C</code> -- propositions 40 41 <li> 42 <code>A ∧ B</code> -- conjunction ("and") 43 44 <li> 45 <code>A ∨ B</code> -- disjunction ("or") 46 47 <li> 48 <code>A → B</code> -- implication ("if A then B") 49 50 <li> 51 <code>A ↔ B</code> -- bi-implication ("A iff B") 52 53 <li> 54 <code>¬ A</code> -- negation ("not A") 55 56 <li> 57 <code>⊥</code> -- false, falsum, nonsense, bullshit, the middle finger 58 59 </ul> 60 61 <div id="Propositional logic-Rules of inference"><h3 id="Rules of inference" class="header"><a href="#Propositional logic-Rules of inference">Rules of inference</a></h3></div> 62 <p> 63 "C is a logical consequence of A and B": 64 </p> 65 66 <p> 67 <img src="img/logical-consequence.png" alt="Logical consequence" /> 68 </p> 69 70 71 <table> 72 <tr> 73 <th> 74 Implication 75 </th> 76 <th> 77 Conjunction 78 </th> 79 <th> 80 Negation 81 </th> 82 <th> 83 Disjunction 84 </th> 85 <th> 86 Bi-implication ("if and only if") 87 </th> 88 </tr> 89 <tr> 90 <td> 91 <img src="img/implication-elimination.png" alt="Implication elimination" /> 92 </td> 93 <td> 94 <img src="img/conjunction-introduction.png" alt="Conjunction introduction" /> 95 </td> 96 <td> 97 <img src="img/negation-hypothetical-reasoning.png" alt="Negation hypothetical reasoning" /> 98 </td> 99 <td> 100 <img src="img/disjunction-introduction.png" alt="Disjunction introduction" /> 101 </td> 102 <td> 103 <img src="img/bi-implication-introduction.png" alt="Bi-implication introduction" /> 104 </td> 105 </tr> 106 <tr> 107 <td> 108 <img src="img/hypothesis.png" alt="Hypothesis" /> 109 </td> 110 <td> 111 <img src="img/and-elimination.png" alt="And elimination" /> 112 </td> 113 <td> 114 <img src="img/negation-elimination.png" alt="Negation elimination" /> 115 </td> 116 <td> 117 <img src="img/disjunction-elimination.png" alt="Disjunction elimination" /> 118 </td> 119 <td> 120 <img src="img/bi-implication-elimination.png" alt="Bi-implication elimination" /> 121 </td> 122 </tr> 123 </table> 124 125 <p> 126 Truth and falsity: from false, you can conclude anything, and from nothing, you can conclude true. 127 </p> 128 129 <p> 130 <img src="img/falsum-elimination.png" alt="Falsum elimination" />, <img src="img/truth-introduction.png" alt="Truth introduction" /> 131 </p> 132 133 <p> 134 You can also derive this conjunction rule: 135 </p> 136 137 <p> 138 <img src="img/conjunction-negation-rule.png" alt="Conjunction negation rule" /> 139 </p> 140 141 <div id="Propositional logic-Forward and backward reasoning"><h3 id="Forward and backward reasoning" class="header"><a href="#Propositional logic-Forward and backward reasoning">Forward and backward reasoning</a></h3></div> 142 <p> 143 Backward reasoning: looking at the goal and seeing what rules need to be applied ("bottom-up") 144 </p> 145 146 <p> 147 Forward reasoning: starting at some hypotheses/assumptions 148 </p> 149 150 <p> 151 The general heuristic is to always work backwards, as much as possible. Only once you get stuck should you work from your assumptions or hypotheses. 152 </p> 153 154 <p> 155 If all else fails, try proof by contradiction. 156 </p> 157 158 <div id="Propositional logic-Proof by contradiction"><h3 id="Proof by contradiction" class="header"><a href="#Propositional logic-Proof by contradiction">Proof by contradiction</a></h3></div> 159 <p> 160 Suppose a negation of a formula is true, prove that it's impossible, thereby proving the original formula. 161 </p> 162 163 <p> 164 <img src="img/proof-by-contradiction.png" alt="Proof by contradiction" /> 165 </p> 166 167 <p> 168 RAA stands for <em>"reductio ad absurdum"</em> 169 </p> 170 171 <div id="Propositional logic-Vocab definitions"><h3 id="Vocab definitions" class="header"><a href="#Propositional logic-Vocab definitions">Vocab definitions</a></h3></div> 172 <ul> 173 <li> 174 derivable: a formula φ is "derivable" if we can prove φ with no global hypotheses (bottom line is φ, everything is closed). Then we write ⊢ φ. 175 176 <li> 177 φ is derivable from hypotheses ψ₁..ψn if we can compute φ assuming ψ₁..ψn 178 179 <li> 180 formulas φ and ψ are logically equivalent if ⊢ φ ↔ ψ 181 182 </ul> 183 184 <div id="Propositional logic-Classical reasoning"><h3 id="Classical reasoning" class="header"><a href="#Propositional logic-Classical reasoning">Classical reasoning</a></h3></div> 185 <p> 186 Principles: 187 </p> 188 <ul> 189 <li> 190 Proof by contradiction: assume the contradiction, and show false, thereby proving the original. 191 192 <li> 193 Double negation elimination: ¬ ¬ A ↔ A. 194 195 <li> 196 Contrapositive: if A → B, then ¬ B → ¬ A 197 198 </ul> 199 200 <p> 201 A general heuristic: 202 </p> 203 <ol> 204 <li> 205 Work backward from the conclusion, using introduction rules. 206 207 <li> 208 When you run out of stuff to do, work forward with elimination rules. 209 210 <li> 211 If you get stuck, 212 213 </ol> 214 <blockquote> 215 <img src="img/go-go-proof-by-contradiction.jpg" alt="Proof by contradiction meme" style="width:20%" /> 216 </blockquote> 217 <blockquote> 218 (meme credit goes to Geo) 219 </blockquote> 220 221 <div id="Propositional logic-Syntax vs Semantics"><h3 id="Syntax vs Semantics" class="header"><a href="#Propositional logic-Syntax vs Semantics">Syntax vs Semantics</a></h3></div> 222 <p> 223 Syntax: 224 </p> 225 <ul> 226 <li> 227 derivation, proofs 228 229 <li> 230 Γ ⊢ A ("A is derivable from hypotheses in Γ") 231 232 </ul> 233 234 <p> 235 Semantics: 236 </p> 237 <ul> 238 <li> 239 truth and falsity 240 241 <li> 242 truth assignment says which propositional letters are true 243 244 <li> 245 valuation says which formulas are true 246 247 </ul> 248 249 <div id="Propositional logic-Soundness and completeness"><h3 id="Soundness and completeness" class="header"><a href="#Propositional logic-Soundness and completeness">Soundness and completeness</a></h3></div> 250 <p> 251 provable: if there is a formal proof of a formula (syntactic) 252 </p> 253 254 <p> 255 tautology/valid: if true under any truth assignment (semantic) 256 </p> 257 258 <p> 259 soundness: if a formula is provable, it is valid (if ⊢ A, then ⊨ A) 260 </p> 261 262 <p> 263 completeness: if a formula is valid, it is provable (if ⊨ A, then ⊢ A) 264 </p> 265 266 <p> 267 Proving soundness is easier than proving completeness. 268 </p> 269 270 <p> 271 A is a logical consequence of Γ if, given any truth assignment that makes every formula in Γ true, A is true. 272 </p> 273 274 </div> 275 </body> 276 </html>