Kicking Away the Classical Ladder

This part of the postscript to An Introduction to Non-Classical Logic struck me as important:

It may fairly be asked what logic I have been using to specify and reason about the semantics of the various logics we have been dealing with. The procedures employed have not been formal ones, of course. Like most mathematics, matters have been left at an informal level. They could be formalised in a standard set theory, such as Zermelo Fraenkel set theory, based on classical logic. But to someone, such as an intuitionist or paraconsistent logician, who takes such reasoning not to be correct, at least in part, things cannot be left like this. The classical ladder must, so to speak, be kicked away.

If non-classical logics are correct formalizations of some kinds of thinking, it's worth wondering why metalogical reasoning about those logics should be done in classical terms. If non-classical logics were just, so to speak, games of symbol-manipulation, then abandoning their principles when doing "correct" reasoning would make sense. But non-classical logics have philosophically respectable semantics, thanks to recent scholarship. Not only do the proof-theories of these logics make internal sense, but those proof-theoretic methods mirror semantic interpretations that make intuitive sense and link the symbol-manipulation of the logics to real ways of thinking about real things.

I think there is an analogy with non-Euclidean geometries. At first, they were perhaps viewed as logically-consistent but meaningless consequences of the nature of geometrical reasoning. Recent advances in the sciences have shown that, in truth, non-Euclidean geometries are fair representations of actual things. Non-classical logics are fair representations of things: modal logic of possibility and necessity, fuzzy logic of vagueness, and so on. Though these logics will always be developing alongside metaphysical accounts of the nature of the reality each logic is describing, they have already come into their own. There is no barrier to using non-classical logic to reason about logic itself. This is to my mind (and probably to others) a very difficult thing to attempt. The classical ladder is comfortable and natural. Thinking about logic paraconsistently, for example, is strange.

But it might just be the way forward.