GUSTAVO FERNÁNDEZ DÍEZ

FIVE OBSERVATIONS CONCERNING THE INTENDED MEANING

OF THE INTUITIONISTIC LOGICAL CONSTANTS

(Received: 22 September 1999; revised: 24 March 2000)

ABSTRACT. This paper contains five observations concerning the intended meaning of
the intuitionistic logical constants: (1) if the explanations of this meaning are to be based
on a non-decidable concept, that concept should not be that of ‘proof’; (2) Kreisel’s ex-
planations using extra clauses can be significantly simplified; (3) the impredicativity of the
definition of → can be easily and safely ameliorated; (4) the definition of → in terms of
‘proofs from premises’ results in a loss of the inductive character of the definitions of ∨ and
∃; and (5) the same occurs with the definition of ∀ in terms of ‘proofs with free variables’.

KEY WORDS: intuitionistic semantics, logical constant, construction, proof, intended

meaning

1. I NTRODUCTION

The attempts to make the intended meaning of the intuitionistic logical

constants explicit have lead to a number of ‘informal explanations’. The
accuracy of these explanations is not very important for the actual practice
of intuitionistic mathematics, which relies mainly on intuitive understand-
ing and previous usage, but it is essential from a philosophical point of
view:
(. . . ) it is therefore necessary, in the first place, to inquire whether these explanations of
the logical constants are coherent or not, whether they confer intelligible meanings on
them; if this question (. . . ) has to be answered negatively, the whole conception, inherent
in intuitionistic mathematics, of how mathematical statements are to be given meaning will
have been shown to be defective. (Dummett, 1977, p. 390)

The idea of what such explanations should look like is perhaps best repre-
sented by the usual definition of intuitionistic disjunction:

DEFINITION 1. A proof of p ∨ q is either a proof of p or a proof of q.

This definition combines three qualities which make it particularly at-

tractive: (a) it is very simple; (b) it makes transparent that aspect of the
intuitionistic ∨ which constitutes its most salient difference with its clas-
sical counterpart (indeed, in classical mathematics we often prove p ∨ q

Journal of Philosophical Logic 29: 409–424, 2000.

© 2000 Kluwer Academic Publishers. Printed in the Netherlands.
410 GUSTAVO FERNÁNDEZ DÍEZ

without proving either p or q); and (c) it has an ‘inductive character’, that
is: the meaning of a complex sentence is given in terms of the meanings of
its constituents, sentences logically simpler than it.
Unfortunately, when we try to reduce the other logical constants – and,
in particular, →, ¬ and ∀ – to a schema such as Definition 1, we encounter
serious difficulties. In the present paper, I shall make five observations con-
cerning these difficulties and the attempts that have been made to overcome
them.

2. T HE CONDITIONAL

I would like to start by looking at the definition of the intuitionistic con-

ditional. Of the various versions which currently appear in the literature,
the following is one of the simplest, taken from a well-known textbook on
constructivism:
DEFINITION 2. A proof of p → q is a construction that permits us to
transform any proof of p into a proof of q.
(Troelstra and van Dalen, 1988, p. 9). In this and the subsequent quotations
I always use my choice of notation.
This definition resembles the previous one for intuitionistic disjunction,
but it is based on a peculiar appeal to any – arbitrary – proof of p, and this
fact makes it defective in two ways that the other is not. In the first place, it
is impredicative: the construction which is being defined and which proves
p → q must be able to transform any possible proof of p into a proof of
q; as no boundary is put on the complexity of those possible proofs of p,
they could include some complicated roundabout proofs which involved
reference to the sentence p → q itself, and hence to the same proof being
defined. In sum: the definition of a proof of p → q appeals to a totality of
proofs, with some of which the very proof of p → q could be intimately
related.
In the second place, this definition of → has the effect of converting
the proof relation induced into a non-decidable relation. Indeed, it is quite
possible that a given construction c is able to transform every proof of p
into a proof of q, but without being obviously so; and in such a case, the
fact that c does transform every proof of p into a proof of q will ask for
a separate proof. As long as we cannot provide this additional proof, we
will be unable to decide whether, according to Definition 2, the original
construction c is a proof of p → q or not.
However, it is extremely unnatural – both intuitionistically and classi-
cally – to say that a construction might be a ‘proof’ of a given sentence,
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 411

