Tests:
Test1, Sol
Test2Sol

Topics (Videos below)	Slides	Read	Prac	Sol
Introduction
Propositional Logic
Informal Understanding & Proofs
Formal Proofs
Syntax & Semantics
Induction
Computing
Complexity
Generalizing Neural Nets
Representing Numbers
Non Constructive Proofs
Vector Spaces
Information Theory Example

Request:
     Jeff tends to talk too fast. Please help him go pole pole slowly.
     Please ask questions.

Mandate:
       Teaching numerous courses has led me to believe that a lack of
       abstract and logical thinking, along with a shallow grasp of the big
       picture, is often the root cause of student struggles.
       To address this, I explain the same material from many perspectives,
       aiming for at least one to resonate with your subconscious.
       To ensure you aren't overwhelmed, I offer detailed insights on the
       main topic while keeping peripheral matters in a more relaxed context.

How to Study:
     Watch, Pause, Think, and Unpause the slides/videos.
     Try to solve things yourself.
     If you get stuck, watch for another slide or two.
     Repause it. Was that enought of hint so that you can now solve it?
     After watching the entire solution, ask yourself what you were missing.
     Maybe set all notes aside and see if you can now write up the solution on your own.

Readings:
No text required
Jeff's Logic Chapter
George Tourlakis. Mathematical Logic, Wiley. [Not required for Jeff's section]
Mathematics for Computer Science, Lehman, Leighton and Meyer
Russell's Proof Rules
Foundations of Computer Science
Discrete Math
YouTube: logic, 1, all or 4, 6, 10-21. Find us others.
More Jeff Topics
Jeff's Fun Stuff

Symbol Meaning:
ppt Power Point Slides
5 Video from this year's Math1019 (5min)
5 Video from 2021
5 Video from 2020 (Rough because first year teaching it)
5 Never taught
Video covers more than needed.
Sorry. The plan is not to cover this.
Pooh

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):
	Propositional Logic	And, Or, Neg, Implies
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 ⊢, Implies ⊧
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 ⊂
	Tautology, Equiv, and Proofs	[(A → C) ∨ (B → C)]   ≡   [(A∧B) → C]
	- Table	Check all 2n assignments
	- Cases	Within each case simplify
	- Chain of equivalences	(x+y)2-(x2+y2) = (x2+2xy+y2)-(x2+y2) = 2xy
	- Hilbert	Each line follows from previous
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 (γ∨α)∧(γ∨β)
40	Arguing Our Rules/Lemmas:	Lots of intuition
	- And vs Or	Separating vs Selection
22 6	- Implies	Modus Ponens, Contrapositive, & Transitivity
	- Deduction	Assume α, prove β, conclude α→β.
	- Cases	Two cases α & β. Case α, prove γ. Case β, prove γ. Conclude γ.
	- Contradiction	From ¬α → (β∧¬β) conclude α
	- Distributive	γ∧(α∨β) iff (γ∧α)∨(γ∧β) and γ∨(α∧β) iff (γ∨α)∧(γ∨β)
	- Without Loss of Generality	Exploit symmetries to avoid too many cases
	Example Proofs
43 3 30 8	- Axiom Schema	"x nurse young" → "x are mammals"
46 6	- A World with out Racism	Winding to contradiction
Math 1090 only material
15	- Pleasing Father	(A ∨ B)→ C)   ≢   (A → C) ∨ (B → C)   ≡   (A ∧ B)→ C)
	- Horn Clauses	A solution can be found faster
15 15	- Hard Example	Brute for proof from both directions.
11	Davis-Putnam	Algorithm and Proof Technique by Example.
11 18	Formulas vs Circuits	Circuits reuse computations and Formulas (¬P∧Q)∨(R⊕S)→T do not.
10 8	NP vs Co-NP	There are not likely smaller proofs witnessing that a formula is satisfiable or a tautology
Skipped material
34	True iff Provable	Sound & Complete
62 9 12 40	More Davis Putnam Alg
Predicate Logic - Informal Understanding & Proofs (ppt):
- 1019/1090 Intro:		Forall object, Exists object
26 26	Objects, Predicates, & Relations	∀x,y [Daughter(y,x) iff Parent(x,y) ∧ Female(y)]
	- Hugely Expressive	Helps you understand and prove mathematical statements
	Intro to Quantifiers	∀x ≡ for All x  and   ∃x ≡ there Exists a y
	- Testing Validity	An Infinite Iterative Algorithm
