Introduction (ppt):
	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
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 Γ⊧Φ

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.

.