but that we cannot decide whether that is the case or not; and that we need
a further proof, which requires true ingenuity to find, in order to establish
that c is indeed the ‘proof’ of the sentence in question.
I shall examine the undecidability problem first, and leave the impred-
icativity, less urgent one, for later.

3. A FUNDAMENTAL DICHOTOMY

The fact that Definition 2 induces a non-decidable relation is only the

particular case of a general dichotomy, familiar from computer program-
ming: the dichotomy between a concrete detailed mathematical construc-
tion which performs a certain task, and that additional construction which
proves that the first one does indeed the task in question. Very often we ten-
tatively define a mathematical construction with the purpose of operating
in a particular way, but once the construction is completely defined, it is not
at all obvious that it will always behave in the way it was expected to. In
such cases we must devise a separate proof that our completed construction
does the job required, and the resulting proof is a different object from the
original construction itself.
Sundholm has stressed the distinction between a mathematical con-
struction as a finished object, and the act or process of constructing it (a
distinction embedded in Martin-Löf’s type theory, cf. Sundholm (1983,
pp. 164–168); (1994, pp. 144–148), Martin-Löf (1984, 1994) and Nord-
ström, Petersson and Smith (1990)). Moreover, Sundholm maintains that:
The proof that the construction does what it is supposed to do is not itself a construction
object, but rather the act of proof/construction whereby the construction object is given.
(Sundholm, 1994, p. 148, footnote)
For any proposition, be it an implication, a conjunction or what have you, it must
be possible to recognise its proof-objects as such (. . . ). This property has to be ensured
through the way in which the relevant proof-object is given (the act of proof/construction).
(Sundholm, 1994, p. 148, his italics)

However, it seems to me that this cannot be always the case. For example,
let us consider a construction, c, which enables us to find, for each positive
integer n, a prime number larger than n which is of the form 4m − 1 for
some m (a special case of Dirichlet’s theorem):

take the smallest divisor of 4n! − 1 which is of the form

4m − 1 for some integer m.

It is very easy to prove that c indeed does the job required, i.e.: that the
result of applying c to a positive integer n is always a number which is
412 GUSTAVO FERNÁNDEZ DÍEZ

prime, larger than n and of the form 4m − 1 for some m. But this fact is
not completely obvious, and the mere description of c does not reveal it:
the proof that establishes it is a very different construction from c itself.
Moreover, sometimes an open mathematical problem remains unsolved,
not because we lack the basic construction which does or is supposed to
do the job required, but because we lack the proof that such a construction
does that job indeed. An example is Goldbach’s conjecture: the construc-
tion for decomposing an arbitrary even number n into a sum of two primes,
is a matter of finite routine searching over the numbers smaller than n.
Insofar as it has been possible to test such a construction, it worked; but
we cannot prove that it will work in general.
Hence we have a very simple construction which appears to transform
all proofs of ‘n is even’ into proofs of ‘n is a sum of two primes’ (showing
two such primes), but we cannot decide whether it does so in general, for
all natural n, and because of that we cannot decide whether it will be,
according to Definition 2, a proof of ‘if n is even, then n is a sum of two
primes’ for every n.
Such a situation, by the way, is quite different from those others where
we even lack the basic construction which is supposed to do the job re-
quired. For example, in the case of the twin prime conjecture, we simply
do not have any candidate for a construction which appeared to transform
any positive integer into a pair of twin primes bigger than it, and behaved
so, e.g., when tested against relatively small numbers.

4. K REISEL’ S EXTRA CLAUSES

In order to ensure the decidability of the proof-relation induced, Kreisel

proposed the introduction of an ‘extra clause’ in the definition:
DEFINITION 3. A proof of p → q is a pair of constructions (c1 , c2 ),
where c1 proves that c2 transforms any proof of p into a proof of q.
(Cf. Kreisel, 1961, p. 107, footnote; 1962, p. 205; 1965, p. 128). Hence, if
we have a construction that appears to transform all proofs of p into proofs
of q, but we are unable to prove this fact, we can readily conclude that we
do not, according to this definition, have a proof of p → q.
In turn, Kreisel’s definition is not inductive: the proof of p → q is
defined not only in terms of proofs of p and q, but also of an extra proof,
c1 , of a much wider scope. This loss of the inductive character significantly
reduces the explanatory power of the definition.
At first, Kreisel’s extra clauses were received largely as a straight im-
provement (cf., e.g., Troelstra, 1969, p. 5; 1977, p. 977, van Dalen, 1973,
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 413

p. 24, or Dummett, 1977, p. 399); but after some debate (e.g., Prawitz,
1977, p. 27, Sundholm, 1983, pp. 153–161, Weinstein, 1983, pp. 263–
266), a number of authors abandoned them, reverting henceforth to simpler
formulations such as Definition 2 (e.g., van Dalen, 1983, p. 166; 1986,
p. 231, Troelstra and van Dalen, 1988, p. 9):
It must be pointed out however that the decidability of the proof-relations has been critized
and that the ‘extra clauses’ are not universally accepted. (van Dalen, 1986, p. 232)

