Intuitionistic logic

Another interesting attempt to generalize from classical logic that denies the Law of Bivalence is that of the Intuitionists, who deny the applicability of the Law of Excluded Middle: ∖-p v -∣p.

tic logic—and then, by an application of the second form of DN—fromderive p—

this is what is denied by the intuitionists.) Indirect proof only works if you assume that each proposition has a determinate truth value in advance of being discovered or invented by human ingenuity; then p must be either true or false, so that proving its negation false leaves its truth as the only other option. If bivalence is rejected, then to have proved -∣p false is to have provedbut this is NOT the same as having established p directly.

Predicate Logic only three of the four forms of Quantifier Negation are permissible:

But the following form is not valid:

From -³ VxΦx, derive Ξx-∣Φx.

EXERCISE 24.5

Prove that the first three forms of QN above are derivable without assuming DN.

above. As a result, if we take all the points x that are indistinguishable from 0, and call this the infinitesimal neighbourhood of 0, Σ(0), then this does not reduce to the set of points containing only 0. Thus if we call all those numbers that are so close to 0 as to be indistinguishable from it infinitesimals, then from the fact that

^[1] John Bell, A Primer of Infinitesimal Analysis (Cambridge: Cambridge UP, 1998), pp. 6-7. This inference would be provable if we allowed the form of QN that was declared invalid

As mentioned above, Heyting gave a set of axioms for Intuitionistic Logic (hereafter IL). These can be recast as a natural deduction system like the one in this book.

Now Heyting’s system of axioms is provably equivalent to this set of rules minus the converse DN rule: MP, CP; Conj, Simp; Disj, DS; and RA. To this set we may now add UI, UG, EI, EG; this set constitutes IL. What then is the status of this system vis-a-vis classical logic?

One way to regard IL is as a generalization of classical logic; on this reading it stands in the same relation to classical logic as non-Euclidean Geometry stands to Euclidean Geometry. In each case we drop one classical axiom; in each case, too, the resulting sys­tem can be proven to be consistent in the sense that the classical system can be modelled in it, so that the non-classical system is consistent if the classical one is. But then the meaning of at least some of the statement operators must be different. Just as the points and lines of non-Euclidean Geometry are implicitly defined by the four axioms of that geometry (without the parallel postulate), and so do not necessarily mean the same thing as in classical geometry, so ‘and,’ ‘not,’ ‘if...then...,’ and ‘or’ will also have slightly altered meanings without the principle of bivalence. This is particularly true of negation, since the law of double negation does not hold in the intuitionists’ system; and as we have seen, to say that a proposition is negated in the intuitionists’ sense is to say that it can be (constructively) proven that it is not (constructively) provable.

^[1] See Kurt Gδdel, “Zur Intuitionistischen Arithmetik und Zahlentheorie,” and “Eine Interpreta­tion des Intuitionistischen Aussagenkalkuls,” Ergebnisse eines mathematischen Kolloquiums, Heflt iv (1932), pp. 34-38 and 39-40; Kneale and Kneale, pp. 678-80.

regarded as an axiomatic theory of provability by such constructive methods. But then, as the Kneales astutely observe, “Heyting’s calculus is not a system of logic in the strict sense,” since “it presupposes classical logic, and has only been mistaken for an alter­native logic because of the intuitionists’ unfortunate custom of talking of theorems as statements of provability” (Development, p. 681).