Axiomatic WikiWWikiDDefinitionsProof from a theory
Definition·D104
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
, using the connective and quantifier notation for formulas: a proof of
from
is a
such that
,
, and, for every
,
is one of:
In words
A finite sequence of formulas with at least one entry, ending at the target formula, where every entry in it is one of: a logical axiom, a member of the theory, 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
The modus ponens clause
reads, in prefix form, as "
is
implies
": the earlier entry at index
must have exactly the shape of the implication from the earlier entry at index
to the current entry. 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.