[FOM] Re: Combining classical and intuitionistic features in one logic

Joao Marcos vegetal at cle.unicamp.br
Fri Feb 13 07:15:59 EST 2004


Concerning my earlier reply to you on the combination of classical and
intuitionistic logics, I sent a copy of it to some of my colleagues off-list,
and one of them, Carlos Caleiro, ended up proposing a much more careful and
detailed answer to your questions.  I believe it might be of interest to
everybody.  Below I paste his message integrally.

Joao Marcos


On Feb 12, "Carlos Caleiro" wrote:

Dear Alex and Joao,

Fibring is a very general mechanism for combining logics originally proposed
by Dov Gabbay. There would be much to say about it, its developments and
problems, but that is not the point here. For an account of the line of work
that I and close collaborators have been involved in in the last few years
in this direction you can browse at http://clc.math.ist.utl.pt/fiblog.html.

Now, the particular example of fibring (mixing up the connectives) of
classical and intuitionistic logics into some interesting logic is certainly
appealing. However, if you consider their fibring at the semantic level,
even without any sharing of connectives, the resulting combined logic turns
out to be just classical! This happens essentially because the only Heyting
algebras that are sound for the classical connectives are precisely Boolean.
A solution to this problem is indeed modulated fibring. We have also been
working on another extension of fibred semantics that also solves this
problem, called cryptofibring, but it is unfortunately not yet in readable

At the deductive level, however, things are different. By just putting
together the usual axiomatizations of classical and intuitionistic logics we
do not end up with intuitionistic connectives behaving classically!

This may seem in contradiction with Dov Gabbay in
An overview of fibred semantics and the combination of logics. In F. Baader
and K. Schulz, editors, Frontiers of Combining Systems, pages 1-55. Kluwer
Academic Publishers, 1996,
where he argues that this collapse really happens. His argument, however,
uses the fact that the deduction theorem for both classical and
intuitionistic implications hold in the combined logic. Of course, if you
formulate your deductive systems in such a way that the deduction theorem is
a rule by itself then the collapse indeed occurs, but if it comes only as a
metatheorem as in a common Hilbert style axiomatization then it is not the
case. The proposal of Luis Fariñas del Cerro and Andreas Herzig is in fact a
restricted Kripke semantics for a logic combining classical and
intuitionistic connectives but in a much more restricted way, so as to cope
with Gabbay's idea of collapse, by constraining the scope of application of
some axioms.

We are also writing a short paper on this fibred classical + intuitionistic
logic, but again it is not yet finished.

Of course, I shall be happy to send to anyone interested copies of these two
papers-to-be as soon as they are ready.

Carlos Caleiro

Carlos Caleiro
Centro de Lógica e Computação
Departamento de Matemática
Instituto Superior Técnico
Av Rovisco Pais, 1049-001 Lisboa

tel: (+351) 218417138
fax: (+351) 218417048
email: ccal at math.ist.utl.pt
www: http://www.math.ist.utl.pt/cs/ccal.html

More information about the FOM mailing list