ECS 20 — Lecture 4 — Fall 2013 —8 Oct 2013
Phil Rogaway
o Quiz 1
o More logic
– Finish propositional calculus: Formal proofs, and some without-proof theorems
– First-order logic (adding quantifiers) (didn’t get to this)
Propositional Logic “Propositional Logic” = “Sentential Logic” = “Sentential Calculus”
Review: WFFs truth tables
truth assignments logical completeness DNF
satisfiability tautology ⊨
is logically equivalent
A formula is satisfiable if some t.a. makes it true.
A set of formula is satisfiable if some t.a. makes them all true.
A formula of propositional logic is tautological (or valid) if it is true for every t.a. ⊨ (It is satisfiable if it is true under some t.a.)
Formulas and are logically equivalent , written , if a tautology.
Prop: There is an algorithm (=a precisely-describable procedure, mechanism, recipe) that, given a WFF of sentential logic, decides
– if it is a tautology.
– if it is a satisfiable.
– if it equivalent to some given, second formula. f |= =| g
Some simple tautologies Velleman, List from How to Prove It, p. 21, 23, 47, 49 . You can check any of these with a truth table.
Today:
Associative: P (Q R) (P Q) R P (Q R) (P Q) R
DeMorgan’s: (P Q) P Q (P Q) P Q
Idempotent: P and P P P P P
Contradiction P Q P Q P Q (P Q)
Formal Proofs
//Mention the similarities to arithmetic //laws with corresponding to addition //and corresponding to multiplication
1
Discuss conventional proofs vs. formal proofs.
I now discuss formal proofs, although what mathematicians – and you – will mostly be producing conventional (informal) ones.
Following from Wikipedia, Propositional Calculus. Following 14 rules
Axiom List W
Name
THEN-1 THEN-2
AND-1 AND-2 AND-3
OR-1
OR-2
OR-3 NOT-1
NOT-2
NOT-3
IFF-1 IFF-2
IFF-3
One of the reasons to have a list of axioms like the list just given is to develop a notion of “what is provable”” We will write X ⊢Y if statement Y follows from X. Read: Y is provable from X. Turnstyle is the name of the symbol.
Formal proofs are quite different from conventional proofs, but a thesis in mathematics is that conventional proofs can be recast as formal ones. What are formal proof? They are syntactic objects in some formalized system. There are many choices one has in how to do the formulation,
Axioms
Axiom Schema
Description
Add hypothesis , implication introduction
Distribute hypothesis over implication
Eliminate conjunction
Introduce conjunction
Introduce disjunction
Eliminate disjunction
Introduce negation
Eliminate negation
Excluded middle, classical logic
Eliminate equivalence
Introduce equivalence
2
but here is what we would typically have: that a formal proof is a sequence of formula: 1, …, n where each i is either
1. an assumption or
2. an axiom (it appear on a list like Axiom List W) or
3. it follows from a previous set of lines in the proof by one of a number of enumerated rules –
indeed we can make do with one rule, modes ponens,
i) (A B)
… j) A
…
k) B modes ponens
if 1, …, n are the assumptions used in a proof and is a statement in the proof then we write 1, …, n ⊢ to indicate that can be proven from 1, …, n
Definition: if { 1, …, n } ⊢ then ( 1, …, n )⊢
Example:
⊢ (PQ)(P R S)(SQ T) T
1. PQ
2. PRS 3. SQ T 4. P
5. Q
6. P R
7. S
8. SQ
9. T
assumption
assumption
assumption
“conjunction elimination” (P Q P) applied to (1) “conjunction elimination” (P Q Q) applied to (1) “disjunction introduction” (P R S) applied to (5)
modus ponens (AB A gives B) applied to (2) and (6) “conjunction introduction” (S, Q SQ) applied to (7) and (5) modus ponens applied to (3) and (8)
therefore
{PQ, PRS, SQT} ⊢ T //Thegivenstatementisprovable
⊢can derive (prove) (from the — no assumptions) ⊢ can derive from
Some theorem and terms: Completeness, Soundness, and Compactness of Predicate Calculus
SOUNDNESS: ⊢ ⊨ COMPLETENESS ⊨ ⊢
COMPACTNESS: Let be a set of WFFs.
Suppose that every finite subset of is satisfiable.
3
Then is satisfiable.
(contrapositive:
Let be a set of WFFs.
If is unsatisfiable then some finite subset of is too)
Don’t prove — want to use this in a computer-science example.
Application: TILING (Dominos)
Can you tile the with tiles of specified types (adjacent edges of the same color)
Eg:
Make an example where the plane is and is not tileable. Indicate that, in ecs120, common to prove that the TILING decision question is undecidable. But not our interest here. We are interested in whether the tileability of the plane for a given set of tile types is FALSIFIABLE — is there a proof of untileability? There will be if the following is true:
If the plane is untellable, it is already untileable on some finite subset of the plane.
Not an obvious claim — a priori possible that plane is untileable even though every finite rectangle of it is tileable.
To prove from compactness: Introduce a variable
P[i,j,k]: there is a tile of type k at position (i, j )
Write a boolean formula to capture
– One and only one tile per cell: P[i,j,k] not P[i,j,k’] for all i,j and all k k’.
– Adjoining tiles are of compatible types. P[i,j,k] (k’P[i+1,j,k’] for all i, j, if a tile of type k’ can
be put atop a tile of type k; and so on (three more sets of rules)
Now: connect it to compactness theorem. The set is all the formulas above. If it is unsatisfiable, then some finite subset of is unsatisfiable. Let n be the largest index used by a variable in . Then the [-n..n] [-n..n] subset of the plane is already untileable.
Gamma is satisfiable iff every the plane can be tiled with tiles of the given types.
In the language you will learn in ecs120, TILING is co-RE 4
5