This debate was strongly influenced by the idea that the constructive
meaning of mathematical sentences has to be given in terms of proof condi-
tions as opposed to truth conditions, an idea which is deeply rooted among
intuitionists (Heyting, 1956, p. 97, Kreisel, 1962, p. 201, Dummett, 1977,
p. 12). However, it seems to me that, if we want to dispense with Kreisel’s
extra clauses and preserve the inductive structure of the definition, then we
must change the concept of ‘proof’, at the core of that inductive structure,
and replace it by a different concept.

5. T HE OPERATIONAL INTERPRETATION

As a matter of fact, it is not difficult to find such a replacement. For exam-

ple, we could say that a construction c ‘performs’ a given sentence p when
the application of c carries out those constructive operations that the sen-
tence p claims to be possible. Thus, if p says ‘every positive integer has a
bigger prime of the form 4m−1’, then the application of the corresponding
construction c to a positive integer n should always yield a number which
is prime, bigger than n and of the form 4m − 1 for some m. This type
of interpretation is very similar – if not identical – to Kleene’s concept of
realizability, but I shall call it here ‘the operational interpretation’.
In the case of an intuitionistic conditional, this definition would read:

DEFINITION 4. A construction c performs p → q when it transforms

every construction c which performs p into a construction which per-
forms q.

This clause has exactly the same structure as Definition 2, and the relation
induced, which, in this case, is the ‘performing relation’, is indeed a non-
decidable relation as well. However, in the present case, there is no paradox
in the fact that the performing relation turns out to be undecidable. As a
matter of fact, here we draw a clear distinction between the construction c
which performs p → q, and a proof that could be supplied, showing that
c in effect performs p → q.
414 GUSTAVO FERNÁNDEZ DÍEZ

Whether it is intuitionistically acceptable to have a non-decidable con-

cept at the core of the semantic definition, is a very deep issue which I
cannot attempt to settle here. I do not even have a determinate opinion
myself. My contention is (observation number 1) that, if we choose to have
a non-decidable concept, in order to preserve the inductive structure of the
semantic definition – as some authors do –, then such a concept should not
be that of ‘proof’, but one more according to its non-decidable character.

6. K REISEL’ S INTERPRETATION REVISITED

Besides, the operational interpretation can help us simplify Kreisel’s defi-

nition of the conditional in a significant way: according to Kreisel’s inter-
pretation, in a proof (b1 , b2 ) of a nested conditional sentence such as

(p → q) → (r → s),

the second component b2 is required to transform every pair (c1 , c2 ) which

proves p → q into a corresponding pair (d1 , d2 ) which proves r → s. But
a moment’s reflection shows that, as a matter of fact, it is enough that b2
transforms every construction which performs p → q into a construction
which performs r → s. And then, if the extra clause b1 proves that this
is really the case, the transformation of the other extra clauses will follow
quite trivially.
Indeed, let us suppose that b2 transforms every construction which per-
forms p → q into a construction which performs r → s; and let b1 be
a proof of this fact. Let us also assume that p, q, r, and s are all atomic
sentences, so that there is no need of further extra proofs: if a construction
performs p, q, r, or s, this fact must be apparent, so it immediately qualifies
as a proof of it by all standards.
Then, if we are supplied with a ‘full’ proof (c1 , c2 ) of p → q, we can
use b2 to transform c2 into a construction d2 = b2 (c2 ) which performs
r → s. And the proof that d2 is indeed such a construction will follow at
once from c1 , which ensures that c2 performs p → q, and our previous
proof b1 , which ensures that the result of applying b2 to a construction
performing p → q is a construction performing r → s.
This suggests (observation number 2) that Kreisel’s requirement of the
extra clauses is not in essence an inductive requirement, which demands to
be placed at each step of the inductive definition, but rather, a direct one,
which demands to be placed on the top of a previous definition, such as the
operational interpretation, which is inductive itself.
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 415

This observation was inspired to me by a question posed on this respect,

long ago, by Kreisel himself:
There is an additional distinction which has so far not been formally necessary, but which
is probably important, for example in the explanation of implication (or universal quantifi-
cation). When we think of the pair (b1 , b2 )
b1 proves the identity : for variable c, if c proves p, then b2 (c) proves q,
b2 is a genuine function or operation, while b1 recognizes that b2 satisfies the condition
stated: thus, b1 is a judgement. But similarly, since in general both the arguments c and
the values b2 (c) of b2 are such pairs, say c = (c1 , c2 ) and b2 (c) = (d1 , d2 ), should
the function d2 depend both on c2 and c1 (or only on c2 )? (Kreisel, 1970, pp. 145–146,
endnote)
He does not give an explicit answer to his own question, nor has he devel-
oped this point later – at least not to my knowledge.
If I am correct – in which case the answer to Kreisel’s question is def-
initely ‘only on c2 ’ –, the natural way to re-formulate Kreisel’s definition
of the conditional would be:

DEFINITION 5. A proof of p → q is a pair of constructions (c1 , c2 ),

where c1 proves that c2 performs p → q.

Or more in general,

DEFINITION 6. A proof of a sentence p is a pair of constructions (c1 , c2 ),

where c1 proves that c2 performs p.

7. T HE IMPREDICATIVITY OF →

It is time to go back to the impredicativity problem. We noticed that the de-

finition of a proof of p → q referred to arbitrary proofs of p, and that some
of those proofs could be roundabout proofs, in which the very proof of
p → q played a role. This problem does concern Kreisel’s definition, and
the operational interpretation as well, insofar as there could be roundabout
constructions which perform p on the basis of a mid-step performance of
p → q.
The problem is substantially ameliorated, however, if we consider that
in virtually all intuitionistic proofs of conditional sentences such as p →
q, the only property of the possible proofs of p which is employed in the
derivation of q is precisely that of being a proof of p. Hence, the transfor-
mation of the proofs of p does not depend on the internal structure of those
proofs, except for the requirements that the inductive definition places on
416 GUSTAVO FERNÁNDEZ DÍEZ

them, according to the logical form of p (for example, if p is a disjunction,

then any proof of p must include a proof of one of the disjuncts, and the
subsequent proof of q might very well depend on which disjunct is the one
included).
However, as it happens, the only notable occasion in which all possible
proofs of the antecedent were classified and transformed according to its
internal structure and beyond the requirements that the inductive definition
places on them, is Brouwer’s attempted proof of the bar theorem, which,
as we know, is incorrect and no way has been found to correct it preserving
its original form (cf., e.g., Brouwer (1927), and for a discussion Dummett,
1977, pp. 94–104).
This suggests (observation number 3) a very simple way in which we
could safely ameliorate the impredicativity from our two previous explana-
tions of the intuitionistic conditional: to replace the occurrence of the word
‘transforms’ (or ‘transform’) in each of them, by e.g. ‘extends’ (‘extend’).
And the fact that the intuitionistic conditional has never been successfully
used, in mathematical practice, in other than this restricted sense, probably
means that such is the best way to characterize its intended interpretation.
In fact, Heyting’s original definitions of the intuitionistic conditional
were very much on these lines:
p → q represents then the intention of a construction which, from each demonstration of
p, leads to a demonstration of q. (Heyting, 1934, p. 17)
The implication p → q can be asserted, if and only if we possess a construction c,
which, joined to any construction proving p (supposing that the latter be effected), would
automatically effect a construction proving q. In other words, a proof of p, together with
c, would form a proof of q. (Heyting, 1956, p. 98. My italics in ‘joined’)

8. P ROOFS FROM PREMISES

A yet further refinement on the previous proposal is to define a proof of

a conditional sentence p → q directly as a ‘proof of p with premise –
or hypothesis – q’. This idea is in fact the oldest one, as it corresponds
to Kolmogorov’s interpretation of the intuitionistic conditional in terms of
mathematical problems:
(. . . ) p → q is the problem of ‘solving the problem q, supposing that the solution to p is
given’. (Kolmogorov, 1932, p. 59)

