Topics:
Introduction
Propositional Logic
Informal Understanding & Proofs
Syntax,
Semantics,
Sound & Complete
Formal Proofs
Examples:
Computing
Complexity
Induction
Representing Numbers
Non Constructive Proofs
Vector Spaces
Information Theory Example
Introduction (ppt): | ||
53 | Administrative Details | How the course will be run. |
18 | Abstract Thinking | Layers of understanding |
9 11 | History of Proofs | Euclid, Hilbert, Gödel, Turing |
21 | Propositional Logic | And, Or, and Implication between true/false statements |
Predicate Logic: Informal | ∀ boys ∃ girl Loves(boy,girl) | |
8 | Proof is a Game | The prover provides for ∃x & the adversary provides for ∀y |
15 | Order of Operations | ∀x∃yP(x,y) vs ∃y∀xP(x,y) |
12 | Understanding from the Inside | ∀ boys ∃ girl Loves(boy,girl) says something about the set of boys. |
3 | Formula Validity | ∀ is a big And and ∃ is a big Or. |
4 7 | Syntax & Semantics | Which strings of characters are well formed formulas and what do they mean? |
Formal Proofs | Mechanical steps to prove that a given formula is valid | |
35 | Models/Universes | The set of objects and how functions and relations are interpreted. |
40 | Formal Proof Systems | A set of axioms and a set of rules |
Sound & Complete | Proofs should only prove valid formulas and each valid formula should have a proof | |
Applications | We will cover much of Computer Science Theory | |
Propositional Logic (ppt): CLO 1 | ||
6 | What This Logic Is and Is Not. | It is not hope, beliefs, probability, time dependent, but just true or false. |
2 | Quick Examples | Clue and Menu |
14 | Proof Techniques/Lemmas: | Lots of useful things |
- Modus Ponens | From α and α→β, conclude β. | |
- Deduction | Assume α, prove β, conclude α→β. | |
- Equivalence | From α→β and β→α, conclude (α iff β). | |
- Contrapositive | ¬β→¬α iff ¬(α∧¬β) iff α→β. | |
- Transitivity | From α→β and β→γ, conclude α→γ. | |
- Proof by Cases | From α∨β, α→γ, and β→γ, conclude γ. | |
- Proof by Contradiction | From ¬α→β and ¬α→¬β, conclude α. | |
- Inconsistent | From β and ¬β, conclude anything. | |
- Separating And | From α∧β, conclude α and β. | |
- Selecting Or | From α∨β and ¬α, conclude β. | |
- Evaluate/Build | From α, α', and ¬β, conclude α∧α', ¬(β∧γ), α∨γ, γ→α, β→γ, ... | |
- Double Negation | From ¬¬α, conclude α | |
- Excluded Middle | α∨¬α and ¬(α∧¬α). The universe must decide. | |
- Commutative | α∧β iff β∧α and α∨β iff β∨α | |
- De Morgan's Law | ¬(α∧β) iff ¬α∨¬β | |
- Distributive | γ∧(α∨β) iff (γ∧α)∨(γ∧β) and γ∨(α∧β) iff (γ∨α)∧(γ∨β) | |
3 42 | Example Proof | Prove "A World with out Racism" |
30 8 | Axiom Schema | "x nurse young" → "x are mammals" |
9 | Formal Proofs | Each sentence in the Hilbert sequence follows from axioms or previous |
15 | Hard Example | Brute for proof from both directions. |
9 | Tautologies vs Lemmas | Proving Lemmas from Tautologies and visa versa. |
23 | Operator's Truth Tables | And ∧, Or ∨, Not ¬, Implies →, iff, Exclusive-Or ⊕ |
9 | Evaluate/Build | With α=T, α∨γ evaluates to T. From α, conclude α∨γ. |
12 | Simplify | With α=T, α∧γ simplifies to γ. |
14 | Tautologies | Formula is true under every setting of the variables. |
11 | Propositional Formulas vs Circuits | Circuits reuse computations and Formulas (¬P∧Q)∨(R⊕S)→T do not. |
Proofs of Tautologies: CLO 2 | ||
8 | - Exponential sized truth tables | Determine true/false for each of the 2^{n} setting of the variables |
- NP & Co-NP | There are not likely smaller proofs witnessing that a formula is satisfiable or a tautology | |
7 | - Formal Proofs | We will convert DP algorithm to a DP proof. |
62 | - Davis Putnam Alg | Heuristic that might be fast |
40 | - Davis-Putnam Axioms | |
- Deduction | Assume α, prove β, conclude α→β | |
- Evaluate/Building | From α, α', ¬β, and ¬β', conclude α∧α', ¬(β∧γ), ¬(γ∧β), α∨γ, γ,∨α ¬(β∨β'), γ→α, β→γ, ¬(α→β), and ¬¬α. | |
- Merge | From α→Φ, and ¬α→Φ, conclude Φ | |
- Davis-Putnam Proof CLO 5 | Mirrors a Davis-Putnam computation to ensures proof system is Complete. | |
Horn Clauses | A solution can be found faster | |
Predicate Logic - Informal Understanding & Proofs (ppt): | ||
26 | Intro to Quantifiers | ∀x ≡ for All x and ∃x ≡ there Exists a y |
- Understand as as a Game | Boss gives free values, prover ∃x, adversary ∀y, and oracle answers to queries | |
- Hugely Expressive | Helps you understand and prove mathematical statements | |
- So wrong | ∀inputs x, ∃program J, J(x)=P(x) | |
15 | Objects, Predicates, & Relations | ∀x,y [daughter(y,x) iff father(x,y) ∧ girl(y)] |
5 | Order of Quantifiers | ∀x∃yP(x,y) vs ∃y∀xP(x,y) |
80 | Sets of Tuples: | α is true for each tuple in S = {❬x_{1},y_{1},x_{2},y_{2}❭ | x_{1}&x_{2}∈U, y_{1}=y_{1∃}, y_{2}=y_{2∃}(x_{1})} |
14 | Free and Bound Variables: | α(x)∧∀xβ(x) |
- Free Variables | Values supplied by boss | |
14 | Sentence Truth | An Infinite Iterative Algorithm |
9 | Skolem/Auxiliary Functions | ∀x∃yP(x,y) ⇒ P(x,y_{∃}(x)) |
17 | Negations | ¬∃xP(x) ≡ ∀x¬P(x) |
6 | Understanding from the Inside | ∀x [∃y+y=0] ≡ ∀x Property(x) |
9 | Constructive & Contradiction | I don't like proofs of ∀x P(x) that assume the contradiction so that it can construct an x. |
Instead, say "Let x be an arbitrary object." | ||
14 | The Proof Viewed as a Game: | Boss gives values to free variables. |
Oracle assures you of A when proving A→B. | ||
Prover works to prove by providing good ∃x objects. | ||
Adversary works to disprove by providing worst case ∀y objects. | ||
15 | - Game Tree | ∃M^{w}_{1}∀M^{b}_{1}∃M^{w}_{2}∀M^{b}_{2}... White-Wins(M^{w}_{1},M^{b}_{1},M^{w}_{2},M^{b}_{2},...) |
21 | - Reals | ∃a∀x∃y x=a ∨ x×y=1 |
Oracles: | ||
19 41 | - Help from an Oracle | Assume ∀x ∃y P(x,y). You give oracle x and she gives you y for which P(x,y). |
67 12 | - Proof Game with Oracle | Various examples with Oracle, Prover, and Adversary |
13 | - Humans are Mortal | "All humans are mortal" and "Socrates is human" hence "Socrates is mortal" |
26 | - Diagonal Solutions | to remove |
35 | - f(x) Solution | to remove |
34 | - Free Variable Fail | α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true |
26 9 | - Distributive Laws | Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)] and ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)] |
16 23 | - Order of Quantifiers | ∃y∀xP(x,y) ⇒ ∀x∃yP(x,y) |
67 | Computing: | ∃ Alg A, ∀ Inputs I, A(I)=P(I) |
39 57 7 | - Coding Phase vs Execution Phase | ∃ Alg A, ∃ # k, ∀ Inputs I, ∃ time t, A(I)=P(I) & Lines(A,I)=k & Time(A,I)=t |
27 58 | - Compiling Java to TM | ∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I) |
Formal Proofs (ppt): CLO 3 | ||
Formal Proof Systems | Really trimmed down proof system from which you can prove everything! | |
Intuitive and robust proof system from which proving things is easy! | ||
9 | Our Formal Proof System Quick | Hilbert, Lemmas, Deduction, Adding/Removing Quantifiers |
42 | Game and Γ Example | Comparing Informal and Formal Proofs |
Non-Logical Axioms Γ (e.g., to do number theory) | ||
12 | Gödel | Completeness and Incompleteness |
4 | Our Formal Proof System: | |
- Quantifier Closure | If φ is a line in our proof, then its meaning is QC(φ) ≡ ∀M∃y_{∃}∀x∀x' [α(x')→φ]. | |
Given rule "From line φ, include line φ' ", we write QC(φ)⊧QC(φ') and prove QC(φ)→QC(φ'). | ||
14 | - Lemmas via Substitutions: CLO 7 | Add all propositional tautologies as axioms. |
- Modus Ponens | If α and α→β then β | |
- True/False | If Φ(P,Q), then Φ(α,β) If [α iff β], then [Φ(α) iff Φ(β)] | |
- Objects | If α(x,y), then α(t_{1},t_{2}) If [t_{1}=t_{2}], then [α(t_{1}) iff α(t_{2})] and [f(t_{1})=f(t_{2})] | |
? 9 | - Deduction | Assume α(x'), prove β(x'), conclude α(x)→β(x) |
9 | - Quantifier Rules: CLO 6 | If φ is a line of your proof, then you can include φ as a line as well. (We don't say follows from) |
- Removing ∃ | From ∃y α(x,y), include α(x,y_{∃}(x)) | |
- Adding ∃ | From α(term), include ∃y α(y) unless term depends on an x bound with ∀x | |
- Removing ∀ | From ∀x α(x), include α(x) | |
- Adding ∀ | From α(x), include ∀x α(x) unless fixed x_{∃} or x' | |
- Negations | ¬∃α(x) iff ∀x¬α(x) | |
Formal vs Informal: | ||
17 | - Adding ∀ & ∃ | Relates to Adversary Game and to Prover Game |
20 | - Removing ∀ & ∃ | Relates to Oracle Game |
Examples of Proofs: | ||
95 | - Order of Quantifiers | ∃y∀xP(x,y) → ∀x∃yP(x,y) |
10 | - Distributive Laws | Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)] and ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)] |
9 | - Proof by Cases | From α∨β, α→γ, and β→γ, prove γ |
68 | - Proof by Duality | Switch true/false, ∧/∨, ∀/∃, →/← |
- Free Variable Fail | α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true | |
Proving Sound | For each rule "From line φ, include line φ' " prove | |
Sequent Calculus LK: CLO 4 | Tree of Sequents α_{1}∧...∧α_{n} → β_{1}∨...∨β_{m} | |
- Prove each its Rules | Left and Right rule for ∧, ∨, ¬ ∃, and ∀ | |
Syntax (ppt): | Which strings are grammatically correct formulas? | |
4 | Context Free Grammar of Syntax | S ⇒ ∀xS | ∃xS | ¬S | S∧S | S∨S | R(T,T) |
Meta Syntax | α(x) is not itself a first order logic sentence, but denotes one | |
Closure of Syntax | If α(x) is a sentence then so is ∀xα(x) | |
Parsing of Syntax | Matching {[]()} using a stack | |
Semantics (ppt): | ||
6 | Meaning?: | What does formula α mean? |
- Human | ∀x∃y x+y=0 ≡ "Integers are closed under negation" | |
-The Model/Universe M | Defines the universe of objects, the functions and relations (but not free variables) | |
- Sentences Truth | Infinite recursive algorithm looping over all models and objects | |
- Informal Proof | Strategy for the ∀ ∃ game | |
- Formal Proof | Each sentence in the Hilbert sequence follows from the previous | |
Free and Bound Variables | α(x)∧∀xβ(x) | |
Deduction Variables x' | Assume α(x'), prove β(x'), conclude α(x)→β(x) | |
Quantifier Closure: | For a Hilbert style proof, we need each line standing alone to state something valid. | |
If φ is a line in our proof, then its meaning is QC(φ) ≡ ∀M∃y_{∃}∀x∀x' [α(x')→φ] | ||
- Skolem/Auxiliary Functions | QC(α(x,y_{∃}(x))) ≡ ∀α∃y_{∃}∀x α(x,y_{∃}(x)) | |
- Deduction | QC( β(x')) ≡ ∀β∃y_{∃}∀x∀x' [α(x')→β(x')] | |
Sound & Complete (ppt): | ||
19 | Quantifier Closure | Φ ≡ QC(φ) ≡ ∀M∃y_{∃}∀x∀x' [α(x')→φ] |
Truth/Valid: | ||
- M[a]⊧Φ | Formula Φ is true under variable assignment a in universe/model M. | |
- ⊧Φ | Φ is Valid, ie Φ is true under every model/ass M[a]. | |
- Γ⊧Φ | Φ is a Logical Consequence of Γ, ie Γ→Φ is valid, | |
ie Φ is true under every model/ass M[a] under which Γ is true. | ||
Proofs: | ||
- Γ⊢Φ | Φ is a Theorem or Syntactic Consequence of Γ, ie from formulas in Axioms_{fixed}∪Γ, one can prove Φ. | |
- (Φ_{i-2}∧Φ_{i-1}) ⇒Φ_{i} | If φ_{i-2} and φ_{i-1} are lines in your proof, then you can add φ_{i}, ie (Φ_{i-2}∧Φ_{i-1}) →Φ_{i} can be proved. | |
Interchangeable? | ⊧, ⊢, ⇒, and → are interchangeable when interpreted with QC. | |
Be Careful. α(x)⇒∀x α(x) even though α(x)→∀x α(x) is not true. | ||
Sound: | A Proof System is Sound if a proof of φ from Γ ensures that Φ is valid when Γ is valid. | |
- Traditionally | Γ⊧φ ensures Γ⊢φ | |
- Our proof system | Γ⊧φ ensures Γ⊢QC(φ) | |
- Rule Requires | Rule "If φ_{i-2} and φ_{i-1} are line in your proof, then you can add φ_{i}" | |
requires "If QC(φ)_{i-2} and QC(φ)_{i-1} are valid, then so is QC(φ)_{i}", | ||
ie "Φ_{i-2}∧Φ_{i-1}⇒Φ_{i}", requires "Φ_{i-2}∧Φ_{i-1}→Φ_{i}". | ||
Complete | A Proof system is Complete if Φ being valid ensures that it has a proof. i.e. Γ⊢Φ ensures Γ⊧Φ | |
EXAMPLES | ||
Computing (ppt): More slides | Computational problems, machines, and inputs | |
See above in Informal Section: | ∃ Alg A, ∀ Inputs I, A(I)=P(I) | |
- Coding Phase vs Execution Phase | ∃ Alg A, ∃ # k, ∀ Inputs I, ∃ time t, A(I)=P(I) & Lines(A,I)=k & Time(A,I)=t | |
- Compiling Java to TM | ∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I) | |
Computable vs Uncomputable | ∃M∀I M(I)=P(I) vs ∃P∀M∃I M(I)≠P(I) | |
54 | Time Complexity | ∃M∃c∀I M(I)=P(I) and Time(M,I)≤ |I|^{c} |
44 | Classifying Functions | f(n)∈O(g(n)) ≡ ∃c∃n_{0}∀n≥n_{0} f(n) ≤ cg(n) |
Coding Phase vs Execution Phase | Before input is choosen vs after | |
4 | Table Look Up vs TM | ∀k∃M_{table}∀x,y≤k M_{table}(x,y)=x×y vs ∃M∀x,y M(x,y)=x×y |
26 | Probabilistic Algorithms | ∃M∀I Pr_{R}[M(I,R)≠P(I)] ≤ 2^{-|R|} |
6 | Universal TM | ∃ TM M_{U}, ∀ TM M, ∀ input I, M_{U}(M,I) = M(I) |
64 | Hugely Expressive | There is a first order logic sentence Compute(J,I,y) |
that states computer program J on input I outputs y. | ||
Complexity (ppt): | Classifying Computational Problems, NP, & Computable | |
12 | Computing vs Accepting | Halt(M,I,t) is computable and Halt(M,I) ≡ ∃t Halt(M,I,t) is not |
1 | Poly vs NP | Sat(C,I) is in poly and Sat(C) ≡ ∃I Sat(C,I) is likely not |
56 50 | NP | Clause-Sat(I) ≡ ∃S ∀C ∃x "Assignment S satisfies variable x in clause C" |
Reductions | [∀I [Sat(I) iff P(InstanceMap(I))]] ⇒ [Sat≤P] | |
24 | Uncomputable Problems | ∃P ∀M ∃I M(I)≠P(I) |
Halting & MathTruth | Knowing whether a TM M halts or a first order sentence α is valid | |
are both uncomputable. | ||
7 | Gödel's Incompleteness | No formal proof system is capable of proving all valid |
and no invalid formulas about the integer. | ||
To guarantee a proof, α needs to also be true in every nonstandard model. | ||
Induction (ppt): | [S(0)&∀i[S(i-1)→S(i)]] → ∀iS(i) | |
90 | Counting | Though we never reach all integers i, each i is eventually reached. |
Understanding Induction | Though we never prove S(i) for all i, for each i, S(i) eventually is proved. | |
- Sums | ∑_{i=1..n} i = ½ n(n+1) | |
- Special | Prove that every positive integer is special. | |
- Proof of Soundness | Having is a proof of φ ensures that φ is valid. | |
Loop Invariants: | S(i) ≡ "My algorithm maintains its loop invariants for the first i iterations." | |
- Establishing | ⟨Pre-Cond⟩ & ⟨Pre-Code⟩ ⇒ ⟨Loop-Inv⟩ | |
- Maintaining | ⟨Loop-Inv_{t}⟩ & ¬⟨Exit-Cond⟩ & ⟨Loop-Code⟩ ⇒ ⟨Loop-Inv_{t+1}⟩ | |
- Ending | ⟨Loop-Inv⟩ & ⟨Exit-Cond⟩ ⇒ ⟨Post-Cond⟩ | |
- Max in Array | Max_{i∈[1..n] A[i] } | |
- Differential Equations | Acceleration(t) = - Distance(i) | |
- Konig's Lemma | Infinite trees either have a node with infinite degree or an infinite path. | |
Recursion: | S(i) ≡ "My algorithm gives the correct answer on every input of size at most i." | |
- Friends | Trust friends to solve any smaller instances meeting the pre-conditions | |
- Merge Sort | Friends sort first and second halves and then I merge these solutions together. | |
- Planar Graph | For every planar graph, #Edges = #Nodes + #Faces - #Components - 1 | |
Every planar graph can be bichromatically coloured with 6 colours. | ||
- Strong Induction | [∀i [(∀j<i S(j))→S(i)]] → ∀iS(i) | |
Representing Numbers (ppt): | ||
Calculus Epsilon/Delta Proofs | ∀x∀ε∃δ∀x'∈[x+δ,x-δ] f(x')∈[f(x)-ε,f(x)+ε] | |
Vector Spaces | ∀V, ∀⟨w_{1}...w_{d}⟩, ∀v∈V, ∃⟨c_{1}...c_{d}⟩, v=c_{1}w_{1}+...+c_{d}w_{d} | |
Graphs | ∀u∃v[Edge(u,v) & ∀v'≠v ¬Edge(u,v')] | |
Induction | [S(0)&∀i[S(i)→S(i+1)] → ∀iS(i) | |
Fields: | ||
- Rules | ∃1∀x x×1=x ∀x∃y x×y=1 | |
- Constructing Integers | ∀x∃y y=x+1 | |
- Finite Fields | ∀x∃y y=x+1 but 4+1=0 | |
- Integers mod p | ∀primes p ∀x∃y x×y=1 (mod p) | |
- Proofs for Integers | Integers ⇒ axioms ⇒ prove great facts | |
Finite, Countable, and Uncountable | There are more reals than integers. S is countable iff ∃List, ∀x∈S, ∃i∈N, List(i) = x. | |
Non Constructive Proofs (pdf pg 23): | ||
Expander Graphs | The probability that it exists is greater than zero. | |
An infinite number of primes | ∀n∃prime p>n (It divides into n!+1) | |
Vector Spaces (ppt): | ||
- Spanning the Space | ∀V, ∀⟨w_{1}...w_{d}⟩, ∀v∈V, ∃⟨c_{1}...c_{d}⟩, v=c_{1}w_{1}+...+c_{d}w_{d} | |
- Linear Transformations | A matrix times the vector ⟨c_{1}...c_{d}⟩ for one v gives the vector ⟨c'_{1}...c'_{d}⟩ for another v' | |
- Change of Basis | A matrix times the vector ⟨c_{1}...c_{d}⟩ given one basis ⟨w_{1}...w_{d}⟩ gives | |
the ⟨c'_{1}...c'_{d}⟩ for another ⟨w'_{1}...w'_{d}⟩ | ||
One proof & many applications: | ||
- Colour | Red/Blue/Green forms a basis for humans, but in science light is infinitely dimensional | |
- Error Correcting Codes | Encoding is a linear transformation from the message to the code vectors | |
- Fourier Transformation | A change from the sine basis to the time basis | |
- Integer Multiplication | A change from the polynomial basis to the evaluation basis | |
- JPEG Image Compression | A change from the pixel basis to the sine basis | |
- Dim Reduce & Face Recog | A change from xy basis to rotated basis | |
- Calculus | Integrating is the inverse linear transformation of differentiating | |
- Probabilistic Markov Process | Each time step is a linear transformation of the probability vector | |
- Quantum Probability | Each time step is a different linear transformation of the probability vector | |
Information Theory Example (ppt): | ||
Knowing Mud Problem | I know that my mom knows that my dad know that I am good. | |
Common Knowledge | Everybody knows that everybody knows that everybody knows | |
Def^{n} of "Knowing" | It is true in every universe that I consider possible | |
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.