###
Intuitionistic Logic +

The dispute between supporters of classical and intuitionistic logic revolves around application of
the law of excluded middle (LEM) to formulas containing object variables.
Propositional logic can be considered a part of the mathematics of finite sets because of
availability of finite models using truth tables. Thus, LEM for propositional formulas is not really
a target of intuitionistic criticism of classical logic.
The classical assumption that every propositional atom (symbol) is either true or false but not both
translates into decidability of propositional atoms in terms of proof theory.

First-order intuitionistic logic with decidable propositional atoms is supposed to be a system somewhat
acceptable by both camps: classical and intuitionistic. On one hand, it is fully classical in
its propositional part. On the other hand, LEM, double negation elimination and their variants
are not extended onto statements about infinite collections. Properties of intuitionistic logic
with decidable propositional atoms are investigated in my paper
*Intuitionistic Predicate Logic with Decidable Propositional Formulas* published in
*Reports on Mathematical Logic*, 42(2007).

This approach to extending intuitionistic logic can be generalized in order to cover the entire
space between intuitionistic and classical logics.
One can consider extensions of intuitionistic logic defined by sets of decidable (classical) predicate symbols.
My article on this topic called *Classicality as a Property of Predicate Symbols*
appears in the proceedings of *6th Panhellenic Logic Symposium*.

Copyright © 2008 Alexander Sakharov
Need to relax? Try brain teasers. I would recommend those marked 'cool'.