α ∧ β a pair (π1, π2), where π1 is a proof of α and π2 is a proof of β

α ∨ β a procedure p whose execution yields, after a finite time, either a proof of α or a

proof of β

α → β a constructive functiona f such that, for every proof π of α, f (π ) is a proof of β

¬α a constructive function f such that, for every proof π of α, f (π ) is contradiction

∀x α† a constructive function f such that, for every c ∈ D, f (c) is a proof of α(c)‡

∃x α† a procedure p whose execution yields, after a finite time, a pair (c,π ), where

c ∈ D and π is a proof of α(c)‡

† where x varies on D

‡ c is a name of c

a Heyting speaks of “general method”; I shall use throughout “constructive function” (or briefly “function”) with the same meaning.

In order to arrive at defining the meaning of (2t), we must ask how to define a proof of K α. There is no official intuitionistic answer, and there are several possibilities, according to the intended intuitive reading of K: “α is presently known by someone”, “α is known by someone at some time”, “α is presently known by the one who is considering α”, and so on. I shall choose the last reading because, on the one hand, it seems to be the most congenial to intuitionistic ideas and, on the other hand, it is equivalent to the other readings for my present purposes. Here is my proposal:

Definition 2 Whenever one is presented with a proof of α, a proof of K α is the observation that what one is presented with is a proof of α.

In the light of Definitions 1 and 2, (2t) expresses the expectation, for any proposition α, of a function f associating to every proof π of α the observation that π is a proof of α.

Now, a fundamental characteristic of proofs, as the intuitionists conceive them, is that "for them, esse est concipi", to quote Dummett's illuminating formulation.11 In other words, a proof of α is essentially what is recognized as such by an idealized knowing subject: there is no point of view from which something can be judged to be a proof of α in spite of the fact that an idealized subject who is presented with it does not judge it as a proof of α, or from which something can be judged not to be a proof of α in spite of the fact that an idealized subject who is presented with it does judge it as a proof of α. I shall call this characteristic of intuitionistic proofs their epistemic transparency; it can be expressed in the following way:

(4) A proof of α is epistemically transparent if and only if a subject who is presented with it is in a position to know that it is a proof of α.

11"[M]athematical objects […] are mental constructions […] in the sense that, for them, esse est concipi." [3, p. 7].

A little12 reflection shows that, if proofs are transparent, the function f whose expectation is expressed by (2t) does exist: by (4), for any proof π of α, if one is presented with π , one is in a position to know that π is a proof of α; so one can associate to π the observation that π is a proof of α; and this, by Definition 2, is the proof of K α required by the definition of f . Conversely, if a subject s knows, i.e. can compute, a function f associating to every proof π of α the observation that π is a proof of α, then s, when presented with a proof of α, is in a position to know that it is a proof of α. In conclusion (2t), far from saying that every intuitive truth is known, says that proofs are epistemically transparent, and is therefore obviously true; moreover, it remains true if K is read as “is known by someone at some time”, since, if α is presently known by me, then α is known by someone at some time.

Williamson [25], pp. 430–1, raises the following objection to the validity of (2t). He first argues that a proof of α → β should be conceived by intuitionists as a

function f from proof-tokens to proof-tokens "that is unitype in the sense that if p and q are proof-tokens of the same type then so are f ( p) and f (q)." Then, under the assumption that

a proof of α → K α is a unitype function that evidently takes any proof-token of α to a proof-token, for some time t , of the proposition that α is proved at t ,

he shows that, if α has not yet been decided, the function f that associates to every proof-token of α a proof-token of the proposition that α is proved at t is not unitype: if the proof-token p is carried out at t1 and the proof-token q is carried out at t2, where t1 /= t2, then f ( p) /= f (q), since the proposition that α is proved at t1 is different from the proposition that α is proved at t2. However, the quoted assumption is by no means conceptually necessary, nor is it a consequence of the general conception of proofs of conditionals as unitype functions. If we assume that a proof of α → K α is a unitype function that takes any proof-token of α to a proof-token of the proposition that α is proved (with no mention of the time at which it is proved), f is unitype.

Let us now consider (1t). It is more difficult to suggest an intuitionistic reading for it, since it is not easy to devise a clear intuitionistic sense for the possibility operator.

Here is one plausible candidate:

Definition 3 A proof of ♦α is a procedure such that its execution yields,13 after a finite time, a proof of α.

According to this explanation, (1t) expresses the expectation, for any proposition α, of a function g associating, to every proof π of α, a procedure p whose execution yields, after a finite time, the observation that what one is presented with is a proof of α. Now, if we remember that the function f whose expectation is expressed by (2t) does exist, and that f associates, to every proof π of α, directly the empirical observation that π is a proof of α, we see that also the function g exists: the procedure consists precisely in effecting the empirical observation. In conclusion, also between the content of (1t) and the intuitive content of (K) there is a substantial difference.

Found a mistake? Please highlight the word and press Shift + Enter