# Lob's Theorem

## Summary

Lob's Theorem asserts that no formal system T can prove statements of the form "If A is provable in T, then A is true" unless it is also capable of proving A directly. It can be seen as a generalization of Godel's Second Incompleteness Theorem.

## Context

This concept has the prerequisites:

- semantics of first-order logic (Lob's Theorem is a statement about the semantics of first-order logic.)
- proofs in first-order logic (Lob's Theorem is a statement about proofs in first-order logic.)
- Godel numbering (Stating Lob's Theorem requires Godel numbering.)
- Godel's Incompleteness Theorems (Lob's Theorem is a generalization of Godel's Second Incompleteness Theorem, and the proof is analogous.)

## Goals

- Know the statement of Lob's Theorem and why it is significant

- Show how to derive Godel's Second Incompleteness Theorem as a special case of Lob's Theorem

- Prove Lob's Theorem

## Core resources (read/watch one of the following)

## -Free-

→ Notes on Logic (2013)

Lecture notes for a course on first order logic.

→ Wikipedia

## -Paid-

→ A Mathematical Introduction to Logic

An undergraduate textbook in mathematical logic, with proofs.

Location:
Part of Section 3.7, "Second Incompleteness Theorem," from pages 268-270

## See also

-No Additional Notes-