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
Formal Proofs
Syntax & Semantics,
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.
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)
  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)
45 87 11 80   Sets of Tuples α is true for each tuple in S = {❬x1,y1,x2,y2❭ | x1&x2∈U, y1=y1∃, y2=y2∃(x1)}
9 14   Free and Bound Variables: α(x)∧∀xβ(x)
    - Bound Variables Local to a quantifier ∀ or ∃.
    - Free Variables Values supplied by boss
10 14   Sentence Validity (Truth) An Infinite Iterative Algorithm
4 9   Skolem/Auxiliary Functions ∀x∃yP(x,y) ⇒ P(x,y(x))
41 17   Negations ¬∃xP(x) ≡ ∀x¬P(x)
10 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."
12 10 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.
19 15     - Game Tree ∃Mw1∀Mb1∃Mw2∀Mb2... White-Wins(Mw1,Mb1,Mw2,Mb2,...)
4     - Solution to Hard Problem ∃ solution y HardProblem(y) & ∀ potential counter examples x ¬HardProblem(x)
38 21     - Reals ∃a∀x∃y x=a ∨ x×y=1
  Oracles:
19 6 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).
20 67 12     - Proof Game with Oracle Various examples with Oracle, Prover, and Adversary
33 16 23     - Order of Quantifiers ∃y∀xP(x,y) → ∀x∃yP(x,y)
16     - Follow the Parse Tree Determines the order of playing the game.
17 13     - Humans are Mortal "All humans are mortal" and "Socrates is human" hence "Socrates is mortal"
27 26     - Diagonal ∃y∀xα(x,y) → ∃yα(x,y)
27 59 35 35     - Function f(x) ∀yα(y) → ∀xα(f(x))
60 26 9     - Distributive Laws Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)]   and    ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
8     - Finding vs Verifing Model For proving a statement is not valid.
  Tutorials
47     - Euclidian Geometry ∀ pairs of points ∃ line
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!
28 9 4 9 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')→φ].
Our rules are of the form "From line φ, include line φ' ".
     We don't say follows from because φ→φ' might not be true.
     What must be true is QC(φ)→QC(φ').
    - Quantifier Rules:
        - 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)
    - Deduction Assume α(x'), prove β(x'), conclude α(x)→β(x)
15 17 20   Formal vs Informal:
    - Adding ∀ & ∃ Relates to Adversary Game and to Prover Game
    - Removing ∀ & ∃ Relates to Oracle Game
10   True iff Provable Sound & Complete
  Examples of Proofs:
20 95     - Repeat from Informal Slides ∃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, ∧/∨, ∀/∃, →/←
40 34     - 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 & Semantics (ppt):
20 4 6   Syntax Which strings are grammatically correct formulas?
Context Free Grammar & Closure
  Sentax What does formula α mean?
  A lot more You can skip it.
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
15   Computable ∃ Alg A, ∀ Inputs I, A(I)=P(I)
4   Uncomputable ∃P∀M∃I M(I)≠P(I)
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|
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)
40   Coding Phase vs Execution Phase ∃ Alg A, ∃ # k, ∀ Inputs I, ∃ time t, A(I)=P(I) & Lines(A,I)=k & Time(A,I)=t
40   Compiling Java to TM ∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I)
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
  

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.