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
5 Video from this year (5min)
Video covers more than needed.
Skipped Covering
Pooh
Videos

Introduction (ppt):
53	Administrative Details	How the course will be run.
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): CLO 1
6	What This Logic Is and Is Not.	It is not hope, beliefs, probability, time dependent, but just true or false.
2	Quick Examples	Clue and Menu
14	Proof Techniques/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	From ¬¬α, conclude α
	- Excluded Middle	α∨¬α and ¬(α∧¬α). The universe must decide.
	- Commutative	α∧β iff β∧α and α∨β iff β∨α
	- De Morgan's Law	¬(α∧β) iff ¬α∨¬β
	- Distributive	γ∧(α∨β) iff (γ∧α)∨(γ∧β) and γ∨(α∧β) iff (γ∨α)∧(γ∨β)
3 42	Example Proof	Prove "A World with out Racism"
30 8	Axiom Schema	"x nurse young" → "x are mammals"
9	Formal Proofs	Each sentence in the Hilbert sequence follows from axioms or previous
15	Hard Example	Brute for proof from both directions.
9	Tautologies vs Lemmas	Proving Lemmas from Tautologies and visa versa.
23	Operator's Truth Tables	And ∧, Or ∨, Not ¬, Implies →, iff, Exclusive-Or ⊕
9	Evaluate/Build	With α=T, α∨γ evaluates to T. From α, conclude α∨γ.
12	Simplify	With α=T, α∧γ simplifies to γ.
14	Tautologies	Formula is true under every setting of the variables.
11	Propositional Formulas vs Circuits	Circuits reuse computations and Formulas (¬P∧Q)∨(R⊕S)→T do not.
	Proofs of Tautologies: CLO 2
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	- Formal Proofs	We will convert DP algorithm to a DP proof.
62	- Davis Putnam Alg	Heuristic that might be fast
40	- Davis-Putnam Axioms
	- Deduction	Assume α, prove β, conclude α→β
	- Evaluate/Building	From α, α', ¬β, and ¬β', conclude α∧α', ¬(β∧γ), ¬(γ∧β), α∨γ, γ,∨α ¬(β∨β'), γ→α, β→γ, ¬(α→β), and ¬¬α.
	- Merge	From α→Φ, and ¬α→Φ, conclude Φ
	- Davis-Putnam Proof CLO 5	Mirrors a Davis-Putnam computation to ensures proof system is Complete.
	Horn Clauses	A solution can be found faster
Predicate Logic - Informal Understanding & Proofs (ppt):
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 father(x,y) ∧ girl(y)]
5	Order of Quantifiers	∀x∃yP(x,y)   vs   ∃y∀xP(x,y)
80	Sets of Tuples:	α is true for each tuple in S = {❬x1,y1,x2,y2❭ | x1&x2∈U, y1=y1∃, y2=y2∃(x1)}
14	Free and Bound Variables:	α(x)∧∀xβ(x)
	- Free Variables	Values supplied by boss
14	Sentence Truth	An Infinite Iterative Algorithm
9	Skolem/Auxiliary Functions	∀x∃yP(x,y) ⇒ P(x,y∃(x))
17	Negations	¬∃xP(x) ≡ ∀x¬P(x)
6	Understanding from the Inside	∀x [∃y+y=0] ≡ ∀x Property(x)
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	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	- Game Tree	∃Mw1∀Mb1∃Mw2∀Mb2... White-Wins(Mw1,Mb1,Mw2,Mb2,...)
21	- Reals	∃a∀x∃y x=a ∨ x×y=1
	Oracles:
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).
67 12	- Proof Game with Oracle	Various examples with Oracle, Prover, and Adversary
13	- Humans are Mortal	"All humans are mortal" and "Socrates is human" hence "Socrates is mortal"
26	- Diagonal Solutions	to remove
35	- f(x) Solution	to remove
34	- Free Variable Fail	α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true
26 9	- Distributive Laws	Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)]    and    ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
16 23	- Order of Quantifiers	∃y∀xP(x,y) ⇒ ∀x∃yP(x,y)
67	Computing:	∃ Alg A, ∀ Inputs I, A(I)=P(I)
39 57 7	- Coding Phase vs Execution Phase	∃ Alg A, ∃ # k, ∀ Inputs I, ∃ time t, A(I)=P(I) & Lines(A,I)=k & Time(A,I)=t
27 58	- Compiling Java to TM	∀ Java Programs J, ∃ TM M, ∀ input I, J(I)=M(I)
Formal Proofs (ppt): CLO 3
	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!
9	Our Formal Proof System Quick	Hilbert, Lemmas, Deduction, Adding/Removing Quantifiers
42	Game and Γ Example	Comparing Informal and Formal Proofs
		Non-Logical Axioms Γ (e.g., to do number theory)
12	Gödel	Completeness and Incompleteness
4	Our Formal Proof System:
	- 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(φ').
14	- Lemmas via Substitutions: CLO 7	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)]
? 9	- Deduction	Assume α(x'), prove β(x'), conclude α(x)→β(x)
9	- Quantifier Rules: CLO 6	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)
	Formal vs Informal:
17	- Adding ∀ & ∃	Relates to Adversary Game and to Prover Game
20	- Removing ∀ & ∃	Relates to Oracle Game
	Examples of Proofs:
95	- Order of Quantifiers	∃y∀xP(x,y) → ∀x∃yP(x,y)
10	- Distributive Laws	Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)]    and    ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
9	- Proof by Cases	From α∨β, α→γ, and β→γ, prove γ
68	- Proof by Duality	Switch true/false, ∧/∨, ∀/∃, →/←
	- Free Variable Fail	α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true
	Proving Sound	For each rule "From line φ, include line φ' " prove
	Sequent Calculus LK: CLO 4	Tree of Sequents α1∧...∧αn → β1∨...∨βm
	- Prove each its Rules	Left and Right rule for ∧, ∨, ¬ ∃, and ∀
Syntax (ppt):		Which strings are grammatically correct formulas?
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
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	Time Complexity	∃M∃c∀I M(I)=P(I) and Time(M,I)≤ |I|c
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	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	Probabilistic Algorithms	∃M∀I PrR[M(I,R)≠P(I)] ≤ 2-|R|
6	Universal TM	∃ TM MU, ∀ TM M, ∀ input I, MU(M,I) = M(I)
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	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
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	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.
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.
Induction (ppt):		[S(0)&∀i[S(i-1)→S(i)]] → ∀iS(i)
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)
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

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.