This symbol is used to claim that a statement is a theorem of the
classical propositional calculus, i.e. that it follows by applications
of Modus Ponens from instantiations of the axioms (which may be the common
three involving 'implies', but need not be).
This symbol is used to claim that a statement is a theorem of the
classical first-order predicate calculus, i.e. that it follows by
applications of Modus Ponens, and generalisation from instantiations of
the Axioms (which may be the common three involving 'implies', together
with forall-instantiation and moving forall inside implication, but need
not be).
This symbol represents a line in a formal proof which is an instance of
an axiom. The first child is the line in the proof: the second is the
axiom used.
Note how the issue of substitution is dealt with in the specification
of axiom 4 of the predicate calculus. Essentially, it has to be
assumed that beta-reduction takes place when the axiom is instantiated.
This symbol represents the generation of a line of a proof by application
of Modus Ponens. The first argument is the new well-formed formula (B),
the second is the line number in the proof for A and the third is the line
number in the proof for A implies B.
This symbol represents the generation of a line of a proof by application
of Generalisation. The first argument is the new well-formed formula
(forall x.B) and the second is the line number in the proof for B.
This symbol represents a sequence of justified well-formed formulae
(i.e. objects of type ProofLine). The single argument is a List of
ProofLine objects.
This symbol is used to state, with proof (the second child), that a
statement (the first child) is a theorem of the classical propositional
calculus, i.e. that it follows by applications of Modus Ponens from
instantiations of the axioms (which may be the common three involving
'implies', but need not be).
This symbol is used to state, with justification, that a statement is a
theorem of the classical first-order predicate calculus, i.e. that it
follows by applications of Modus Ponens, and generalisation from
instantiations of the Axioms (which may be the common three involving
'implies', together with forall-instantiation and moving forall inside
implication, but need not be), and the hypotheses (elements of the set
which is the second child).
This symbol is used to claim that a statement (the first child) is a
deduction of the classical propositional calculus, i.e. that it follows by
applications of Modus Ponens from instantiations of the axioms (which may
be the common three involving 'implies', but need not be), and the
hypotheses (elements of the set which is the second child).
This symbol is used to claim, with proof (the third child), that a
statement (the first child) is a deduction of the classical propositional
calculus, i.e. that it follows by applications of Modus Ponens from
instantiations of the axioms (which may be the common three involving
'implies', but need not be), and the hypotheses (elements of the set which
is the second child).
This symbol is used to claim that a statement (the first child) is a
deduction of the classical predicate calculus, i.e. that it follows by
applications of Modus Ponens, forall-introduction and exists-elimination,
from instantiations of the axioms (which may be the common three involving
applications of Modus Ponens, and generalisation from instantiations of
the Axioms (which may be the common three involving 'implies', together
with forall-instantiation and moving forall inside implication, but need
not be), and the hypotheses (elements of the set which is the second child).
This symbol is used to claim, with proof (the third child), that a
statement (the first child) is a deduction of the classical predicate
calculus, i.e. that it follows by applications of Modus Ponens,
forall-introduction and exists-elimination, from instantiations of the
axioms (which may be the common three involving applications of Modus
Ponens, and generalisation from instantiations of the Axioms (which may be
the common three involving 'implies', together with forall-instantiation
and moving forall inside implication, but need not be), and the hypotheses
(elements of the set which is the second child).