The same idea is the motivation behind Gentzen’s rule of →-introduction

(which he considered a meaning definition, cf. Gentzen (1935, pp. 78–80)),
and has been treated since then as a faithful explanation of the meaning of
the intuitionistic conditional, e.g., by Sundholm (1986, p. 490), Martin-Löf
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 417

(1985, p. 45; 1987, pp. 410–412), or Bridges and Richman: “the statement
p → q means that q holds under the assumption that p holds” (Bridges
and Richman, 1987, p. 11).
The idiosyncrasies of this type of interpretation have been widely ig-
nored, but it is quite remarkable that, prima facie, under this definition the
decidability problem seems to disappear completely: indeed, there is no
reason in principle why we should not be able to recognize a ‘proof of
q with premise p’ when we see one, provided that we already know the
intuitionistic meanings of p and q.
However, this gain of decidability is again not without cost. To start
with, once we agree to define the proof of any conditional sentence p → q
as a proof of q with premise p, we must immediately re-define all the other
logical constants in terms of a finite set of premises. For instance, in the
case of a sentence such as

p → (r → (s ∨ t)),

the proof of the disjunction s ∨ t should be given in terms of the two

premises p and r.
But when we try to carry out such a re-definition, we run into the most
unexpected problem. Indeed, we cannot admit the definition:

DEFINITION 7. A proof of p ∨ q from a set P of premises is either a

proof of p from premises P , or a proof of q from premises P ,

because that would legitimate the inference

r → (s ∨ t) ` (r → s) ∨ (r → t),

which is not intuitionistically valid (i.e., not deducible in the intuitionistic

propositional calculus).
Then, the only possible alternative seems to be:

DEFINITION 8. A proof of p ∨ q from a set P of premises is a proof

from premises P that either a proof of p or a proof of q can be constructed.

But this definition is not inductive, as there is no decrease of logical com-

plexity in the definiens.
Similarly, we cannot admit a definition of the intuitionistic existential
quantifier such as:

DEFINITION 9. A proof of ∃xA(x) from a set P of premises consists in

a construction c in the domain plus a proof from premises P of A(c),
418 GUSTAVO FERNÁNDEZ DÍEZ

because that would invalidate the intuitionistically accepted inference

∀x(A(x) → B(x)) ` ∃xA(x) → ∃xB(x);
indeed, the transformation of a proof of ∃xA(x) into a proof of ∃xB(x)
will, in general, depend on the particular object c which the first proof
provides as an instantiation (this point is made by Dummett (1977, pp. 14–
15, arguing against an explanation akin to Definition 9)).
Then, the only possible alternative is:

DEFINITION 10. A proof of ∃xA(x) from a set P of premises is a proof

from premises P that an object c in the domain can be constructed, and a
proof provided that A(c),

which as before is not an inductive definition.

As we can see (observation number 4), although the appeal to ‘proofs
from premises’ in the definition of the intuitionistic conditional appears
to ensure the decidability of the proof relation, it has also the undesired
effect of collapsing the inductive structure of the definition. This is similar
to what happened with Kreisel’s extra clauses, except for the striking fact
that here the collapse takes place exactly in the definition of disjunction
and the existential quantifier.
To be sure, it is easy to see that, in particular, the definition of the
universal quantifier in terms of proofs from premises does not face the
same problem; but for showing this we first have to examine the usual
definition of the intuitionistic ∀.

9. T HE UNIVERSAL QUANTIFIER

Of the various definitions of the intuitionistic ∀ that can be found in the

literature, the following is one of the simplest ones, analogue to Definition
2 for the conditional:

DEFINITION 11. A proof of ∀xA(x) is a construction which transforms

any construction c in the domain into a proof of A(c).

If the domain of interpretation is non-decidable, this definition is supple-

mented accordingly:

DEFINITION 12. A proof of ∀xA(x) is a construction which transforms

any proof that a given construction c belongs to the domain, into a proof
of A(c).
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 419

