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

Passion:
Often, I want to share my excitement about something like Angular Momentum and few people have interest.
They might want to share their excitement about astrology and I try to show interest.
I find it much easier to find people who want to teach then to find people who want to learn.
I always figure that I should have to pay my York students to listen to me - not the other way around.
But for wanting me to deal with you wanting a higher mark - for that the students need to pay.


Jeff, Readme, * Course Info *, Thoughts, Times, Dates, Course Description,
Mental Health, EClass, Zoom, Forum, Partner, Videos, Discord

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):
41   Administrative Details How the course will be run.
45   Summary of course Just a quick over view
  Overwhelming summery You can skip it.
34     - Math Has a Fatal Flaw Excellent Youtube video.
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):
2 3   Quick Examples Clue and Menu
11 23   Truth Tables And ∧, Or ∨, Not ¬, Implies →, if and only if iff, Exclusive-Or ⊕
  Meta-Notation Next line of proof ⇒, After many lines of proof ⊢, Impies ⊧
22 4 6   What This Logic Is and Is Not. It is not hope, beliefs, probability, time dependent, but just true or false.
11   Venn Diagrams ∧ relates to ∩; ∨ to ∪; → to ⊂
40   Arguing Our Rules/Lemmas: Lots of intuition
    - And vs Or Seperating vs Selection
    - Implies Modus Ponens, Contrapositive, & Transitivity
    - Deduction Assume α, prove β, conclude α→β.
    - Cases Two cases α & β. Case α, prove γ. Case β, prove γ. Conclude γ.
    - Distributive γ∧(α∨β) iff (γ∧α)∨(γ∧β) and γ∨(α∧β) iff (γ∨α)∧(γ∨β)
22     - Eval/Build If ¬α, then α → γ
6     - Simplify If ¬ β, then (γ → β iff ¬ γ)
18 3   Our Rules/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 ¬¬α iff α
    - Excluded Middle α∨¬α and ¬(α∧¬α). The universe must decide.
    - Commutative α∧β iff β∧α and α∨β iff β∨α
    - De Morgan's Law ¬(α∧β) iff ¬α∨¬β
    - Distributive γ∧(α∨β) iff (γ∧α)∨(γ∧β) and γ∨(α∧β) iff (γ∨α)∧(γ∨β)
19   Quick Proofs [(α ∨ β)→ γ] → [(α ∧ β)→ γ]
34   True iff Provable Sound & Complete
46 6 20 42   Example Proof Prove "A World with out Racism"
43 3 30 8   Axiom Schema "x nurse young" → "x are mammals"
12 9   Formal Proofs Each sentence in the Hilbert sequence follows from axioms or previous
15 15   Hard Example Brute for proof from both directions.
14 14   Tautologies via Tables Formula is true under every setting of the variables.
36 9   Tautologies vs Lemmas Proving Lemmas from Tautologies and visa versa.
11 18   Formulas vs Circuits Circuits reuse computations and Formulas (¬P∧Q)∨(R⊕S)→T do not.
  Proofs of Tautologies:
10 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 7     - Formal Proofs We will convert DP algorithm to a DP proof.
5   Review Example Adversarial Father
3     - Venn Diagrams basically proof by table
3     - Counter Example Model A model in which equivalence fails
12     - Deduction and Cases Standard proof techniques
2 3     - Duality Good vs Evil
.1     - And of Ors of Literals Conver to standard for
11     - Davis-Putnam Algorithm and Proof Technique by Example.
  Likely Skipped
62 62     - Davis Putnam Alg Heuristic that might be fast
9 9     - Evaluate/Build With α=T, α∨γ evaluates to T. From α, conclude α∨γ.
5 12     - Simplify With α=T, α∧γ simplifies to γ.
    - Davis-Putnam Axioms
        - Deduction Assume α, prove β, conclude α→β
        - Evaluate/Building From α, α', ¬β, and ¬β', conclude α∧α', ¬(β∧γ), ¬(γ∧β), α∨γ, γ,∨α ¬(β∨β'), γ→α, β→γ, ¬(α→β), and ¬¬α.
        - Cases From α→Φ, and ¬α→Φ, conclude Φ
40 40     - Davis-Putnam Proof Mirrors a Davis-Putnam computation to ensures proof system is Complete.
20     - Long Davis-Putnam Proofs A random And of Or's required an exponential size DP proof, as does the Or of parity.
    - Horn Clauses A solution can be found faster
