-
-
Save viecode09/f130067f0fb072ef0d397af0329ba920 to your computer and use it in GitHub Desktop.
Discrete Math Using a Computer: Chapter 06 Propositional Logic notes and exercise solutions
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #+TITLE: DiscreteMathComputer 06 - Propositional Logic | |
| #+DATE: | |
| #+LATEX_HEADER: \usepackage{fullpage} | |
| #+LATEX_HEADER: \usepackage{tgschola} | |
| #+OPTIONS: H:3 toc:nil | |
| * Chapter Outline | |
| - Difficulties with informal logic | |
| - Propositional logic (one type of formal logic) | |
| - Three mathematical systems for reasoning about propositions: | |
| + Truth Tables: easy to understand but unwieldy for large expressions; "semantic technique" | |
| + Natural Deduction: "syntactic technique", uses inference rules | |
| + Boolean Algebra: axiomatic approach | |
| * Need for Formalism | |
| - Natural language has ambiguities and subtleties | |
| + e.g. "and" can sometimes suggest an implication as in "The sun is shining and I am happy" | |
| - *Proposition*: variable whose value must be either _True_ or _False_ | |
| - *Logical Operators*: _and_, _or_, _not_, _implies_ . Operate on propositions | |
| - Statements that can't be represented by propositional logic (due to lack of context): | |
| + e.g. "That cloud looks like a motor bike" | |
| + context required: which cloud? who thinks that it looks like a motor bike? | |
| * Basic Logical Operators | |
| ** Logical And ($\wedge$) | |
| - aka *Conjunction* | |
| *** Truth Table | |
| | $A$ | $B$ | $A \wedge B$ | | |
| |-------+-------+--------------| | |
| | False | False | False | | |
| | False | True | True | | |
| | True | False | False | | |
| | True | True | True | | |
| ** Inclusive Or ($\vee$) | |
| - aka *Disjunction* | |
| *** Truth Table | |
| | $A$ | $B$ | $A \vee B$ | | |
| |-------+-------+------------| | |
| | False | False | False | | |
| | False | True | True | | |
| | True | False | True | | |
| | True | True | True | | |
| ** Exclusive Or ($\oplus$) | |
| - Either one or the other, but not both | |
| *** Truth Table | |
| | $A$ | $B$ | $A \oplus B$ | | |
| |-------+-------+--------------| | |
| | False | False | False | | |
| | False | True | True | | |
| | True | False | True | | |
| | True | True | False | | |
| ** Logical Not ($\neg$) | |
| *** Truth Table | |
| | $A$ | $\neg A$ | | |
| |-------+----------| | |
| | True | False | | |
| | False | True | | |
| ** Logical Implication ($\Rightarrow$) | |
| - Use to represent conditional phrases | |
| - e.g. "If it is sunny today, then there will be a picnic." | |
| - *Implication does not say anything about cause-and-effect* | |
| *** Truth Table | |
| | $A$ | $B$ | $A \Rightarrow B$ | | |
| | False | False | True | | |
| | False | True | True | | |
| | True | False | False | | |
| | True | True | True | | |
| *** Understanding the truth table | |
| - Why is an implication true even if $A$ is False? | |
| - One way to think about is that an implication is a statement that if something happens then something else must also happen | |
| - So, if the first event happens, but the second doesn't, the implication must have been faulty | |
| - But the first event doesn't happen at all, then we're indifferent about the implication | |
| - Rephrasing the above point, "If A then B" is like saying that "A" is sufficient for B to occur | |
| + So, if we see an A but not a B, clearly A isn't sufficient for B | |
| + But if we see a B on its own, maybe something other than A caused it. | |
| + e.g. Matchsticks are sufficient for fire. But just because you use a lighter to make a fire doesn't mean matchsticks can't cause fire. However, if you have a matchstick and still can't produce fire, it clearly isn't sufficient. | |
| - Book is a little handwavy and just says "this is the way it is" | |
| ** Logical Equivalence ($\Leftrightarrow$) | |
| - Use to make a claim that two propositions always have the same value, or are equivalent | |
| - aka "If and only if", "necessary and sufficient" | |
| *** Truth Table | |
| | $A$ | $B$ | $A \Leftrightarrow B$ | | |
| |-------+-------+-----------------------| | |
| | False | False | True | | |
| | False | True | False | | |
| | True | False | False | | |
| | True | True | True | | |
| *** "If and only If" | |
| - $A \Leftrightarrow B$ can be written as $(A \Rightarrow B) \wedge (B \Rightarrow A)$ | |
| * The Language of Propositional Logic | |
| ** Well-Formedness | |
| - Have a grammar for propositional logic | |
| - If a formula doesn't follow this grammar, it isn't well formed | |
| - e.g. Well-Formed Formula: $A \Rightarrow (B \wedge (\neg A))$ | |
| - e.g. not Well-Formed Formula: $\wedge A B \neg C$ | |
| - *Well-formedness is only about the syntax and says nothing about the semantics of the formula* | |
| + e.g. "if it compiles", then it is well-formed. Just because something compiles doesn't mean it'll pass all the tests | |
| ** Syntax of Well-Formed Formulas | |
| - *Constants* $False$ and $True$ are WFF. | |
| - Any propositional *variable* is WFF. | |
| - *Negation*: If $a$ is WFF, then $\neg a$ is WFF | |
| - *Conjunction*: If $a$ and $b$ are WFF, then $a \wedge b$ is WFF | |
| - *Disjunction*: If $a$ and $b$ are WFF, then $a \vee b$ is WFF | |
| - *Implication*: If $a$ and $b$ are WFF, then $a \Rightarrow b$ is WFF | |
| - *Equivalence*: If $a$ and $b$ are WFF, then $a \Leftrightarrow b$ is WFF | |
| *** Example: $P \Rightarrow (Q \wedge R)$ is a WFF | |
| - $P, Q, R$ are WFF because they're propositional variables | |
| - So, $Q \wedge R$ is a WFF (conjunction rule) | |
| - So, $P \Rightarrow (Q \wedge R)$ is a WFF (implication rule) | |
| ** Order of Precedence | |
| - Negation ($\neg$) is the most tightly binding operator | |
| - Conjunction ($\wedge$) | |
| - Disjunction ($\vee$) | |
| - Implication ($\Rightarrow$) | |
| - Equivalence ($\Leftrightarrow$) is the least tightly binding operator | |
| ** Object Language and Meta Language | |
| - WFFs of propositional language will be called *object language* | |
| + They refer to sentences in propositional logic | |
| - Language of equations, substitutions, and justifications will be called the *meta language* | |
| + The surround the object language | |
| + They're used to talk _about_ propositions | |
| ** Computing with Boolean Expressions | |
| - $\neg x$ is written \texttt{not x} | |
| - $a \wedge b$ is written \texttt{a \&\& b} | |
| - $a \vee b$ is written \texttt{a || b} | |
| - $a \Rightarrow b$ is written \texttt{a ==> b} | |
| - $a \Leftrightarrow b$ is written \texttt{a <=> b} | |
| ** (Exercise 1) : Lying Bus Driver | |
| *** Scenario | |
| - Want to go to the airport, are at the bus stop | |
| - Either this bus or the next is going to the airport, but not both | |
| - Can only ask one "yes-or-no" question | |
| - Some drivers will answer "yes" when the correct answer is "no" | |
| + You don't know if this bus driver is one of those people | |
| - Ask one "yes or no" question that can help you decide whether to take this bus or the next | |
| *** Solution 1 | |
| - I first gave names to the situations: | |
| + $A$: this bus goes to the airport | |
| + So, $\neg A$ means the next one goes to the airport | |
| + $L$: this driver is a liar | |
| + So, $\neg L$ means this driver answers truthfully | |
| - I want to formulate my question so that if the answer is "True", then $A$. | |
| - I then made a table of the possible situations: | |
| | L | A | Desired Answer | | |
| |-------+-------+----------------| | |
| | True | True | True | | |
| | True | False | False | | |
| | False | True | True | | |
| | False | False | False | | |
| - So, clearly just asking $A$ gives me the desired answer regardless of what $L$ is | |
| ** (Exercise 2) : Evaluating propositional formulas | |
| - $False \wedge True$ | |
| + $False$ | |
| - $True \vee (\neg True)$ | |
| + $True$ | |
| - $\neg (False \vee True)$ | |
| + $\neg True$ | |
| + $False$ | |
| - $(\neg (False \wedge True)) \vee False$ | |
| + $(\neg False) \vee False$ | |
| + $True \vee False$ | |
| + $True$ | |
| - $(\neg True) \Rightarrow True$ | |
| + $False \Rightarrow True$ | |
| + $True$ | |
| - $True \vee False \Rightarrow True$ | |
| + $True \Rightarrow True$ | |
| + $True$ | |
| - $True \Rightarrow (True \wedge False)$ | |
| - $True \Rightarrow False$ | |
| - $False$ | |
| - $False \Rightarrow False$ | |
| + $True$ | |
| - $\neg False \Leftrightarrow True$ | |
| + $True \Leftrightarrow True$ | |
| + $True$ | |
| - $True \Leftrightarrow (False \Rightarrow False)$ | |
| + $True \Leftrightarrow True$ | |
| + $True$ | |
| - $False \Leftrightarrow (True \wedge (False \Rightarrow True))$ | |
| + $False \Leftrightarrow (True \wedge True)$ | |
| + $False \Leftrightarrow True$ | |
| + $False$ | |
| - $\neg (True \vee False) \Leftrightarrow False \wedge True$ | |
| + $\neg True \Leftrightarrow False$ | |
| + $False \Leftrightarrow False$ | |
| + $True$ | |
| *** Verification using the Book's Stdm Library | |
| #+begin_src haskell | |
| *Stdm> False /\ True | |
| False | |
| *Stdm> True \/ (not True) | |
| True | |
| *Stdm> not (False \/ True) | |
| False | |
| *Stdm> (not (False /\ True)) \/ False | |
| True | |
| *Stdm> (not True) ==> True | |
| True | |
| *Stdm> True \/ False ==> True | |
| True | |
| *Stdm> True ==> (True /\ False) | |
| False | |
| *Stdm> False ==> False | |
| True | |
| *Stdm> (not False) <=> True | |
| True | |
| *Stdm> True <=> (False ==> False) | |
| True | |
| *Stdm> False <=> (True /\ (False ==> True)) | |
| False | |
| *Stdm> (not (True \/ False)) <=> False /\ True | |
| True | |
| *Stdm> | |
| #+end_src | |
| * Truth Tables: Semantic Reasoning | |
| - Table | |
| - Column headers are all the variables (and expressions) | |
| - Add a row for each possible setting of values for variables | |
| - 3 variables means $2^3 = 8$ rows | |
| - because 2 possible settings for each of the 3 variables | |
| ** Example: Calculating using a Truth Table | |
| - Suppose we want to know when the proposition $((A \Rightarrow B) \wedge \neg B) \Rightarrow \neg A$ is true | |
| - Make a Truth Table | |
| | | A | B | $A \Rightarrow B$ | $\neg B$ | $(A \Rightarrow B) \wedge \neg B$ | $\neg A$ | $((A \Rightarrow B) \wedge \neg B) \Rightarrow \neg A$ | | |
| |---+---+---+-------------------+----------+-----------------------------------+----------+--------------------------------------------------------| | |
| | / | < | > | < | | | > | <> | | |
| | # | F | F | T | T | T | T | T | | |
| | # | F | T | T | F | F | T | T | | |
| | # | T | F | F | T | F | F | T | | |
| | # | T | T | T | F | F | F | T | | |
| ** Definition: Tautology | |
| - Proposition that is always True, regardless of its variables | |
| ** Definition: Contradiction | |
| - Proposition that is always False, regardless of its variables | |
| ** Definition: Entailment ($\vDash$) | |
| - $P_1, P_2, \cdots, P_n \vDash Q$ means that if all the propositions $P_1, P_2, \cdots, P_n$ are True, then $Q$ is also True | |
| *** Discussion | |
| - $\vDash$ makes a statement about actual meanings of propositions | |
| - *Model of a logic system*: Set of truth values along with the method for calculating meaning of any well-formed formula | |
| - Different values of $n$ | |
| - $n = 1$ gives $P \vDash Q$, which has the same semantics as $\Rightarrow$ | |
| - $n = 0$ gives $\vDash Q$, which means that $Q$ is always True, or is a tautology | |
| ** Limitations of Truth Tables | |
| - Size is exponential in number of variables | |
| - Other techniques (natural deduction, Boolean algebra) give much better insight into why a proposition is true | |
| ** Exercise 3: Determine which formulas are tautologies using truth tables | |
| *** $(True \wedge P) \vee Q$ | |
| | | P | Q | $True \wedge P$ | $(True \wedge P) \vee Q$ | | |
| |---+---+---+-----------------+--------------------------| | |
| | / | < | > | <> | <> | | |
| | # | T | T | T | T | | |
| | # | T | F | T | T | | |
| | # | F | T | F | T | | |
| | # | F | F | F | F | | |
| - not a tautology | |
| - without truth tables: $(True \wedge P) \vee Q$ becomes $P \vee Q$, which is False when both $P$ and $Q$ are False | |
| *** $(P \vee Q) \Rightarrow (P \wedge Q)$ | |
| | | P | Q | $P \vee Q$ | $P \wedge Q$ | $(P \vee Q) \Rightarrow (P \wedge Q)$ | | |
| |---+---+---+------------+--------------+---------------------------------------| | |
| | / | < | > | < | > | <> | | |
| | # | T | T | T | T | T | | |
| | # | T | F | T | F | F | | |
| | # | F | T | T | F | F | | |
| | # | F | F | F | F | T | | |
| - not a tautology | |
| *** $(P \wedge Q) \Rightarrow (P \vee Q)$ | |
| | | P | Q | $P \wedge Q$ | $P \vee Q$ | $(P \vee Q) \Rightarrow (P \wedge Q)$ | | |
| |---+---+---+--------------+------------+---------------------------------------| | |
| | / | < | > | < | > | <> | | |
| | # | T | T | T | T | T | | |
| | # | T | F | F | T | T | | |
| | # | F | T | F | T | T | | |
| | # | F | F | F | F | T | | |
| - Tautology | |
| *** $(P \vee Q) \Rightarrow (Q \vee P)$ | |
| | | P | Q | $P \vee Q$ | $Q \vee P$ | $(P \vee Q) \Rightarrow (P \wedge Q)$ | | |
| |---+---+---+------------+------------+---------------------------------------| | |
| | / | < | > | < | > | <> | | |
| | # | T | T | T | T | T | | |
| | # | T | F | T | T | T | | |
| | # | F | T | T | T | T | | |
| | # | F | F | F | F | T | | |
| - Tautology | |
| - Without Truth Table: by commutativity of $\vee$ | |
| *** $((P \vee Q) \wedge (P \vee R)) \Leftrightarrow (P \wedge (Q \vee R))$ | |
| | | P | Q | R | $P \vee Q$ | $P \vee R$ | LHS | $Q \vee R$ | RHS | LHS $\Leftrightarrow$ RHS | | |
| |---+---+---+---+------------+------------+-----+------------+-----+---------------------------| | |
| | / | < | | > | <> | <> | <> | <> | <> | <> | | |
| | # | F | F | F | F | F | F | F | F | T | | |
| | # | F | F | T | F | T | F | T | F | T | | |
| | # | F | T | F | T | F | F | T | F | T | | |
| | # | F | T | T | T | T | T | T | F | F | | |
| |---+---+---+---+------------+------------+-----+------------+-----+---------------------------| | |
| | # | T | F | F | T | T | T | F | F | F | | |
| | # | T | F | T | T | T | T | T | T | T | | |
| | # | T | T | F | T | T | T | T | T | T | | |
| | # | T | T | T | T | T | T | T | T | T | | |
| - Not a tautology | |
| ** Exercise 4: Determine Well-formedness, and build a truth table | |
| *** $(True \wedge P) \vee Q$ | |
| - Truth table from Ex 3.1 | |
| - See that it is satisfiable, but not a tautology | |
| *** $((P \vee Q) \wedge (P \vee R)) \Leftrightarrow (P \wedge (Q \vee R))$ | |
| - Truth table from Ex 3.5 | |
| - Satisfiable, but not a tautology | |
| *** $((P \wedge \neg Q) \vee (Q \wedge \neg P)) \Rightarrow \neg(P \Leftrightarrow Q)$ | |
| | | P | Q | A=$P \wedge \neg Q$ | B=$Q \wedge \neg P$ | A \vee B | C=$(P \Leftrightarrow Q)$ | $\neg C$ | $(A \vee B) \Rightarrow C$ | | |
| |---+---+---+---------------------+---------------------+----------+---------------------------+----------+----------------------------| | |
| | / | < | > | <> | <> | <> | <> | <> | <> | | |
| | # | T | T | F | F | F | T | F | T | | |
| | # | T | F | T | F | T | F | T | T | | |
| | # | F | T | F | T | T | F | T | T | | |
| | # | F | F | F | F | F | T | F | T | | |
| - Tautology | |
| *** $(P \Rightarrow Q) \wedge (P \Rightarrow \neg Q)$ | |
| | | P | Q | LHS=$P \Rightarrow Q$ | RHS=$P \Rightarrow \neg Q$ | LHS \wedge RHS | | |
| |---+---+---+-----------------------+---------------------------+----------------| | |
| | / | < | > | <> | <> | <> | | |
| | # | T | T | T | F | F | | |
| | # | T | F | F | T | F | | |
| | # | F | T | T | T | T | | |
| | # | F | F | T | T | T | | |
| - Satisfiable, but not a tautology | |
| *** $(P \Rightarrow Q) \wedge (\neg P \Rightarrow Q)$ | |
| | | P | Q | LHS=$P \Rightarrow Q$ | RHS=$\neg P \Rightarrow Q$ | LHS \wedge RHS | | |
| |---+---+---+-----------------------+----------------------------+----------------| | |
| | / | < | > | <> | <> | <> | | |
| | # | T | T | T | T | T | | |
| | # | T | F | F | T | F | | |
| | # | F | T | T | T | T | | |
| | # | F | F | T | F | F | | |
| - Satisfiable, but not a tautology | |
| *** $(P \Rightarrow Q) \Leftrightarrow (\neg Q \Rightarrow \neg P)$ | |
| | | P | Q | LHS=$P \Rightarrow Q$ | RHS=$\neg Q \Rightarrow \neg P$ | LHS \Leftrightarrow RHS | | |
| |---+---+---+-----------------------+---------------------------------+-------------------------| | |
| | / | < | > | <> | <> | <> | | |
| | # | T | T | T | T | T | | |
| | # | T | F | F | F | T | | |
| | # | F | T | T | T | T | | |
| | # | F | F | T | T | T | | |
| - Tautology | |
| - (This is just the contrapositive) | |
| * Natural Deduction: Inference Reasoning | |
| ** Introduction | |
| - Natural deduction allows us to reason about logical propositions without substituting values for variables | |
| - *Logical Inference*: reasoning formally about a set of statements. Requires: | |
| + *Object Language*: to talk about the statements we're reasoning about. e.g. Propositional expressions | |
| + *Inference Rules*: Rules to infer new facts from information given | |
| + *Meta Language*: Defines the "form of argument" so that we can determine whether arguments are actually valid | |
| *** Definition: Sequent ($\vdash$) | |
| - $P_1, P_2, \cdots, P_n \vdash Q$ is called a *sequent* | |
| - Means: if all propositions $P_1, \cdots, P_n$ are known, then proposition $Q$ can be inferred formally using the rules of natural deduction | |
| - e.g. Difference between $P \vDash Q \Rightarrow P$ and $P \vdash Q \Rightarrow P$ | |
| + The $\vDash$ version doesn't say *how* we know that $Q \Rightarrow P$ when we assume $P$. It just says that it is True. | |
| + The $\vdash$ version says that there is a proof that shows $Q \Rightarrow P$ when we assume $P$ | |
| *** Meta Variables | |
| - Meta variables can stand for any WFF proposition | |
| - e.g. we can have $a$ be $P \wedge Q$ | |
| - Convention: meta variables will be written in lower case, propositional variables in upper case | |
| *** Writing an Inference Rule | |
| - Assumptions are written above a horizontal line | |
| - Conclusion written below the line. | |
| - (For latex simplicity, I'll just use the sequent notation to talk about inference rules) | |
| - *Inference rule only works in one direction* | |
| ** Definitions of True, Not and Equivalence | |
| *** Primitives | |
| - Only primitive objects are constant False, and $\vee, \wedge, \Rightarrow$ | |
| - All other objects are built using these | |
| - Below we give definitions for some primitives | |
| - can be verified using truth tables | |
| - But we'll only manipulate them using rules of logical deduction | |
| *** Definition: True | |
| - $True = False \Rightarrow False$ | |
| - (Verify using truth table, but this particular definition is "trivial" because that's how we defined implication) | |
| *** Definition: Negation | |
| - $\neg a = a \Rightarrow False$ | |
| - Proof (via truth tables): | |
| - Suppose $a$ is $True$, then right side becomes $True \rightarrow False$, which is $False$ | |
| - Suppose $a$ is $False$, then right side becomes $False \rightarrow False$, which we defined to be $True$ | |
| - So in both cases the definition is consistent | |
| - Consistency (via logical inference only): | |
| - If $a$ is $True$, then $\neg True$ is $True \Rightarrow False$ which is $(False \Rightarrow False) \Rightarrow False$ | |
| - We have a rule called Reduction Ad Absurdum which allows us to infer $False$ from $(False \Rightarrow False) \Rightarrow False$ | |
| - If $a$ is $False$, then $\neg False$ is $False \Rightarrow False$< which we defined to be $True$ | |
| *** Definition: Equivalence | |
| - $a \Leftrightarrow b = (a \Rightarrow b) \wedge (b \Rightarrow a)$ | |
| - (Note that's the definition of if and only if) | |
| - Proof by Truth Table: | |
| | | a | b | a \Rightarrow b | b \Rightarrow a | LHS | RHS | | |
| | / | < | > | <> | <> | <> | <> | | |
| |---+---+---+-----------------+------------------+-----+-----| | |
| | # | T | T | T | T | T | T | | |
| | # | T | F | F | T | F | F | | |
| | # | F | T | T | F | F | F | | |
| | # | F | F | T | T | T | T | | |
| - Hence, this formula is also correct | |
| ** IMPORTANT: Note on Proofs of the Inference Rules | |
| - I've "proven" each of the inference rules by making references to the Truth Table | |
| - But it looks like that might be circular atleast based on the discussion in the section on "Inferring the Operator Truth Tables" | |
| - Assume that you have a system with FALSE, and three operators OR, AND, IMPLIES | |
| - Pretend that it is just a coincidence that they match the names of Boolean operators | |
| ** And Introduction | |
| *** Definition: $a, b \vdash a \wedge b$ | |
| - Proof: | |
| + We know that $a$ and $b$ are True | |
| + By definition of $\wedge$, $a \wedge b$ is True | |
| *** Usage Example 1 | |
| - Statement: $(R \Rightarrow S), \neg P \vdash (R \Rightarrow S) \wedge \neg P$ | |
| - Proof: | |
| + Use _and introduction_ | |
| *** Usage Example 2 | |
| - Statement: $P, Q, R \vdash (P \wedge Q) \wedge R$ | |
| - Proof: | |
| + If $P$ and $Q$ are True, $P \wedge Q$ is True by _and introduction_ | |
| + Since, $R$ is True, another usage of _and introduction_ means $(P \wedge Q) \wedge R$ is True as well | |
| - Note: This can be written in a tree diagram type form (Page 130) | |
| *** Exercise 10: | |
| - *Statement*: Prove $P, Q, R \vdash P \wedge (Q \wedge R)$ | |
| - Proof: | |
| + If $Q$ and $R$ are True, $Q \wedge R$ is true by _and introduction_ | |
| + If, $P$ is true, another application of _and introduction_ means $P \wedge (Q \wedge R)$ is True as well | |
| - Note, we could have proven this simply by noting the associativity of $\wedge$ | |
| *** Exercise 11 | |
| **** Shape of $x = A \wedge (B \wedge (C \wedge D))$ | |
| - Right-heavy tree | |
| - If there are $2^n$ variables in $x$, then the height of the proof tree will also be $2^n$ | |
| - (At each level, we can reason about one of the variables in x) | |
| **** Shape of $y = (A \wedge B) \wedge (C \wedge D))$ | |
| - Balanced tree: height is logarithmic in number of variables | |
| - (At each level, we can reason about half of the variables in y) | |
| ** And Elimination | |
| *** Definition: $(a \wedge b) \vdash a$, $(a \wedge b) \vdash b$ | |
| - Proof: | |
| + We know that $a \wedge b$ is True | |
| + But $a \wedge b$ is True exactly when both $a$ and $b$ are True | |
| + So, if the conjunction is True, they must individually be True as well | |
| *** Usage Example | |
| - Statement: $P, Q \wedge R \vdash P \wedge Q$ | |
| - Proof: | |
| + $P$ is True by assumption | |
| + $Q \wedge R$ means $Q$ is True by _and elimination_ | |
| + Since both $P$ and $Q$ are true, $P \wedge Q$ is True (by _and introduction_) | |
| *** Usage Example | |
| - Statement: $(P \wedge Q) \wedge R \vdash R \wedge Q$ | |
| - Proof: | |
| + By _and elimination_, both $P \wedge Q$ and $R$ are True | |
| + Another _and elimination_ on $P \wedge Q$ yields True for $P$ and $Q$ | |
| + So, both $Q$ and $R$ are True, by _and introduction_, $Q \wedge R$ is True | |
| *** Usage Example | |
| - Statement: $P \wedge Q \vdash Q \wedge P$ | |
| - Proof: | |
| + By _and elimination_, both $P$ and $Q$ are True | |
| + By _and introduction_, $Q \wedge P$ is True | |
| - This proves the commutativity of And (which we could have also done using Truth Tables) | |
| *** Usage Example | |
| - Statement: $a \wedge (b \wedge c) \vdash (a \wedge b) \wedge c$ | |
| - Proof: | |
| + By _and elimination_ on $a \wedge (b \wedge c)$, both $a$ and $b \wedge c$ are True | |
| + By _and elimination_ on $b \wedge c$, both $b$ and $c$ are True | |
| + By _and introduction_, $a \wedge b$ is True | |
| + By _and introduction_, $(a \wedge b) \wedge c$ is True | |
| - We've proved the associativity of and | |
| *** Exercise 12 | |
| - Statement: Prove: $(P \wedge Q) \wedge R \vdash P \wedge (Q \wedge R)$ | |
| - Proof: | |
| + We proved that "and" is associative for well formed propositions | |
| + This is a well formed proposition | |
| ** Imply Elimination | |
| *** Definition: $a, a \Rightarrow b \vdash b$ | |
| - Also known as *Modus Ponens* | |
| - Proof: | |
| + Know $a$ is True | |
| + Know $a \Rightarrow b$ is True | |
| + If $b$ is False, we get $True \Rightarrow False$ which would be False | |
| + But if $b$ is True, we get $True \Rightarrow True$, which is True | |
| + So, $b$ is True | |
| *** Usage Example | |
| - Statement: $Q \wedge P, P \wedge Q \Rightarrow R \vdash R$ | |
| - Proof: | |
| + $Q \wedge P$ is True which means that $P \wedge Q$ is true by the commutativity of and (proved earlier) | |
| + By _Modus Ponens_ on $P \wedge Q \Rightarrow R$, we get $R$ is True | |
| *** Usage Example | |
| - Statement: $a, a \Rightarrow b, b \Rightarrow c \vdash c$ | |
| - Proof: | |
| + By _Modus Ponens_ on $a, a \Rightarrow b$, we see that $b$ is True | |
| + By _Modus Ponens_ on $b, b \Rightarrow c$, we see that $c$ is True | |
| *** Exercise 13 | |
| - Statement: $P, P \Rightarrow Q, (P \wedge Q) \Rightarrow (R \wedge S) \vdash S$ | |
| - Proof: | |
| + By _Modus Ponens_ on $P, P \Rightarrow Q$, we see that $Q$ is True | |
| + By _And Introduction_, $P \wedge Q$ is True | |
| + By _Modus Ponens_ on $P \wedge Q, P \wedge Q \Rightarrow R \wedge S$, we see that $R \wedge S$ is True | |
| + By _And Elimination_ on $R \wedge S$, we see that both $R$ and $S$ are True | |
| *** Exercise 14 | |
| - Statement: $P \Rightarrow Q, R \Rightarrow S, P \wedge R \vdash S \wedge R$ | |
| - Proof: | |
| + By _And Elimination_ on $P \wedge R$, we see that $P$ and $R$ are True | |
| + By _Modes Ponens_ on $R, R \Rightarrow S$, we see that $S$ is True | |
| + By _And Introduction_ on $R$ and $S$, we see that $S \wedge R$ is True | |
| ** Imply Introduction | |
| *** Definition: $(a \vdash b) \vdash (a \Rightarrow b)$ | |
| - "In order to imply the logical implication $a \Rightarrow b$, you must have a proof of $b$ using $a$ as an assumption" | |
| *** Example Usage | |
| - Statement: $\vdash (P \wedge Q) \Rightarrow Q$ | |
| - Since the $\vdash$ doesn't have anything to the left, it is saying that this is a tautology | |
| - What proof do we have for this? | |
| + Consider the sequent $P \wedge Q \vdash Q$, which is just _and elimination_ | |
| + So, we have a proof for $P \wedge Q \vdash Q$, which means we can write $\vdash P \wedge Q \Rightarrow Q$ by Implies introduction | |
| **** Assumptions Made | |
| - _And Elimination_ assumed $P \wedge Q$ is True. | |
| - We can't infer $Q$ without this assumption. | |
| - So, this appears in the sequent to the left of the $\vdash$ in $P \wedge Q \vdash Q$ | |
| - But the entire sequent $P \wedge Q \vdash Q$ doesn't have any further assumptions | |
| + Whenever $P \wedge Q$ is true, $Q$ is true. | |
| - So, this sequent can be put in as an assumption without adding any other assumptions | |
| - This is why when we do implies introduction, we get $\vdash (P \wedge Q) \Rightarrow Q$ | |
| *** Discharged assumptions | |
| - Assumptions that are made temporarily to establish a sequent, and which is then thrown away | |
| - E.g. to establish the sequent $P \wedge Q \vdash Q$, we made an assumption $P \wedge Q$ | |
| - Once we got $P \wedge Q \vdash Q$, we don't need to assumption for any other purpose | |
| - Indicate discharged assumptions by boxes | |
| *** Implication Chain Rule | |
| - Statement: $a \Rightarrow b, b \Rightarrow c \vdash a \Rightarrow c$ | |
| - Proof: | |
| + Since we are trying to prove $a \Rightarrow c$, we must use _Imply Introduction_ somewhere | |
| + This means that we need to show $a \vdash c$ | |
| + Assume $a$ is True, then by _Modus Ponens_ on $a \Rightarrow b$, $b$ is True | |
| + Since $b$ is True, by _Modus Ponens_ on $b \Rightarrow c$, $c$ is True | |
| + So, we have a sequent $a \vdash c$, and we can discharge the assumption that $a$ is True | |
| + By _Imply Introduction_ on $a \vdash c$, we get $a \implies c$ | |
| *** Modus Tollens | |
| - Statement: $a \Rightarrow b, \neg b \vdash \neg a$ | |
| - Proof: | |
| + $\neg a$ is an abbreviation for $a \Rightarrow False$ | |
| + This means that we need to use _Imply Introduction_ | |
| + Expand $\neg a$ and $\neg b$ to get: $a \Rightarrow b, b \Rightarrow False \vdash a \Rightarrow False$ | |
| + This is just _implication chain rule_ | |
| *** Exercise 15 | |
| - Statement: $P \vdash Q \Rightarrow P \wedge Q$ | |
| - Proof: | |
| + We are trying to prove an implication $Q \Rightarrow P \wedge Q$, means we have to _Imply Introduction_ | |
| + To _introduce imply_, we need to prove the sequent $Q \vdash P \wedge Q$ | |
| + We know that $P$ is true from what is given | |
| + Assume that $Q$ is true. | |
| + By _and introduction_, we have $P, Q \vdash P \wedge Q$ | |
| + This sequent does not have any further assumptions, so we can discharge the assumption that B is True | |
| + So, we have the sequent $Q \vdash P \wedge Q$, which means we have $Q \Rightarrow P \wedge Q$ by _introduce imply_ | |
| - (Maybe incorrect) | |
| *** Exercise 16 | |
| - Statement: $\vdash P \wedge Q \Rightarrow Q \wedge P$ | |
| - Proof: | |
| + We need to use _introduce imply_ on the sequent $P \wedge Q \vdash Q \wedge P$ | |
| + But that's just commutativity of $\wedge$, which we proved earlier, the sequent holds without any further assumptions | |
| + So, we can _introduce imply_ on the sequent to get the desired answer | |
| ** Or Introduction | |
| *** Definition: $a \vdash a \vee b$ and $b \vdash a \vee b$ | |
| - Proof | |
| + By the definition of $\vdash$, if one of its arguments is true, then the whole expression becomes true | |
| *** Example Usage | |
| - Statement: $P \wedge Q \vdash P \vee Q$ | |
| - Proof | |
| + By _and elimination_ on $P \wedge Q$, we have $P$ is True, $Q$ is True | |
| + By _or introduction_, we have $P \vee Q$ is True | |
| *** Exercise 17 | |
| - Statement: $P \Rightarrow False \vee P$ | |
| - Proof | |
| + To prove this implication, we need to prove the sequent $P \vdash False \vee P$ | |
| + But that sequent is True by _or introduction_ | |
| + So, by _introduce implication_, we have $P \Rightarrow False \vee P$ | |
| *** Exercise 18 | |
| - Statement: $P, Q \vdash (P \wedge Q) \vee (Q \vee R)$ | |
| - Proof: | |
| + By _and introduction_, we have $P \wedge Q$ is True | |
| + By _or introduction_, we have $Q \vee R$ is True | |
| + By _or introduction_, $(P \wedge Q) \vee (Q \vee R)$ is True | |
| + (Actually, knowing that $P \wedge Q$ is True is sufficient because we can _or introduce_ that to get True) | |
| ** Or Elimination | |
| *** Definition (((a \vee b), (a \vdash c), (b \vdash c)) \vdash c) | |
| - This is *Proof by Case Analysis* | |
| - Proof: | |
| + Assumption is that $a \vee b$ is True | |
| + By the definition of $\vee$ (from Truth Table), atleast one of $a$ and $b$ must be True | |
| + Suppose $a$ is True | |
| + We have $a \vdash c$, i.e. a proof that $c$ is True when $a$ holds | |
| + Otherwise, $b$ is True | |
| + We have $b \vdash c$, i.e. a proof that $c$ is True when $a$ holds | |
| + So, $c$ is True whenever the assumptions hold | |
| - (Did i just prove Proof by Case Analysis by DOING proof of case analysis? Something is weird here...) | |
| *** Example Usage | |
| - Statement: $(P \wedge Q) \vee (P \wedge R) \vdash P$ | |
| - Proof: | |
| + Suppose $P \wedge Q$ is True, then by _and elimination_, $P$ is True | |
| + Suppose instead that $P \wedge R$ is True, then by _and elimination_, $P$ is True | |
| + So, we have $((P \wedge Q) \vee (P \wedge R)), (P \wedge Q) \vdash P, (P \wedge R) \vdash P$ | |
| + Use _or elimination_ to get that $P$ is True | |
| *** Example Usage | |
| - Statement: $(a \wedge b) \vee (a \wedge c) \vdash (b \vee c)$ | |
| - Proof: | |
| + Assume $a \wedge b$ by _and elimination_, we get $a \wedge b \vdash b$ | |
| + Discharge the assumption $a \wedge b$ because we have a sequent | |
| + By _or introduction_, we have $b \vdash b \vee c$ | |
| + Assume $a \wedge c$ by _and elimination_, we get $a \wedge c \vdash c$ | |
| + Discharge the assumption $a \wedge c$ | |
| + By _or introduction_, we have $c \vdash b \vee c$ | |
| + We can no do _or elimination_ on $(a \wedge b) \vee (a \wedge c) \vdash (b \vee c), ((a \wedge b) \vdash b) \vdash b \vee c, ((a \wedge c) \vdash c) \vdash b \vee c$ | |
| + This gives us $b \vee c$ | |
| ** Identity | |
| *** Definition $a \vdash a$ | |
| - It is necessary because we can't prove $P \vdash P$ without it. | |
| *** Theorem: $\vdash True$ | |
| - By definition, $True = False \Rightarrow False$ | |
| - So, we need to _introduce imply_ to prove this | |
| - To introduce imply, we need to prove the sequent $False \vdash False$ | |
| - This is true by _identity_ | |
| - So, we have $False \Rightarrow False$ or equivalently, $True$ | |
| ** Contradiction | |
| *** Definition: $False \vdash a$ | |
| - Anything can be inferred if the assumption is False | |
| - (Remember the Truth table for $P \Rightarrow Q$ gave True when $P$ was False?) | |
| - Expresses the fact that *False is untrue* purely using logical inference | |
| + Can't just say False is not True, because we defined True that way | |
| + Also doesn't rely on us making "intuitionistic" statements like "False is Wrong" | |
| *** Example Usage | |
| - Statement: $P, \neg P \vdash Q$ | |
| - Proof: | |
| + $\neg P$ is shorthand for $P \Rightarrow False$ | |
| + So, from $P, P \Rightarrow False$ by _modus ponens_, we have $False$ | |
| + $False \vdash Q$ follows from _contradiction_ | |
| *** Example Usage | |
| - Statement; $a \vee b, \neg a \vdash b$ | |
| - Proof: | |
| + $\neg a$ is shorthand for $a \Rightarrow False$ | |
| + Performing _or elimination_ on $a \vee b$, | |
| + Assume $a$ is True, then we have $a, a \Rightarrow False$, which by _Modus Ponens_ gives us $False$ | |
| + So, by _contradiction_, $b$ is True | |
| + (Discharge the assumption that $a$ is True) | |
| + Assume $b$ is True, the by identity, $b$ is True | |
| + (Discharge the assumption that $b$ is True) | |
| + Combining, we have $(a \vee b, \neg a), (((a \vee b) \vdash a), a \Rightarrow False) \vdash b, (((a \vee b) \vdash b) \vdash b)$, we can now perform or elimination | |
| ** Reduction Ad Absurdum | |
| *** Definition: $(\neg a \vdash False) \vdash a$ | |
| - If you can infer False from an assumption $\neg a$, then you must conclude that a is true | |
| - This is the Proof by Contradiction strategy | |
| *** Example Usage | |
| - Statement: $\neg \neg a \vdash a$ | |
| - Proof: | |
| + Strategy: Assume $\neg a$ and show that it leads us to infer False (proof by contradiction) | |
| + Assuming $\neg a$, we have $\neg a, \neg \neg a$ | |
| + Expand out the abbreviations to get: $a \Rightarrow False, (a \Rightarrow False) \Rightarrow False$ | |
| + Since we have $a \Rightarrow False$ and $(a \Rightarrow False) \Rightarrow False$, by _Modus Ponens_, we have $False$ | |
| + So, by reductio ad absurdum, $a$ Must be True if $\neg \neg a$ is True | |
| ** Inferring the Operator Truth Tables | |
| - Two fundamental questions: | |
| + Are inference rules powerful enough? | |
| + Will they ever allow us to make mistakes? | |
| - profound and difficult questions, modern research has shown some astonishing results | |
| - Easy version of first question: Are inference rules powerful enough to infer the truth tables of logical operators? | |
| *** Example: Deriving the Truth Table value of $True \wedge False$ | |
| - Want to show that it is logically equivalent to False, and not logically equivalent to True | |
| - To show equivalence with False, we need to show: $False \Rightarrow (True \wedge False)$, $True \wedge False \Rightarrow False$ | |
| + $False \vdash (True \wedge False)$ follows from _contradiction_ | |
| + By _introduce implication_, we have $False \Rightarrow (True \wedge False)$ | |
| + $True \wedge False \vdash False$ | |
| + Expand out $True$ the expression is now $False \wedge (False \Rightarrow False)$ | |
| + By _and elimination_, we get $False \wedge (False \Rightarrow False) \vdash False$, which by identity gives us $False \vdash False$ | |
| + By _introduce implication_, we have $True \wedge False \Rightarrow False$ | |
| *** Exercise: Calculating value of $True \wedge True$ | |
| - Proof that $True \wedge True \Rightarrow True$ | |
| + By _and elimination_, we have $True \wedge True \vdash True$ | |
| + By _identity_, we have $True \vdash True$ | |
| + By _introduce implication_, we have $True \wedge True \Rightarrow True$ | |
| - Proof that $True \Rightarrow (True \wedge True)$ | |
| + Need to prove the sequent $True \vdash True \wedge True$ | |
| + By _and introduction_, we have $True \vdash True \wedge True$ | |
| + By _introduce implication_, we have $True \Rightarrow True \wedge True$ | |
| *** Exercise: Calculating the value of $True \vee False$ | |
| - Proof that $True \vee False \Rightarrow True$ | |
| + We have $True \vdash True$ from _identity_ | |
| + We have $False \vdash True$ from _contradiction_ | |
| + So, we have $(True \vee False), (True \vdash True), (False \vdash True)$ | |
| + By _or elimination_, we have $(True \vee False) \vdash True$ | |
| + By _introduce implication_, we have $True \vee False \Rightarrow True$ | |
| - Proof that $True \Rightarrow (True \vee False)$ | |
| + From _or introduction_, we have $True \vdash (True \vee False)$ | |
| + By _introduce implication_, we have $True \Rightarrow (True \vee False)$ | |
| *** Extra Credit: What happens when we try to say $True \vee False$ is $False$? | |
| - Need to show equivalence | |
| - Proof that $False \Rightarrow (True \vee False)$ | |
| + $False \vdash (True \vee False)$ by _contradiction_ | |
| + By _introduce implication_, we have $False \Rightarrow (True \vee False)$ | |
| - Proof that $(True \vee False) \Rightarrow False$ | |
| + Need to do an _or elimination_ | |
| + $False \vdash False$ comes from _identity_ | |
| + $True \vdash False$ needs to be shown | |
| + Expand out $True$: $False \Rightarrow False \vdash False$ needs to be shown | |
| + Since $False$ is not $True$, we can't use _Modus Ponens_ | |
| + We have no applicable inference rule to use | |
| *** Exercise | |
| - When we computed value of $True \wedge False$, we used _and elimination_ to say that $(False \Rightarrow False) \wedge False \vdash False$ | |
| - But we could have said $(False \Rightarrow False) \vdash False \vdash (False \Rightarrow False)$ which is True | |
| - What would have happened then? | |
| + We would have had to show that $True \vdash False$ | |
| + That is, $False \Rightarrow False \vdash False$ | |
| + Same situation as in extra credit: Have no valid inference law to use; so can't deduce. | |
| * Proof Checking by Computer | |
| ** Proof Checkers and Theorem Provers | |
| - *Proof Checker*: reads in a theorem and a proof. Determines if the proof is valid | |
| - *Theorem Prover*: reads in a theorem and attempts to generate a proof | |
| ** Example of Proof Checking | |
| - See 06-proofs.hs | |
| * Boolean Algebra: Equational Reasoning | |
| ** Introduction | |
| *** Approaches to Propositional Logic | |
| - Truth Tables: semantic approach | |
| - Natural Deduction: syntactic approach | |
| - Boolean Algebra: axiomatic approach | |
| *** Equational Reasoning | |
| - Show that two values are the same by building chains of equalities | |
| + e.g. show that $a = b$ and $b = c$, so $a = c$ | |
| - can substitute equals for equals | |
| + if $x = y$, can substitute in $x$ wherever $y$ is used | |
| ** Laws of Boolean Algebra | |
| *** Operations with Constants | |
| - $a \wedge False = False$ | |
| - $a \wedge True = True$ | |
| - *Identity for or*: $a \vee True = True$ | |
| - *Identity for and*: $a \vee False = a$ | |
| **** Exercise 25: Simplification | |
| - $(P \wedge False) \vee (Q \wedge True)$ | |
| - $False \vee (Q \wedge True)$ | |
| - $Q \wedge True$ | |
| - $Q$ | |
| **** Exercise 26 | |
| - Prove that: $(P \wedge False) \wedge True) = False$ | |
| - Direct Proof: | |
| + $(P \wedge False) \wedge True)$ | |
| + $False \wedge True$ | |
| + $False$ | |
| *** Basic Properties of $\wedge$ and $\vee$ | |
| - *Disjunctive Implication*: $a \Rightarrow a \vee b$ (Or Introduction) | |
| - *Conjunctive Implication*: $a \wedge b \Rightarrow a$ (And Elimination) | |
| - *Idempotence*: $a \wedge a = a$ | |
| - *Idempotence*: $a \wedge a = a$ | |
| - *Commutative*: $a \wedge b = b \wedge a$ | |
| - *Commutative*: $a \vee b = b \vee a$ | |
| - *Associativity*: $(a \wedge b) \wedge c = a \wedge (b \wedge c)$ | |
| - *Associativity*: $(a \vee b) \vee c = a \wedge (b \vee c)$ | |
| **** Exercise 27 | |
| - Prove: $(P \wedge ((Q \vee R) \vee Q)) \wedge S = S \wedge ((R \vee Q) \wedge P)$ | |
| - Direct Proof starting from LHS | |
| - $(P \wedge ((Q \vee R) \vee Q)) \wedge S$ | |
| - $(P \wedge ((R \vee Q) \vee Q)) \wedge S$ (by commutativity of or) | |
| - $(P \wedge (R \vee (Q \vee Q)) \wedge S$ (by associativity of or) | |
| - $(P \wedge (R \vee Q)) \wedge S$ (by idempotence of or) | |
| - $((R \vee Q) \wedge P) \wedge S$ (by commutivatiy of and) | |
| - $S \wedge ((R \vee Q) \wedge P)$ (by commutivatiy of and) | |
| **** Exercise 28 | |
| - Prove: $P \wedge (Q \wedge (R \wedge S)) = ((P \wedge Q) \wedge R) \wedge S$ | |
| - Direct proof starting from LHS | |
| - $P \wedge (Q \wedge (R \wedge S))$ | |
| - $((P \wedge Q) \wedge (R \wedge S))$ (by associativity of and) | |
| - $((P \wedge Q) \wedge R) \wedge S$ (by associativity of and) | |
| *** Distributive and De Morgan's Laws | |
| - *And distributes over Or*: $a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)$ | |
| - *Or distributes over And*: $a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)$ | |
| - *De Morgan*: $\neg (a \wedge b) = \neg a \vee \neg b$ | |
| - *De Morgan*: $\neg (a \vee b) = \neg a \wedge \neg b$ | |
| **** Exercise 29 | |
| - Give an intuitive explanation of second De Morgan's laws | |
| - If none of (a, b) are true, it means that a is not true and b is not true | |
| *** Laws on Negation | |
| - $\neg True = False$ | |
| - $\neg False = True$ | |
| - $a \wedge \neg a = False$ | |
| - $a \vee \neg a = True$ | |
| - $\neg (\neg a) = a$ | |
| *** Laws on Implication | |
| - *Modus Ponens*: $a \wedge (a \Rightarrow b) \Rightarrow b$ | |
| - *Modus Tollens*: $\neg b \wedge (a \Rightarrow b) \Rightarrow \neg a$ | |
| - *Disjunctive Syllogism*: $(a \vee b) \wedge \neg \Rightarrow b$ | |
| - *Implication Chain*: $(a \Rightarrow b) \wedge (b \Rightarrow c) \Rightarrow (a \Rightarrow c)$ | |
| - *Implication Combination*: $(a \Rightarrow b) \wedge (c \Rightarrow d) \Rightarrow ((a \wedge c) \Rightarrow (b \wedge d))$ | |
| - *Currying*: $(a \wedge b) \Rightarrow c = a \Rightarrow b \Rightarrow c$ | |
| - *Implication*: $a \Rightarrow b = \neg a \wedge b$ | |
| - *Contrapositive*: $a \Rightarrow b = \neg b \Rightarrow \neg a$ | |
| - *Absurdity*: $(a \Rightarrow b) \wedge (a \Rightarrow \neg b) = \neg a$ | |
| **** Understanding the currying law | |
| - Says there are two equivalent ways of establishing that $a$ and $b$ both hold | |
| - One of them is to say $a \wedge b$ | |
| - The other is to have an implication on $a$ and an implication on $b$ | |
| - If either of $a$ or $b$ is false, | |
| + $a \wedge b$ is false, so $(a \wedge b) \Rightarrow c$ is vacuous | |
| + Either $a \wedge b$ or $b \wedge c$ is vacuous (if $a$ is False, then the first one is vacuous, if $b$ is false, the second one) | |
| **** Understanding the Implication Law | |
| - allows us to prove $a \Rightarrow b$ | |
| - Note that we don't have an "Introduce Implication" rule like in natural deduction | |
| - So we use this rule | |
| *** Logical Equivalence | |
| - $a \Leftrightarrow b$ is the same as $(a \Rightarrow b) \wedge (b \Rightarrow a)$ | |
| - Subtle difference between $\Leftrightarrow$ and $=$ | |
| + $=$ is an operator in the meta language that says that two sides of an equation have the same value | |
| + $\Leftrightarrow$ is in the object language itself and it gives a new proposition | |
| **** Exercise 30 | |
| - Prove: $(A \vee B) \wedge B \LeftRightarrow B$ | |
| - Strategy: We'll reduce the left side of the equivalence to be the right side | |
| - $(A \vee B) \wedge B$ | |
| - $(A \vee B) \wedge (B \vee False)$ (by Identity of OR) | |
| - $(B \vee A) \wedge (B \vee False)$ (commutativity of AND) | |
| - $B \vee (A \wedge False)$ (distributivity of OR) | |
| - $B \vee False$ | |
| - $B$ | |
| **** Exercise 31 | |
| - Prove: $((\neg A \wedge B) \vee (A \wedge \neg B)) \Leftrightarrow (A \vee B) \wedge (\neg (A \wedge B))$ | |
| - Direct proof starting from "left side" | |
| - $(\neg A \wedge B) \vee (A \wedge \neg B)$ | |
| - $(\neg A \vee (A \wedge \neg B)) \wedge (B \vee (A \wedge \neg B))$ (by distributing the OR over the AND) | |
| - $((\neg A \vee A) \wedge (\neg A \vee \neg B)) \wedge ((B \vee A) \wedge (B \vee \neg B))$ (by distributing the OR over the AND) | |
| - $(True \wedge (\neg A \vee \neg B)) \wedge ((B \vee A) \wedge True)$ | |
| - $(\neg A \vee \neg B) \wedge (B \vee A)$ | |
| - $\neg (A \wedge B) \wedge (B \vee A)$ (by Demorgan's laws) | |
| **** Exercise 32 | |
| - Prove: $\neg (A \wedge B) \equiv \neg A \vee \neg B$ | |
| - Direct proof starting from "right side" | |
| - $\neg A \vee \neg B$ | |
| - $\neg (\neg (\neg A \vee \neg B))$ (Double negation is just identity) | |
| - $\neg (A \wedge B)$ (by De Morgan's other law) | |
| **** Exercise 33 | |
| - Prove: $(A \vee B) \wedge (\neg A \vee C) \wedge (B \vee C) \Leftrightarrow (A \vee B) \wedge (\neg A \vee C)$ | |
| - Proof is by cases on A | |
| - Case: A is True | |
| - LHS: $(True \vee B) \wedge ((\neg True) \vee C) \wedge (B \vee C)$ | |
| - i.e. $True \wedge C \wedge (B \vee C)$ | |
| - i.e. $C \wedge (B \vee C)$ | |
| - i.e. $C$ (proven in Review Exercise 45) | |
| - RHS: $(True \vee B) \wedge ((\neg True) \wedge C)$ | |
| - i.e. $True \wedge C$ | |
| - i.e. $C$ | |
| - So the equality holds in this case | |
| - Case: A is False | |
| - LHS: $(False \vee B) \wedge ((\neg False) \vee C) \wedge (B \vee C)$ | |
| - i.e. $B \wedge True \wedge (B \vee C)$ | |
| - i.e. $B \wedge (B \vee C)$ | |
| - i.e. $B$ | |
| - RHS: $(False \vee B) \wedge ((\neg False) \vee C)$ | |
| - i.e. $B \wedge True$ | |
| - i.e. $B$ | |
| - So, the equality holds in this case | |
| - Since the equality holds in both cases, the statement is proven. | |
| * Logic in Computer Science | |
| - Talks about applications of theorem provers | |
| * Meta Logic | |
| - Making statements about the logical system itself | |
| - Fundamental Meta-Logic operators: | |
| + $P_1, P_2, \cdots, P_n \vdash Q$ means there is a proof that shows $Q$ from the assumptions $P_1, \cdots, P_n$ | |
| + $P_1, P_2, \cdots, P_n \vDash Q$ means $Q$ must be tree if all assumptions are true, but says nothing about the proof | |
| ** Definition: Consistency of a Logical System | |
| - A formal system is consistent if, for all well-formed formulas $a$ and $b$, if $a \vdash b$ then $a \vDash b$ | |
| - That is, each proposition that is provable is actually True | |
| ** Definition: Completeness of a Logical System | |
| - A formal system is complete if, for all well-formed formulas $a$ and $b$, if $a \vDash b$ then $a \vdash b$ | |
| - That is, every proposition that is true can be proved using the system | |
| ** Theorem: Propositional Logic is consistent and complete | |
| - No proof given | |
| ** Godel's Theorem: A logical system powerful enough to express ordinary arithmetic must be either inconsistent or incomplete | |
| - It is impossible to capture all of mathematics in a safe logical system | |
| * Further Reading | |
| - *Forever Undecided: A Puzzle Guide to Godel* by Raymond Smullyan | |
| + "Don't miss it" | |
| - *Godel, Escher, Bach: An Eternal Braid* by Douglas Hofstadter | |
| + "Another unmissable classic" | |
| - *How to Prove it: A Structured approach* by Daniel Velleman | |
| + Good source for hints on carrying out proofs with lots of example | |
| - *Computer-Aided Reasoning: An approach*: by Matt Kaufmann, Panagiotis Manolios, and J Strother Moore | |
| + Describes the ACL2 theorem prover | |
| - *Introduction to HOL*: by M Gordon and T Melham | |
| - Describes the HOL theorem prover | |
| - *Logic for Mathematics and Computer Science* by Burris | |
| + "more advanced treatement of mathematical logic" | |
| - *A Mathematical Introduction to Logic* by Enderton | |
| + "standard presentation of logic from a mathematical perspective" | |
| - *Type Theorey and Functional Programming* by Thompson | |
| + "detailed development of relationship between inference rules and rules used to define type systems" | |
| - *Logic and Declarative Language* by Downward | |
| - *Proofs and Types* by Girard, Lafont and Taylor | |
| + relationship between inference proofs and type systems at a research level |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment