FOM: Mayberry on justification of logic

[Neil Tennant]

John Mayberry wrote:
___________________________________________
you cannot *justify* a system of proof procedures without using the
the general notion of a model.
	Surely it is obvious that you have to justify a system of 
formal logical proof. Why should logical consequence be *defined* to be 
"formally derivable in just *this* system of formal rules and logical 
axioms"? 
___________________________________________

Clearly Mayberry is talking here of classical logic, rather than, say,
intuitionistic logic. 
	But even so, it seems to me that the question of justification
ought to be distinguished from the question of logical
completeness. For justification, all one needs is a soundness
theorem. (Some people with certain sorts of philosophical scruples
might even object to the claim that a proof of soundness furnished an
adequate justification; but their attitude only provides further
evidence that the question of soundness ought to be addressed
separately from the question of completeness.)
	The history of logic is one of a great variety of alternative
formalisms consisting of axioms and rules of inference (for, say, 
classical logic) all of whose deducibility relations turn out to be
coextensive. This history perhaps furnishes Mayberry's question

	Why should logical consequence be *defined* to be "formally 
	derivable in just *this* system of formal rules and logical axioms"?

with more rhetorical force than ought to be conceded, in the light of
what we now know to be the best system.
	The validity of logical reasoning is grounded in the rules we
can discern as somehow "at work" and underlying both the local and
global manoeurvres that mathematicians make when reasoning from axioms
to lemmas and theorems (and their corollaries). It took logicians a
long time to distill what I would regard as the essence of those
moves, namely the rules of introduction and elimination of logical
operators. Gentzen got them in 1936; and they were almost immediately
adopted by G"odel.
	An introduction rule tells one how to infer a conclusion with
a dominant occurrence of the logical operator in question; while the
corresonding elimination rule tells one how to "reason away from" a
major premiss with that operator dominant.
	For intuitionistic mathematics, the introduction and
elimination rules suffice. [For the cogniscenti who might object that
I have not mentioned the absurdity rule---ex falso quodlibet---I
should quickly add that one can show that it is *unnecessary* for the
logic of intuitionistic mathematics.]
	These introduction and elimination rules are so basic, elegant
and beautiful, and so obviously a distillation of the essence of the
reasoning going on in (intuitionistic) mathematics, that the system
consisting of them should, in my view, be exempt from the implicature
in Mayberry's question. That is to say, this system is *not* "just one
system among many". Rather, it is THE system; and what remains is to
justify it, IF anyone really has a seriously felt need for such a
justification.
	I contend that anyone expressing such a seriously felt need is
in the grip of a misconception as to what it is to expose, and
recognize, a final foundation for one's reasoning. It would be
impossible to convince the skeptic about these natural deduction rules
anyway, since those very rules would need to be used in any supposed
"justification" of the rules themselves. A soundness theorem would
have to be conducted in a language governed by the self-same rules of
logical reasoning. So too would any *further* philosophical argument
purporting to do more than a soundness theorem by way of justification
for the rules. [There is room here, by the way, for a technical
result, analogous to G"odel's 2nd incompleteness theorem: can one show
that it is impossible to establish the soundness of a system of
logical rules without using---hence, assuming the validity of---those
very rules?]
	If pressed, the intuitionist can say more about why the rules
are right, without (contra Mayberry) having to invoke anything like
models. For example, one could justify the rules by showing that they
preserve the property of *having a canonical warrant* from premisses
to conclusion of any proof constructed by means of the rules. This
requires an inductive specification of canonical warrant; and the
resulting soundness theorem is, in effect, the normalization theorem
for the system of natural deduction. This approach goes back to Dag
Prawitz's seminal paper "On the idea of a general proof theory",
Synthese 1974. Interestingly, this approach provides a "reduction" of
the whole system of rules to just the introduction rules. It is the
introduction rules by reference to which the notion of canonical
warrant is defined. The elimination rules are then justified (modulo
the introduction rules) by means of the reduction procedures involved
in normlaizing proofs. If we need a slogan, we can say: "The
introduction rules FIX the meanings of the logical operators; the
elimination rules merely UNPACK the consequences of those meanings."
	To summarize: so far as intuitionistic logic is concerned, the
system of deductive rules is so basic as to need no
justification. But, if one insists on justification, a justification
can be given that makes no use of the notion of a model. Moreover, it
effects a conceptual reduction from the whole set of rules
(introduction and elimination) to just the introduction rules.
	As I said earlier, however, Mayberry's claims concerned
*classical* logic rather than intuitionistic logic. So let us imagine
the system of basic deductive rules extended by the addition of any
one of the usual classical negation rules (double negation
elimination; classical reductio ad absurdum; the law of excluded
middle; the rule of constructive dilemma). Not one of these extra
classical rules can be justified without invoking the very rule
itself---or one provably equivalent to it, modulo intuitionistic
logic---in the course of providing the justification. So why not, as a
classical reasoner, simply adopt one of the classical rules without
further ado? The resulting system is classically sound; and that is
all that is required for *justification* of the choice of such a
system as a codification of correct classical reasoning.
	It is, of course, a major happy accident that we discovered
relatively early on the necessary truth that the resulting classical
system is also complete (at least, at first order). But it would have
been conceptually possible to concern oneself with the foundations of
mathematics even in ignorance of the (necessary fact of)
completeness. If, for example, no one had succeeded in proving
completeness, we could still be arguing about the comparative merits
of set theory v. category theory as a foundation for mathematics while
bearing in mind the conceptual distinction between deducibility by
means of our rules, and truth-preservation under all (classical)
interpretations.

Neil Tennant