Definition·D104
Proof from a theory
A finite sequence of formulas ending at the target, where every entry is a logical axiom, an assumption, or follows from earlier entries by modus ponens or generalization.
For a language
,
, and
: a proof of
from
is a
such that
,
, and, for every
:
In words
A finite sequence of formulas with at least one entry, ending at the target formula, where every entry in it is a logical axiom, or a member of the theory, or obtained from two earlier entries by modus ponens - one of them being the other implying the current entry, or obtained from one earlier entry by generalizing over some variable.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 · A09 (computed from the citation graph, not asserted).
Remarks
Modus ponens' condition reads
(writing
) in prefix form:
is "
implies
". Generalization is unrestricted here - it may bind any variable, even one free in a member of
used earlier in the proof - matching the standard Hilbert-style presentation; the subtlety this creates is confined to the deduction theorem (not proved on this wiki yet), not to this definition itself. Provability
- the existence of such a proof - is defined next.