5 5	Order of Quantifiers	∀x∃yP(x,y)   vs   ∃y∀xP(x,y)
	- So wrong	∀inputs x, ∃program J, J(x)=P(x)
	Negations	¬∃xP(x) ≡ ∀x¬P(x)
12 10 14	Quantifiers and Games	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.
	Humans are Mortal	"All humans are mortal" and "Socrates is human" hence "Socrates is mortal"
10 6	Understanding from the Inside	∀x [∃y+y=0] ≡ ∀x Property(x)
38 21	Playing the Game	∃a∀x∃y x=a ∨ x×y=1
9 9	Proofs by 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."
		√2 is irrational and infinite primes.
	Formal Proof System	Arbitrary c vs Some c
- Math 1090 only material:		Going Deeper
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	- Solution to Hard Problem	∃ solution y HardProblem(y) & ∀ potential counter examples x ¬HardProblem(x)
	And-Or Tree Game	Prover/Adversary Game on Tree
19 15	Game Tree	∃Mw1∀Mb1∃Mw2∀Mb2... White-Wins(Mw1,Mb1,Mw2,Mb2,...)
41 17	Negations	¬∃xP(x) ≡ ∀x¬P(x)
	Restricted Domain	∃x∈S,P(x) ≡ ∃x,(x∈S)∧P(x) and ∀x∈S,P(x) ≡ ∀x,(x∈S)→P(x)
	Empty Set	∀x∈S,P(x) is true if S is empty.
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)}
4 9	Skolem/Auxiliary Functions	∀x∃yP(x,y) ⇒ P(x,y∃(x))
	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)
100	- 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)
26 4 17 20	Formal vs Informal:
	- Adding ∀ & ∃	Relates to Adversary Game and to Prover Game
	- Removing ∀ & ∃	Relates to Oracle Game
12	True iff Provable	Sound & Complete
	Examples of Proofs:
44 23 95	- Repeat from Informal Slides	∃y∀xP(x,y) → ∀x∃yP(x,y)
26 10	- Distributive Laws	Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)]   and    ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
21 9	- Proof by Cases	From α∨β, α→γ, and β→γ, prove γ
15 29 68	- Proof by Duality	Switch true/false, ∧/∨, ∀/∃, →/←
35 34	- Free Variable Fail	α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true
25 42	Proving x+1>x	Non-Logical Axioms Γ (e.g., to do number theory)
	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):
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)
42 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.
44	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.
75	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.
	- Parsing Syntax	Building a parse tree for a logical sentence
82	- 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)
13 4	Uncomputable	∃P∀M∃I M(I)≠P(I)
	Table Look Up vs TM	∀k∃Mtable∀x,y≤k Mtable(x,y)=x×y   vs   ∃M∀x,y M(x,y)=x×y
16 26	Probabilistic Algorithms	∃M∀I PrR[M(I,R)≠P(I)] ≤ 2-|R|
37 54	Time Complexity	∃M∃c∀I M(I)=P(I) and Time(M,I)≤ |I|c
30 44	Classifying Functions	f(n)∈O(g(n)) ≡ ∃c∃n0∀n≥n0 f(n) ≤ cg(n)
62	Coding Phase vs Execution Phase	∃ Alg A, ∃ # k, ∀ Inputs I, ∃ time t, A(I)=P(I) & Lines(A,I)=k & Time(A,I)=t
33 25	Compiling Java to TM	∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I)
8 6	Universal TM	∃ TM MU, ∀ TM M, ∀ input I, MU(M,I) = M(I)
41 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
25 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
17 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]
23 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.
20 12 7	Gödel's Theorems	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.
34	Math Has a Fatal Flaw	Excellent Youtube video.
15	Proving Gödel's Completeness	Using Sequent Calculus
15	Sequent Calculus	Tree of Sequents α1∧...∧αn → β1∨...∨βm
Generalizing Neural Nets (ppt):
20	Machine Learning	How can a neural net do well on data it has never seen before.
	Theorem	∀ distributions of inputs ∀ models of machines
		For most random training data
		[∃ machine that does well on the training data] → [It does well on general inputs]
	Proof	Probabilities, union bound, Chernoff bounds
Representing Numbers (ppt):
30	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):
43	- 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

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.