|
||
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.
Need to relax? Try brain teasers. I would recommend those marked 'cool'.