Topics:
Introduction
Propositional Logic
Informal Understanding & Proofs
Formal Proofs
Syntax & Semantics,
Examples:
Induction
Computing
Complexity
Representing Numbers
Non Constructive Proofs
Vector Spaces
Information Theory Example

ppt Power Point Slides
New Video not made in lectures (5min)
5 Video from this year (5min)
5 Will be covered later this year (expected time 5min)
5 Video from last year (Rough because first year teaching it) (5min)
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):
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)
	Restricted Domain	∃x∈S,P(x) ≡ ∃x,(x∈S)∧P(x) and ∀x∈S,P(x) ≡ ∀x,(x∈S)→P(x)
	Relations vs Functions	y=father(x) ≡ ∃y,fatherOf(x,y)
	Empty Set	∀x∈S,P(x) is true if S is empty.
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)
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
20	- Machine Learning	How can a neural net do well on data it has never seen before.
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): (See Informal-Follow the Parse Tree and Induction-Parsing Syntax)
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
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

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.