(Cf. Troelstra and van Dalen (1988, p. 9).) In either case, the definition
induces a non-decidable relation, just as Definition 2 did, and admits either
the introduction of Kreisel’s extra clause (which will make it decidable,
but non-inductive), or, alternatively, the replacement of its central concept
by one akin to ‘performing’ (which will preserve inductiveness but not
decidability). The way to carry out both things is straightforward. And
the simplification of Kreisel’s definition on the basis of the operational
interpretation (proposed in Section 5) can be straightforwardly extended
to this case, too.
Then, if we want to adapt this definition to the case of an arbitrary set
of premises P , the two available options:
DEFINITION 13. A proof of ∀xA(x) from premises P is a construction
which transforms any construction c in the domain into a proof of A(c)
from premises P
and
DEFINITION 14. A proof of ∀xA(x) from premises P is a proof from
premises P that we can transform any construction c in the domain into a
proof of A(c),
are clearly equivalent in meaning. In particular, from a proof from premises
P that we can transform each c into a proof of A(c), it is very easy to
obtain a method which transforms each c into a proof from premises P of
A(c): all we have to do is to apply the previous proof to each given c. And
the implication in the other direction is even more obvious.
This means that the definition of → in terms of proofs from premises
results in a decidability problem for the subsequent clauses for ∨ and ∃,
but not for that corresponding to ∀.
On the other hand, it is plain to see that formulations such as 13 and 14
do not, in turn, resolve the decidability problem inherent to the definition
of ∀ itself. And the natural question is whether there is an analogous way
to confront this problem.

10. P ROOFS WITH FREE VARIABLES

The answer is ‘yes’: there is a most peculiar way which appears to preserve
the decidability in the definition of ∀, apparently without inductive loss,
and which runs entirely parallel to the appeal to proofs from premises in
the case of the conditional:
DEFINITION 15. A proof of ∀xA(x) is a proof of A(x) with a free
variable x.
420 GUSTAVO FERNÁNDEZ DÍEZ

