Math1090 Math 1090: Logic for Computer Science
                                    Jeff's Syllabus


Jeff, Readme, Course Info, Thoughts, Times, Dates, Course Description, Mental Health, Notes, EClass/Moodle, Zoom, Forum, Partner, Videos, Solutions

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 2n 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 = {❬x1,y1,x2,y2❭ | x1&x2∈U, y1=y1∃, y2=y2∃(x1)}
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 ∃Mw1∀Mb1∃Mw2∀Mb2... White-Wins(Mw1,Mb1,Mw2,Mb2,...)
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 α(t1,t2)       If [t1=t2], then [α(t1) iff α(t2)] and [f(t1)=f(t2)]
? 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 Axiomsfixed∪Γ, 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∃n0∀n≥n0 f(n) ≤ cg(n)
  Coding Phase vs Execution Phase Before input is choosen vs after
4   Table Look Up vs TM ∀k∃Mtable∀x,y≤k Mtable(x,y)=x×y   vs   ∃M∀x,y M(x,y)=x×y
26   Probabilistic Algorithms ∃M∀I PrR[M(I,R)≠P(I)] ≤ 2-|R|
6   Universal TM ∃ TM MU, ∀ TM M, ∀ input I, MU(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-Invt⟩ & ¬⟨Exit-Cond⟩ & ⟨Loop-Code⟩ ⇒ ⟨Loop-Invt+1
       - Ending ⟨Loop-Inv⟩ & ⟨Exit-Cond⟩ ⇒ ⟨Post-Cond⟩
       - Max in Array Maxi∈[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, ∀⟨w1...wd⟩, ∀v∈V, ∃⟨c1...cd⟩, v=c1w1+...+cdwd
  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, ∀⟨w1...wd⟩, ∀v∈V, ∃⟨c1...cd⟩, v=c1w1+...+cdwd
     - Linear Transformations A matrix times the vector ⟨c1...cd⟩ for one v gives the vector ⟨c'1...c'd⟩ for another v'
     - Change of Basis A matrix times the vector ⟨c1...cd⟩ given one basis ⟨w1...wd⟩ 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
  Defn of "Knowing" It is true in every universe that I consider possible
  

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.