This article will study a class of deduction systems
that allow for a limited use of the modus ponens
method of deduction. We will show that it is possible to
devise axiom systems α that can recognize their consistency
under a deduction system D provided that:
(1) α treats multiplication as a 3-way relation
(rather than as a total function), and that (2) D does not allow
for the
use of a modus ponens methodology above essentially the levels
of Π1 and Σ1 formulae.
¶
Part of what will make this boundary-case exception to
the Second Incompleteness Theorem interesting is that we will
also characterize generalizations of the Second Incompleteness
Theorem that take force when we only slightly weaken the assumptions
of our boundary-case exceptions in any of several further directions.