This does not coincide with Kolmogorov’s original formulation (which

explicitly refers to a “general method for the solution of A(x) for each
particular value of x”, cf. Kolmogorov (1932, p. 60), but it corresponds to
Gentzen’s rule of ∀-introduction (Gentzen, 1935, p. 78), and can be found
in other authors such as Sundholm (1986, p. 491) and Martin-Löf (1985,
p. 54; 1987, pp. 410–412).
Dummett has critized this definition on the grounds that it does not
account for the soundness of the principle of mathematical induction: in
general, a proof of ∀xA(x) from A(0) and ∀x(A(x) → A(x + 1)) will not
be a free-variable proof of A(x), but a method to transform each natural
number n into a proof of A(n), the method being an iterating application
of modus ponens (Dummett, 1977, p. 14). However, this might be taken
simply as evidence that induction is not a logical rule, which can be ex-
tracted right away from the intuitionistic meaning of the logical constants,
but a genuinely mathematical principle.
In any case, the definition faces a problem completely analogous to
that of its respective attempt for the conditional in terms of proofs from
premises. To start with, it forces us to re-define all the other logical con-
stants in terms of a finite set of free variables, something which has not
been tried in detail before. But when we try to do that (observation num-
ber 5), we lose the inductive character of the corresponding definitions of
disjunction and the existential quantifier.
Indeed, a proof of ∀x(A(x) ∨ B(x)) will not be, in general, either a
free-variable proof of A(x) or a free-variable proof of B(x), but rather, a
free-variable proof of the disjunction A(x) ∨ B(x); and similarly, a proof
of, say, ∀x∃yA(x, y), will not usually consist in the production of an object
c plus a proof of A(x, c) with a free variable x, but rather, in a free variable
proof of ∃yA(x, y).
On the other hand, it is important to notice that the definition of → in
terms of ‘proofs with free variables’ (or in terms of ‘proofs with premises
and free variables’) does not constitute any problem: in particular, from
a given method to transform all the free-variable proofs of p into free-
variable proofs of q, we can always obtain a ‘uniform’ free-variable proof
of p → q, the only (trivial) modification possibly needed being that, if the
free-variable proof of p uses a particular sequence of free variables, the
free-variable proof of q which results after the application of the method is
rearranged so that it uses exactly the same sequence. And the implication
in the other direction is even more obvious.
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 421

11. ATOMIC SENTENCES AND THE REST

The treatment of atomic sentences is easy, as intuitionistically we require

that the basic properties of the interpretation be such that, for any given
construction c in the domain (plus a proof that c belongs to it, if it is non-
decidable), we already know how to recognize a proof d that c satisfies any
of them. Hence d will qualify as a proof of the corresponding sentence,
and, at the same time, as a construction which performs it. And similarly
for relations and functions.
The intuitionistic negation is defined as a conditional sentence which
has as consequent a basic self-evident absurdity (a construction which is
obviously impossible to carry out), and as antecedent the sentence negated.
Hence, all that has been said about the conditional applies to negation
directly.
Conjunction is a straight ‘sum’ of the proofs (or performing construc-
tions) corresponding to each conjunct: its definition does not create any
problem at all.
Next, the explanation of the intuitionistic disjunction, which has been
already touched on (Definition 1), does not pose a decidability problem,
nor does it require the introduction of Kreisel’s extra clauses, unless it is
broadened so as to read, e.g.:

DEFINITION 16. A proof of p ∨ q is either a proof of p, or a proof of

q, or an effective procedure which enables us to find either of them,

in which case it will stand in a very similar position to the definition of the
conditional.
The definition of the intuitionistic existential quantifier has also been
mentioned, indirectly. It resembles that of the disjunction in many aspects.
It is usually given as:

DEFINITION 17. A proof of ∃xA(x) is a pair of constructions (c1 , c2 ),

where c2 is a construction in the domain and c1 proves A(c2 ).

Or, if the domain of interpretation is non-decidable:

DEFINITION 18. A proof of ∃xA(x) is a triple of constructions (c0 , c1 ,

c2 ), where c0 proves that c2 belongs to the domain, and c1 proves A(c2 ).

In either case, it does not pose a decidability problem, unless we permit,

as before, that an effective procedure for finding a pair (c1 , c2 ) or a triple
(c0 , c1 , c2 ) directly qualifies as a proof of ∃xA(x).
422 GUSTAVO FERNÁNDEZ DÍEZ

And finally, the way to extend the definition of disjunction to the oper-
ational interpretation is straightforward:

DEFINITION 19. A construction performs p ∨ q when either it performs

p or it performs q.

And as for the existential quantifier, it is in the spirit of the operational

interpretation that the reference to c1 is eliminated:

DEFINITION 20. A construction c performs ∃xA(x) when some other

construction performs A(c);

and thus a proof that c performs ∃xA(x) would require the production of a
concrete construction d which performed A(c).
We can now see that the two groups of intuitionistic logical constants:
{→, ¬, ∀} and {∨, ∃} are really opposed to each other: →, ¬ and ∀ pose a
decidability problem, which ∨ and ∃ normally do not; and the attempts to
resolve it produce a loss of inductiveness either in the definitions of →, ¬,
and ∀, or in those of ∨ and ∃.
What conclusion, if any, can be drawn from this last – unnumbered –
observation, I leave to others to decide.

ACKNOWLEDGEMENTS

The contents of this paper, in somewhat different form, are part of my

doctoral dissertation at the London School of Economics, written under the
direction of Professor Colin Howson, and with the unofficial – but invalu-
able – advice of Professor Moshé Machover. The research was supported,
at various stages, by the British Council, the British Academy, the Spanish
Ministry of Education and Caja de Ahorros del Mediterráneo. I would
like to thank as well an anonymous referee of the Journal of Philosophical
Logic, for helpful comments and suggestions on the earlier draft.

R EFERENCES

Bridges, D. S. and Richman, R. (1987): Varieties of Constructive Mathematics, Cambridge

University Press, Cambridge.
Brouwer, L. E. J. (1927): Über Definitionsbereiche von Funktionen, Math. Ann. 97, 60–
75. English extract in J. van Heijenoort (ed.), From Frege to Gödel: A Source Book
in Mathematical Logic, 1897–1931, Harvard University Press, Cambridge, MA, 1967,
pp. 457–463.
 INTENDED MEANING OF THE INTUITIONISTIC LOGICAL CONSTANTS 423

van Dalen, D. (1973): Lectures on intuitionism, in A. R. D. Mathias and H. Rogers (eds.),

Cambridge Summer School of Mathematical Logic, Springer, Berlin, pp. 1–94.
van Dalen, D. (1983): Logic and Structure, 2nd. rev. edn, Springer, Berlin.
van Dalen, D. (1986): Intuitionistic logic, in D. Gabbay and F. Guenthner (eds.), Handbook
of Philosophical Logic, Vol. III, Reidel, Dordrecht, pp. 225–339.
Dummett, M. A. E., with the assistance of R. Minio (1977): Elements of Intuitionism,
Clarendon Press, Oxford.
Gentzen, G. (1935): Untersuchungen über das logische Schliessen (I, II), Math. Z. 39,
176–210. Quoted by the English version in the Collected Papers, ed. by M. E. Szabo,
North-Holland, Amsterdam, 1969, pp. 69–131.
Heyting, A. (1934): Mathematische Grundlagenforschung: Intuitionism, Beweistheorie,
Springer, Berlin. Quoted by the French expanded edition, Les Fondements des Math-
ématiques. Intuitionnisme. Théorie de la Démonstration, Gauthier-Villars, Paris, 1955.
Heyting, A. (1956): Intuitionism: An Introduction, North-Holland, Amsterdam.
Kolmogorov, A. N. (1932): Zur Deutung der intuitionistischen Logik, Math. Z. 35, 58–65.
Kreisel, G. (1961): Set-theoretical problems suggested by the notion of potential totality,
in Infinitistic Methods: Proceedings of the Symposium of Foundations of Mathematics,
Warsaw, 2–9 September 1959, Pergamon Press, Oxford, pp. 103–140.
Kreisel, G. (1962): Foundations of intuitionistic logic, in E. Nagel, P. Suppes and A. Tarski
(eds.), Logic, Methodology and Philosophy of Science, Vol. I, Stanford University Press,
Stanford, CA, pp. 198–210.
Kreisel, G. (1965): Mathematical logic, in T. L. Saaty (ed.), Lectures on Modern
Mathematics, Vol. III, Wiley, New York, pp. 95–195.
Kreisel, G. (1970): Church’s thesis: A kind of reducibility axiom for constructive math-
ematics, in J. Myhill, A. Kino and R. E. Vesley (eds.), Intuitionism and Proof Theory,
North-Holland, Amsterdam, pp. 121–150.
Martin-Löf, P. (1984): Intuitionistic Type Theory: Notes by Giovanni Sambin of a Series of
Lectures Given in Padova, June 1980, Bibliopolis, Naples.
Martin-Löf, P. (1985): On the meanings of the logical constants and the justifications of
the logical laws, in Atti degli Incontri di Lògica Matemàtica, Vol. II, Scuola di Spe-
cializzazione in Lògica Matemàtica, Dipartimento di Matemàtica, Università di Siena,
pp. 203–281. Quoted by the reprint in Nordic Journal of Philosophical Logic 1 (1996),
11–60.
Martin-Löf, P. (1987): Truth of a proposition, evidence of a judgement, validity of a proof,
Synthese 73, 407–420.
Martin-Löf, P. (1994): Analytic and synthetic judgements in type theory, in P. Parrini (ed.),
Kant and Contemporary Epistemology, Kluwer Acad. Publ., Dordrecht, pp. 87–99.
Nordström, B., Petersson, K. and Smith, J. M. (1990): Programming in Martin-Löf’s Type
Theory: An Introduction, Clarendon Press, Oxford.
Prawitz, D. (1977): Meaning and proofs: on the conflict between classical and intuitionistic
logic, Theoria 43, 1–40.
Sundholm, G. (1983): Constructions, proofs and the meaning of the logical constants, J.
Philos. Logic 12, 151–172.
Sundholm, G. (1986): Proof theory and meaning, in D. Gabbay and F. Guenthner (eds.),
Handbook of Philosophical Logic, Vol. III, Reidel, Dordrecht, pp. 471–506.
Sundholm, G. (1994): Vestiges of realism, in B. McGuiness and G. Oliveri (eds.), The
Philosophy of Michael Dummett, Kluwer Acad. Publ., Dordrecht, pp. 137–165.
Troelstra, A. S. (1969): Principles of Intuitionism, Springer, Berlin.
424 GUSTAVO FERNÁNDEZ DÍEZ

Troelstra, A. S. (1977): Aspects of constructive mathematics, in K. J. Barwise (ed.),

Handbook of Mathematical Logic, North-Holland, Amsterdam, pp. 973–1052.
Troelstra, A. S. and D. van Dalen (1988): Constructivism in Mathematics: An Introduction,
Vol. I, North-Holland, Amsterdam.
Weinstein, S. (1983): The intended interpretation of intuitionistic logic, J. Philos. Logic
12, 57–82.

University of Murcia
Facultad de Filosofía
Apartado 4021
E-30071, Murcia, Spain
(E-mail: [email protected])