Advanced Logic & Metamathematics

Moving beyond the application of logic to prove theorems, we enter the realm of metamathematics: using mathematics to study mathematics itself. This field addresses the deep questions about the power and limitations of formal systems.

Formal Systems and Models

A formal system consists of:

1. Language: A set of symbols (variables, connectives, quantifiers).
2. Grammar: Rules for constructing Well-Formed Formulas (WFFs).
3. Axioms: A set of statements assumed to be true.
4. Rules of Inference: Rules (like Modus Ponens) to derive new formulas from existing ones.

A model for a formal system is a mathematical structure where the axioms of the system are true. For example, the set of natural numbers $\mathbb{N}$ is a model for Peano Arithmetic.

Consistency and Completeness

• Consistency: A system is consistent if it is impossible to derive both $A$ and $\neg A$ for any formula $A$. A system that is inconsistent is worthless, as any statement can be proven from a contradiction ($Ex$ $Falso$ $Quodlibet$).
• Completeness: A system is complete if every true statement (in every model of the system) can be proven using the system’s rules and axioms.

Gödel’s Completeness Theorem

In 1929, Kurt Gödel proved that First-Order Logic (FOL) is complete. This means that if a formula is valid (true in all models), then there exists a formal proof for it. This was a triumph for Hilbert’s program to formalize mathematics.

Gödel’s Incompleteness Theorems

The triumph was short-lived. In 1931, Gödel published his most famous work, which fundamentally changed our understanding of mathematics.

The First Incompleteness Theorem

Any effectively generated formal system capable of expressing basic arithmetic (like Peano Arithmetic) cannot be both consistent and complete.

Specifically, there will always be statements $G$ within the system such that neither $G$ nor $\neg G$ can be proven, even though we can see (from a “meta” perspective) that $G$ is true. Gödel constructed such a statement by encoding the sentence “This statement is not provable in this system” into a numerical relationship.

The Second Incompleteness Theorem

No such formal system can prove its own consistency using its own rules.

If we want to prove that Arithmetic is consistent, we must use a stronger system (like Set Theory), but then we must ask: is Set Theory consistent? This leads to an infinite regress.

Decidability and the Halting Problem

The Entscheidungsproblem (Decision Problem) asked: Is there an algorithm that can determine if any given statement is provable from a set of axioms?

Alan Turing and Alonzo Church independently proved in 1936 that the answer is no. Turing did this by introducing the Turing Machine and proving that the “Halting Problem” is undecidable. This linked the foundations of logic directly to the foundations of computer science.

Model Theory and Non-Standard Analysis

Model Theory studies the relationship between formal languages and their interpretations. One fascinating result is the existence of non-standard models.

• For Peano Arithmetic, there are “non-standard” models that contain “infinite” integers that behave like normal integers but come “after” all the standard natural numbers.
• For Real Analysis, this led to Non-Standard Analysis, which rigorously formalizes “infinitesimals” (infinitely small numbers), providing an alternative to the $ϵ-\delta$ approach for calculus.

Knowledge Check

The Significance of Logic

These results don’t mean that mathematics is “broken.” Rather, they define the boundaries of what formal systems can do. They show that mathematical truth is a larger concept than formal provability, and that mathematical discovery remains a creative, human endeavor that cannot be fully automated or exhausted.