Mastering Formal Proofs in MATH 1090: Mortals, Quantifiers & More 📚

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!
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)
Formal vs Informal:
- Adding ∀ & ∃ Relates to Adversary Game and to Prover Game
- Removing ∀ & ∃ Relates to Oracle Game
True iff Provable Sound & Complete
Examples of Proofs:
- Repeat from Informal Slides ∃y∀xP(x,y) → ∀x∃yP(x,y)
- Distributive Laws Eg ∀x[α(x)→β(x)] → [∀xα(x)→∀xβ(x)] and ∀x[α(x)∧β(x)] iff [∀xα(x)∧∀xβ(x)]
- Proof by Cases From α∨β, α→γ, and β→γ, prove γ
- Proof by Duality Switch true/false, ∧/∨, ∀/∃, →/←
- Free Variable Fail α(x)→∀xα(x) and its dual ∃xα(x)→α(x) are not true
Proving x+1＞x Non-Logical Axioms Γ (e.g., to do number theory)
More Details:
- Definitions Again
- 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