09.04 Lesson Plan: Proof Systems

Elements of propositional logic
- propositional symbols
- logical connectives: and, or, implies, biconditional, not
	defined by truth tables

truth table for AND.

what is the truth table for IMPLIES?

world == a *complete* truth assignment to the propositions

we write:

m |= S       S evaluates to TRUE in m == m is a MODEL of S

	Note the perverseness of logicians.  It would make more sense
 	to say S is a model of m!

H |= C       all models of H are also models of C == H ENTAILS C

if H|=C and C|=H, we say that H and C are EQUIVALENT == have the same set of models
	H == C

if S is true in SOME worlds, we say it is SATISFIABLE.
	--> MODEL FINDING is the task of actually computing such a model for a sentence.

if S is true in ALL worlds, we say it is VALID.

P v ~P is VALID.

What about:

(~(P => Q)) => P   ?

Check validity by going through set of truth assignments to P and Q.

DEDUCTION THEOREM:

H |= C     iff          (H => C) is valid

Go over PROOF OF DEDUCTION THEOREM:

Suppose (H=>C) is valid.  Then in *every* world, either ~H is true or C is true (or both).
If we consider only those worlds where H is true, then C must be true.
Therefore H |= C.

Suppose H|=C.  Consider any world where H is true.  Then C must be true in this
world.  So (H=>C) is true.  Now consider any world where H is false.  By the truth
table, (H=>C) is true.  Therefore (H=>C) is true in all worlds, so it is valid.

REDUCTIO ABSURDUM:

H|=C      iff    (H & ~C) is unsatisfiable

PROOF:  Compare the truth table for (H=>C) and the one for (H&~C).

In fact:   if we like we can DEFINE  (H=>C)   AS   (~H v C).  The => connective is
redundant.

Can we also define away the & connective?

Can we define the truth table for a SINGLE connective that lets us define ALL the
other connectives?

--------

SO FAR: we have reasoned by list sets of models and truth tables.  But we can also
reason just by MANIPULATING SENTENCES.   This is called PROOF THEORY.

A PROOF SYSTEM == set of rules for manipulating sentences
     H  |-  C

Define SOUNDNESS

Define COMPLETENESS

For propositional logic, there are many possible proof systems.

Natural deduction:

Modus Ponens
The nine primitive rules of system L are

   1. The Rule of Assumption (A)
   2. Modus Ponendo Ponens (MPP)
   3. The Rule of Double Negation (DN)
   4. The Rule of Conditional Proof (CP)
   5. The Rule of -introduction (I)
   6. The Rule of -elimination (E)
   7. The Rule of -introduction (I)
   8. The Rule of -elimination (E)
   9. Reductio Ad Absurdum (RAA)

RESOLUTION

- SOUNDNESS
- REFUTATION COMPLETENESS

Example 7.2:  Compare semantic to proof theoretic reasoning