Skip to content

Instantly share code, notes, and snippets.

@viecode09

viecode09/DiscreteMathComputer06.txt

Forked from kanak/DiscreteMathComputer06.txt
Created February 6, 2017 09:06
Show Gist options
  • Save viecode09/f130067f0fb072ef0d397af0329ba920 to your computer and use it in GitHub Desktop.
Save viecode09/f130067f0fb072ef0d397af0329ba920 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. @kanak kanak created this gist Mar 17, 2011.
    897 changes: 897 additions & 0 deletions DiscreteMathComputer06.txt
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,897 @@
    #+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