Free Intuitionistic Logic: A Formal Sketch

Abstract

The inference rule If ⊢

$$If \vdash A(t),{\text{ then }} \vdash (\exists x)A(x)$$

((1))

and its dual

$$If \vdash (\forall x)A(x),{\text{ then }} \vdash A(t)$$

((2))

are of course sound only if t in A(t) denotes something or other. So, prior to 1959, the singular terms owned by logic, be it classical logic or intuitionistic logic, were presumed to be denoting ones. The presumption was overtly made by some writers. It was not by others, and as a result many a novice must have substituted for ‘t’ in (1) – (2) a nondenoting term, thereby perpetrating a non-sequitur. But nondenoting terms do play a large role both in ordinary and in scientific discourse, and a logic that accommodates them eventually proved indispensable. One was supplied in 1959 by Jaakko Hintikka [1959], and another supplied independently and in the very same year by Theodore Hailperin and me [Leblanc and Hailperin 1959].