**PHIL30043: The Power and Limits of Logic** is a University of Melbourne undergraduate subject. It covers the metatheory of classical first order predicate logic, beginning at the *Soundness* and *Completeness* Theorems (proved not once but *twice*, first for a tableaux proof system for predicate logic, then a Hilbert proof system), through the *Deduction Theorem*, *Compactness*, *Cantor’s Theorem*, the *Downward Löwenheim–Skolem Theorem*, *Recursive Functions*, *Register Machines*, *Representability* and ending up at *Gödel’s Incompleteness Theorems* and *Löb’s Theorem*.

The subject is taught to University of Melbourne undergraduate students (for Arts students as a part of the Philosophy major, for non-Arts students, as a breadth subject). Details for enrolment are here. I make use of video lectures I have made freely available on Vimeo.

The course is divided into four major sections and a short prelude. Here is a list of all of the videos, in case you’d like to follow along with the content.

- Logical Equivalence
- Disjunctive Normal Form
- Why DNF Works
- Prenex Normal Form
- Models for Predicate Logic
- Trees for Predicate Logic

- Introducing Soundness and Completeness
- Soundness for Tree Proofs
- Completeness for Tree Proofs
- Hilbert Proofs for Propositional Logic
- Conditional Proof
- Hilbert Proofs for Predicate Logic
- Theories
- Soundness and Completeness for Hilbert Proofs for Predicate Logic

- Counting Sets
- Diagonalisation
- Compactness
- Non-Standard Models
- Inexpressibility of Finitude
- Downward Löwenheim–Skolem Theorem

- Functions
- Register Machines
- Recursive Functions
- Register Machine computable functions are Recursive
- The Uncomputable

- Deductively Defined Theories
- The Finite Model Property
- Completeness
- Introducing Robinson’s Arithmetic
- Induction and Peano Arithmetic
- Representing Functions and Sets
- Gödel Numbering and Diagonalisation
- Q (and any consistent extension of Q) is undecidable, and incomplete if it’s deductively defined
- First Order Predicate Logic is Undecidable
- True Arithmetic is not Deductively Defined
- If Con(PA) then PA doesn’t prove Con(PA)

← Proof Theory: Logical and Philosophical Aspects | Class Archive | PHIL20030: Meaning, Possibility and Paradox →

I’m *Greg Restall*, and this is my personal website. I teach philosophy and logic as Professor of Philosophy at the University of Melbourne. ¶ Start at the home page of this site—a compendium of recent additions around here—and go from there to learn more about who I am and what I do. ¶ This is my personal site on the web. Nothing here is *in any way* endorsed by the University of Melbourne.

- School of Historical and Philosophical Studies, The University of Melbourne, Parkville 3010, Australia.
- greg@consequently.org
- keybase.io/consequently, to sign or encrypt a message to send to me privately.
- @consequently on Twitter.
- @consequently on Instagram.

To receive updates from this site, you can subscribe to the RSS feed of all updates to the site in an RSS feed reader, or follow me on Twitter at @consequently, where I’ll update you if anything is posted.