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

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.
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

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.