lectures.alex.balgavy.eu

Lecture notes from university.
git clone git://git.alex.balgavy.eu/lectures.alex.balgavy.eu.git
Log | Files | Refs | Submodules

propositional-logic.wiki (4636B)

      1 %template math
      2 == Propositional logic ==
      3 === Notation review ===
      4 * `A, B, C` -- propositions
      5 * `A ∧ B` -- conjunction ("and")
      6 * `A ∨ B` -- disjunction ("or")
      7 * `A → B` -- implication ("if A then B")
      8 * `A ↔ B` -- bi-implication ("A iff B")
      9 * `¬ A` -- negation ("not A")
     10 * `⊥` -- false, falsum, nonsense, bullshit, the middle finger
     11 
     12 === Rules of inference ===
     13 "C is a logical consequence of A and B":
     14 
     15 {{local:../img/logical-consequence.png|Logical consequence}}
     16 
     17 
     18 | Implication                                                            | Conjunction                                                              | Negation                                                                               | Disjunction                                                              | Bi-implication ("if and only if")                                              |
     19 |------------------------------------------------------------------------|--------------------------------------------------------------------------|----------------------------------------------------------------------------------------|--------------------------------------------------------------------------|--------------------------------------------------------------------------------|
     20 | {{local:../img/implication-elimination.png|Implication elimination}} | {{local:../img/conjunction-introduction.png|Conjunction introduction}} | {{local:../img/negation-hypothetical-reasoning.png|Negation hypothetical reasoning}} | {{local:../img/disjunction-introduction.png|Disjunction introduction}} | {{local:../img/bi-implication-introduction.png|Bi-implication introduction}} |
     21 | {{local:../img/hypothesis.png|Hypothesis}}                           | {{local:../img/and-elimination.png|And elimination}}                   | {{local:../img/negation-elimination.png|Negation elimination}}                       | {{local:../img/disjunction-elimination.png|Disjunction elimination}}   | {{local:../img/bi-implication-elimination.png|Bi-implication elimination}}   |
     22 
     23 Truth and falsity: from false, you can conclude anything, and from nothing, you can conclude true.
     24 
     25 {{local:../img/falsum-elimination.png|Falsum elimination}}, {{local:../img/truth-introduction.png|Truth introduction}}
     26 
     27 You can also derive this conjunction rule:
     28 
     29 {{local:../img/conjunction-negation-rule.png|Conjunction negation rule}}
     30 
     31 === Forward and backward reasoning ===
     32 Backward reasoning: looking at the goal and seeing what rules need to be applied ("bottom-up")
     33 
     34 Forward reasoning: starting at some hypotheses/assumptions
     35 
     36 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.
     37 
     38 If all else fails, try proof by contradiction.
     39 
     40 === Proof by contradiction ===
     41 Suppose a negation of a formula is true, prove that it's impossible, thereby proving the original formula.
     42 
     43 {{local:../img/proof-by-contradiction.png|Proof by contradiction}}
     44 
     45 RAA stands for _"reductio ad absurdum"_
     46 
     47 === Vocab definitions ===
     48 * derivable: a formula φ is "derivable" if we can prove φ with no global hypotheses (bottom line is φ, everything is closed). Then we write ⊢ φ.
     49 * φ is derivable from hypotheses ψ₁..ψn if we can compute φ assuming ψ₁..ψn
     50 * formulas φ and ψ are logically equivalent if ⊢ φ ↔ ψ
     51 
     52 === Classical reasoning ===
     53 Principles:
     54     * Proof by contradiction: assume the contradiction, and show false, thereby proving the original.
     55     * Double negation elimination: ¬ ¬ A ↔ A.
     56     * Contrapositive: if A → B, then ¬ B → ¬ A
     57 
     58 A general heuristic:
     59     1. Work backward from the conclusion, using introduction rules.
     60     2. When you run out of stuff to do, work forward with elimination rules.
     61     3. If you get stuck,
     62 
     63     {{local:../img/go-go-proof-by-contradiction.jpg|Proof by contradiction meme|style="width:20%"}}
     64 
     65     (meme credit goes to Geo)
     66 
     67 === Syntax vs Semantics ===
     68 Syntax:
     69 - derivation, proofs
     70 - Γ ⊢ A ("A is derivable from hypotheses in Γ")
     71 
     72 Semantics:
     73 - truth and falsity
     74 - truth assignment says which propositional letters are true
     75 - valuation says which formulas are true
     76 
     77 === Soundness and completeness ===
     78 provable: if there is a formal proof of a formula (syntactic)
     79 
     80 tautology/valid: if true under any truth assignment (semantic)
     81 
     82 soundness: if a formula is provable, it is valid (if ⊢ A, then ⊨ A)
     83 
     84 completeness: if a formula is valid, it is provable (if ⊨ A, then ⊢ A)
     85 
     86 Proving soundness is easier than proving completeness.
     87 
     88 A is a logical consequence of Γ if, given any truth assignment that makes every formula in Γ true, A is true.
     89