In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, Löb's theorem states that in
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
(PA) (or any formal system including PA), for any formula ''P'', if it is provable in PA that "if ''P'' is provable in PA then ''P'' is true", then ''P'' is provable in PA. If Prov(''P'') means that the formula ''P'' is provable, we may express this more formally as
:If
:
:then
:
An immediate corollary (the
contrapositive
In logic and mathematics, contraposition refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as proof by contraposition. The contrapositive of a statem ...
) of Löb's theorem is that, if ''P'' is not provable in PA, then "if ''P'' is provable in PA, then ''P'' is true" is not provable in PA. For example, "If
is provable in PA, then
" is not provable in PA.
Löb's theorem is named for
Martin Hugo Löb, who formulated it in 1955. It is related to
Curry's paradox
Curry's paradox is a paradox in which an arbitrary claim ''F'' is proved from the mere existence of a sentence ''C'' that says of itself "If ''C'', then ''F''", requiring only a few apparently innocuous logical deduction rules. Since ''F'' is arbi ...
.
Löb's theorem in provability logic
Provability logic Provability logic is a modal logic, in which the box (or "necessity") operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic.
Examples
...
abstracts away from the details of encodings used in
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research i ...
by expressing the provability of
in the given system in the language of
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
, by means of the modality .
Then we can formalize Löb's theorem by the axiom
:
known as axiom GL, for Gödel–Löb. This is sometimes formalized by means of an inference rule that infers
:
from
:
The provability logic GL that results from taking the
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
K4 (or K, since the axiom schema 4,
, then becomes redundant) and adding the above axiom GL is the most intensely investigated system in provability logic.
Modal proof of Löb's theorem
Löb's theorem can be proved within modal logic using only some basic rules about the provability operator (the K4 system) plus the existence of modal fixed points.
Modal formulas
We will assume the following grammar for formulas:
# If
is a
propositional variable
In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building-blocks of propositi ...
, then
is a formula.
# If
is a propositional constant, then
is a formula.
# If
is a formula, then
is a formula.
# If
and
are formulas, then so are
,
,
,
, and
A modal sentence is a modal formula that contains no propositional variables. We use
to mean
is a theorem.
Modal fixed points
If
is a modal formula with only one propositional variable
, then a modal fixed point of
is a sentence
such that
:
We will assume the existence of such fixed points for every modal formula with one free variable. This is of course not an obvious thing to assume, but if we interpret
as provability in Peano Arithmetic, then the existence of modal fixed points follows from the
diagonal lemma
In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of self-referential sentences in certain formal theories of the natural numbers—specificall ...
.
Modal rules of inference
In addition to the existence of modal fixed points, we assume the following rules of inference for the provability operator
, known as
Hilbert–Bernays provability conditions In mathematical logic, the Hilbert–Bernays provability conditions, named after David Hilbert and Paul Bernays, are a set of requirements for formalized provability predicates in formal theories of arithmetic (Smith 2007:224).
These conditions are ...
:
# (necessitation) From
conclude
: Informally, this says that if A is a theorem, then it is provable.
# (internal necessitation)
: If A is provable, then it is provable that it is provable.
# (box distributivity)
: This rule allows you to do modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.
Proof of Löb's theorem
Much of the proof does not make use of the assumption
, so for ease of understanding, the proof below is subdivided to leave the parts depending on
until the end.
Let
be any modal sentence.
# From the existence of modal fixed points for every formula (in particular, the formula
) it follows there exists a sentence
such that
.
# From 1, it follows that
.
# From the necessitation rule, it follows that
.
# From 3 and the box distributivity rule, it follows that
.
# Applying the box distributivity rule with
and
gives us
.
# From 4 and 5, it follows that
.
# From the internal necessitation rule, it follows that
.
# From 6 and 7, it follows that
.
Now comes the part of the proof where the hypothesis is used.
# Assume that
. Roughly speaking, it is a theorem that if
is provable, then it is, in fact true. This is a claim of ''soundness''.
# From 8 and 9, it follows that
.
# From 1, it follows that
.
# From 10 and 11, it follows that
# From 12 and the necessitation rule, it follows that
.
# From 13 and 10, it follows that
.
Examples
An immediate corollary of Löb's theorem is that, if ''P'' is not provable in PA, then "if ''P'' is provable in PA, then ''P'' is true" is not provable in PA. Given we know PA is consistent (but PA does not know PA is consistent), here are some simple examples:
* "If
is provable in PA, then
" is not provable in PA, as
is not provable in PA (as it is false).
* "If
is provable in PA, then
" is provable in PA, as is any statement of the form "If X, then
".
* "If
the strengthened finite Ramsey theorem is provable in PA, then the strengthened finite Ramsey theorem is true" is not provable in PA, as "The strengthened finite Ramsey theorem is true" is not provable in PA (despite being true).
In
Doxastic logic Doxastic logic is a type of logic concerned with reasoning about beliefs.
The term ' derives from the Ancient Greek (''doxa'', "opinion, belief"), from which the English term ''doxa'' ("popular opinion or belief") is also borrowed. Typically, a d ...
, Löb's theorem shows that any system classified as a ''
reflexive'' "
type 4" reasoner must also be "''modest''": such a reasoner can never believe "my belief in P would imply that P is true", without also believing that P is true.
Gödel's second incompleteness theorem follows from Löb's theorem by substituting the false statement
for ''P''.
Converse: Löb's theorem implies the existence of modal fixed points
Not only does the existence of modal fixed points imply Löb's theorem, but the converse is valid, too. When Löb's theorem is given as an axiom (schema), the existence of a fixed point (up to provable equivalence)
for any formula ''A''(''p'')'' modalized in p'' can be derived.
Thus in
normal modal logic In logic, a normal modal logic is a set ''L'' of modal formulas such that ''L'' contains:
* All propositional tautologies;
* All instances of the Kripke schema: \Box(A\to B)\to(\Box A\to\Box B)
and it is closed under:
* Detachment rule (''modus po ...
, Löb's axiom is equivalent to the conjunction of the axiom schema 4,
, and the existence of modal fixed points.
Notes
Citations
References
*
*
*
*
External links
Löb's theoremat
PlanetMath
PlanetMath is a free, collaborative, mathematics online encyclopedia. The emphasis is on rigour, openness, pedagogy, real-time content, interlinked content, and also community of about 24,000 people with various maths interests. Intended to be c ...
The Cartoon Guide to Löb’s Theoremby
Eliezer Yudkowsky
Eliezer Shlomo Yudkowsky (born September 11, 1979) is an American decision theory and artificial intelligence (AI) researcher and writer, best known for popularizing the idea of friendly artificial intelligence. He is a co-founder and research ...
{{DEFAULTSORT:Lob's theorem
Mathematical logic
Modal logic
Theorems in the foundations of mathematics
Metatheorems
Provability logic
Mathematical axioms