Intuitionistic logic

A set of methods for proving statements which are valid from the point of view of intuitionism. In a narrow sense, intuitionistic logic means the intuitionistic predicate calculus which was formulated by A. Heyting in 1936. This calculus, which is usually formulated in the language of predicate calculus, contains all axiom schemes and derivation rules of intuitionistic propositional calculus (but for the language of predicate calculus), and, in addition, the following quantifier axioms and derivation rules. The axioms:

$$ \forall x A ( x) \ \supset A ( t) \ \ \textrm{ and } \ \ A ( t) \supset \exists x A ( x) , $$

and the two derivation rules

$$ \frac{C \supset A ( x) }{C \supset \forall x A ( x) } ,\ \ \frac{A ( x) \supset C }{\exists x A ( x) \supset C } . $$

Here $ x $ is a variable, $ t $ is a term of the language and the formula $ C $ does not contain $ x $ as a parameter.

The completeness of intuitionistic predicate calculus depends on the semantic principles that underlie the intuitionistic theory under consideration. Thus, Markov's constructive selection principle in the form

$$ \forall x ( P ( x) \lor \neg P ( x) ) \wedge \ \neg \neg \exists x P ( x) \supset \exists x P ( x) $$

is not derivable in intuitionistic predicate calculus, but is considered true in certain approaches to constructivism. Another example of this nature is the so-called uniformization principle

$$ ( \neg Q \supset \exists x P ( x) ) \supset \exists x \ ( \neg Q \supset P ( x) ) , $$

which is true in some intuitionistic interpretations and is at the same time incompatible with the constructive selection principle within the framework of the arithmetic theory supplemented by the Church thesis. The examples given show that there is no complete intuitionistic predicate calculus that could serve as a logical basis for all the intuitionistic theories in use. Depending on the semantic conventions, essentially different variants of intuitionistic logic are possible. The development of the intuitionistic theory of derivation (cf. Derivation, logical) allows one to formulate precisely many semantic problems within the framework of intuitionism. Thus, K. Gödel proved that the completeness of intuitionistic predicate calculus with respect to the intuitionistic theory of derivation implies Markov's constructive selection principle for primitive-recursive predicates. This is an argument in favour of the incompleteness of predicate calculus from the point of view of these semantics. On the other hand, there have been found intuitionistically-valid proofs of the completeness of intuitionistic logic with respect to algebraic semantics of the type of Beth or Kripke models.

References

[1]	A. Heyting, "Intuitionism: an introduction" , North-Holland (1970)
[2]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)

References

[a1]	M.A.E. Dummett, "Elements of intuitionism" , Oxford Univ. Press (1977)