FOM: intuitionist propositional logic

[David J. Pym]

Re: Robert Black's enquiry.

Two relevant references are by Gabbay:

1.Dov M.Gabbay. Investigations in Modal and Tense Logics with Applications.
Synthese Library, Vol. 92, D. Reidel, 1976;

2.Dov M. Gabbay. Semantical Investigations in Heytings's Intuitionistic Logic.

Synthese Library, D. Reidel, Vol. 148, 1981.

The collapse of intuitionistic logic is widely stated but perhaps
less widely understood in detail.  It is really a result about the sermantics
of proofs: a categorical model of IL's proofs collapses to a boolean
algebra in the presence of  [[ p ]]  iso [[ ~~p]] . However,  it is
unclear that a this iso is well-motiviated by a direct consideration
of classical vs. intuitionistic proofs. Now, classical proofs can be
represented by Parigot's lambda-mu-calculus and in categorical
models of this system, a certain class of fibrations of models of IL's
proof theory (which are so included in this semantics) over
a ``structural category'' plus some conditions,  the relationship
between the interpretations of  [[ p ]]  and [[ ~~p]] is a retraction.
In this setting, two forms of (classical) disjunction are available:
one is inherited from Gentzen's LJ and one from LK. Now,  if
two forms are required to have isomorphic interpretations, then
the semantics collapses to a family of boolean algebras. Various
completeness properties can be obtained.

Three papers on this topic (one on semantics, two on proof theory)
can be found at http://www.dcs.qmw.ac.uk/~pym/Paperspage/recent.html .

Finding a completeness result wrt to the unanalysed notion  of
constructive validity  seems a slippery aim.

Best wishes,

David Pym

---------------------------------------------------------------------------------------

Dr. David J. Pym,
Reader in Logic and EPSRC Advanced Fellow,
Department of Computer Science,
Queen Mary & Westfield College,
University of London,
London E1 4NS, England, U.K.

Tel: +44 (0) 171 975 5237   Mob: +44 (0) 370 941 725
Fax: +44 (0) 181 980 6533   Room: CS/426
Email: pym at dcs.qmw.ac.uk    WWW: http://www.dcs.qmw.ac.uk/~pym
----------------------------------------------------------------------------------------




Robert Black wrote:

> Can anyone tell me where I can find information on propositional logics
> intermediate between intuitionist logic and classical logic? As is well
> known, adding excluded middle or double-negation elimination collapses
> intuitionist logic into classical logic.  But we can add to intuitionistic
> propositional logic, for example, the schema (p -> q) v (q -> p) and get
> something strictly stronger, but still weaker than classical logic.  How
> many such intermediate logics are there, and how are they ordered?
>
> My interest is due to the following question:  can we use facts about these
> intermediate logics to get a completeness proof for intuitionistic
> propositional logic which, unlike e.g. completeness proofs relative to
> Kripke semantics, just uses the unanalysed intuitive concept of
> constructive validity? (e.g. to take the ideal case if there were some
> propositional formula which held in every logic strictly stronger than
> intuitionist logic but which was obviously constructively invalid, we would
> thereby have a completeness proof for intuitionist propositional logic
> without needing an analysis of constructive validity.) Or is there some
> obvious reason why nothing like this can be done?
>
> Robert Black
> Dept of Philosophy
> University of Nottingham
> Nottingham NG7 2RD
>
> tel. 0115-951 5845