Predicate Logic - Informal Understanding & Proofs (ppt):
26 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 Parent(x,y) ∧ Femaley)]
5 5   Order of Quantifiers ∀x∃yP(x,y)   vs   ∃y∀xP(x,y)
80 80   Sets of Tuples α is true for each tuple in S = {❬x1,y1,x2,y2❭ | x1&x2∈U, y1=y1∃, y2=y2∃(x1)}
14 14   Free and Bound Variables: α(x)∧∀xβ(x)
    - Bound Variables Local to a quantifier ∀ or ∃.
    - Free Variables Values supplied by boss
14 14   Sentence Validity (Truth) An Infinite Iterative Algorithm
9 9   Skolem/Auxiliary Functions ∀x∃yP(x,y) ⇒ P(x,y(x))
17 17   Negations ¬∃xP(x) ≡ ∀x¬P(x)
6 6   Understanding from the Inside ∀x [∃y+y=0] ≡ ∀x Property(x)
9 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 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 15     - Game Tree ∃Mw1∀Mb1∃Mw2∀Mb2... White-Wins(Mw1,Mb1,Mw2,Mb2,...)
5     - Solution to Hard Problem ∃ solution y HardProblem(y) & ∀ potential counter examples x ¬HardProblem(x)
21 21     - Reals ∃a∀x∃y x=a ∨ x×y=1
  Oracles:
30 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).
30 67 12     - Proof Game with Oracle Various examples with Oracle, Prover, and Adversary
13 13     - Humans are Mortal "All humans are mortal" and "Socrates is human" hence "Socrates is mortal"
26 26     - Diagonal to remove
35 35     - Function f(x) to remove
34 34     - Free Variable Fail α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true
26 26 9     - Distributive Laws Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)]   and    ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
16 16 23     - Order of Quantifiers ∃y∀xP(x,y) ⇒ ∀x∃yP(x,y)
40 67   Computing: ∃ Alg A, ∀ Inputs I, A(I)=P(I)
40 39 57 7     - Coding vs Execution Phase ∃ Alg A, ∃ # k, ∀ Inputs I, ∃ time t, A(I)=P(I) & Lines(A,I)=k & Time(A,I)=t
40 27 58     - Compiling Java to TM ∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I)
Formal Proofs (ppt):
  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!
15 9 4 9   Our Formal Proof System Hilbert, Lemmas, Deduction, Adding/Removing Quantifiers
    - 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(φ').
    - Quantifier Rules: 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)
9 9     - Deduction Assume α(x'), prove β(x'), conclude α(x)→β(x)
15   Formal vs Informal: Breaking proof into three parts
17 17     - Adding ∀ & ∃ Relates to Adversary Game and to Prover Game
20 20     - Removing ∀ & ∃ Relates to Oracle Game
10   True iff Provable Sound & Complete
  Examples of Proofs:
20 95     - Order of Quantifiers ∃y∀xP(x,y) → ∀x∃yP(x,y)
10 10     - Distributive Laws Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)]   and    ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
9 9     - Proof by Cases From α∨β, α→γ, and β→γ, prove γ
20 68     - Proof by Duality Switch true/false, ∧/∨, ∀/∃, →/←
20     - Free Variable Fail α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true
42 42   Proving x+1>x Non-Logical Axioms Γ (e.g., to do number theory)
12 12   Gödel Completeness and Incompleteness
34   Math Has a Fatal Flaw Excellent Youtube video.
  Proving Gödel's Completeness Using Sequent Calculus
15   Sequent Calculus Tree of Sequents α1∧...∧αn → β1∨...∨βm
  More Details:
    - Definitions Again
14     - Lemmas via Substitutions: 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)]
    - Soundness of Our Pr. System
    - Soundness of Sequent Calculus
Syntax (ppt): Which strings are grammatically correct formulas?
20 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
Induction (ppt): [S(0)&∀i[S(i-1)→S(i)]] → ∀iS(i)
90 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)
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 54   Time Complexity ∃M∃c∀I M(I)=P(I) and Time(M,I)≤ |I|c
44 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 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 26   Probabilistic Algorithms ∃M∀I PrR[M(I,R)≠P(I)] ≤ 2-|R|
6 6   Universal TM ∃ TM MU, ∀ TM M, ∀ input I, MU(M,I) = M(I)
64 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 12   Computing vs Accepting Halt(M,I,t) is computable   and   Halt(M,I) ≡ ∃t Halt(M,I,t) is not
1 1   Poly vs NP Sat(C,I) is in poly   and  Sat(C) ≡ ∃I Sat(C,I) is likely not
30 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 24   Uncomputable Problems ∃P ∀M ∃I M(I)≠P(I)
10   Halting & MathTruth Knowing whether a TM M halts or a first order sentence α is valid
are both uncomputable.
20 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.
  Proving Gödel's Completeness Using Sequent Calculus
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
  

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.