FOM: intuitionist propositional logic

[Robert Black]

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