Skip to content

Instantly share code, notes, and snippets.

@kanak
Created March 17, 2011 03:24
Show Gist options
  • Save kanak/873776 to your computer and use it in GitHub Desktop.
Save kanak/873776 to your computer and use it in GitHub Desktop.
Discrete Math Using a Computer: Chapter 06 Propositional Logic notes and exercise solutions
#+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