[FOM] Comparing the power of logics

[Arnon Avron]

There is one claim that has explicitly or implicitly been made several times
during the discussion concerning intuitionistic logic: that
intuitionistic logic is actually stronger than classical logic
(or that it is an extension of classical logic). It was put forward
in  very clear terms by Andrej Bauer (in a private message): 

> Perhaps we should do precisely what you suggest and have two sets of
> connectives: "i-or", "i-not", ... and "c-or", "c-not", ... We could even
> put them all together in one big happy logic. Except it would turn out
> that this logic is intuitionistic and that the c-connectives are
> definable in terms of the i-connectives 
...
> This should
> be taken as evidence that intuitionistic logic is _more general_ than
> classical logic. Mathematicians like generality. Clearly, we need to
> educate them on this point.

Two questions concerning this claim.

First, I am not acquainted with any definition of c-not (say) in terms of the
i-connectives (like the way c-or is definable in classical logic in terms 
of c-not and c-and). Does anybody know one which preserves the
*consequence relation* of classical logic? Is there even a definable unary
connective @ in intuitionistic logic such that for every A, B we have
that  A and @@A intuitionistically follow from each other, 
and B intuitionistically  follows from the set {A, at A}?
(What I do know are some "translations" of classical logic into 
intuitionistic logic, but they either only preserve theoremhood (not 
the consequence relation!), or employ transformations of atomic formulas 
to something different (like their double negations). None of these
translations provides a definition of c-not in terms of the i-connectives).

Second, let us examine the thesis about the greater generality of
intuitionistic logic in the light of an example of a logic
which is *really* more general than classical logic according to the
definability criterion.  Assume that we use a language with four connectives:
the usual disjunction, conjunction and implication connectives,
together with a unary connective  ~ ("negation"). Denote
by CL~ the logic which is obtained by deleting (=>~) from the standard
Gentzen-type system for classical logic, where ~ is taken as the "negation"
connective  (Note that the positive fragment of CL~ is identical
to that of classical logic, but the "horror" called excluded middle
is not derivable in it. Isn't it great?).  Now it was observed by 
J. Y. Beziau that classical negation is definable in CL~ by:
                          -A = A->~A
Indeed, it is not difficult to prove that if we define a function  * by
p* = p, (A->B)* = A*->B*, (A\/B)* = A*\/B*, (A&B)* = A*&B*, (\not A)* = -(A*)
we get a precise translation of CL into CL~, such that \gamma=>\delta
is derivable in CL iff \gamma*=>\delta* is derivable in CL~. On the
other hand it is easy to prove that no translation of this sort in
the other direction exits. Hence CL~ is strictly more general than CL!

  But what is the *meaning* of ~, one may ask. Well, there is a thesis 
according to which the meaning of a connective is completely determined by 
the logical laws that govern it (I might discuss this thesis some other time).
But the main goal of this message is 
to raise a difficult question about comparison of logics which 
should be interesting also to people who think that the meaning
should determine the logical laws, not the other way around. Well, CL~ does
have a very simple semantics of the general type I have called
"non-deterministic matrices" ("Nmatrices", in short). In particular it
is strongly sound and complete w.r.t to the 2-valued Nmatrix in which
the truth-values are t and f, t is designated (and f is not), the
truth-tables of the positive connectives are the usual ones, while the
truth-table for ~ is given by ~t=f, ~f={t,f}. This means that any
valuation v which respects the truth-tables for the positive connectives,
and for which v(~A)=f in case v(A)=t, is legal (in terms of circuits,
one may think of ~ as a gate which outputs 0 if the input is 1, but
whose output is unpredictable and not uniform if the input is 0).
It is very easy to check that the truth-tale one obtains for the
definable connective - is indeed the classical truth-table for negation
(and it is hardly surprising that one cannot define a proper
nondeterministic two-valued connectives using the strictly deterministic
classical ones). So CL~ is strictly more general than classical logic 
not only from the proof-theoretical point of view, but also
from the semantic point of view.
  
 So should we start educating mathematicians
to use the more general CL~ rather than the dull CL? I am not sure, especially
that the job would not end at this point. Thus by moving to 3-valued
Namtrices, and then to 4-valued Nmatrices etc, we get logics which are provably
more and more general (in particular: more general then CL~), and we
shall need to educate mathematicians  to learn and use 
them instead of their poor Classical logic! Well, the sad truth is that 
although` I have found in a series of papers many applications of Nmatrices
(in proof theory, uncertainty reasoning, and other areas), for the
time being it seems to me that mathematicians can go on doing
usual mathematics without them (and without intuitionistic logic too...).
Even in mathematics not always more generality is better.

  But this discussion raises one difficult question, to which I admit
not to have a satisfactory answer: to what extent the possibility
of translating one Logic L1 into another L2 makes L2 stronger than L1?
It somehow seems paradoxical to say that by deleting a rule from 
classical logic we get a stronger system! Yet we all think that the 
classical logic of negation and disjunction (say) is stronger
than the pure implicational fragment of classical logic, because
classical implication is definable in terms of classical
negation and disjunction. What is the difference, if any?

Arnon Avron