Acknowledgments
This work was supported by Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) and Deutscher Akademischer Austauschdienst (DAAD), grant 1110-11-0 CAPES/DAAD to W.d.C.S., by Agence Nationale de la Recherche (ANR) and Deutsche Forschungsgemeinschaft (DFG) within the French-German ANR-DFG project “Hypothetical Reasoning”, grant DFG Schr 275/16-1/2 to T.P.; and by DFG grant 444 BRA-113/66/0-1 to T.P.
1The Brouwer–Heyting–Kolmogorov (BHK) interpretation is taken to be the official rendering of the intuitionistic meaning for the logical constants. For each constant an individual clause establishes what conditions must be fulfilled in order to assert a proposition containing it (see [Heyting 1971]). The semantical clauses are supposed to be the main part of an inductive definition of the logical constants; the basis of this definition is to be given by stating the conditions under which atomic propositions in a specific mathematical theory can be asserted. Usually it is assumed that the assertability of atomic propositions can be specified by means of so-called boundary rules (as in [Dummett 1991]), production rules or Post system rules (as in [Prawitz 1971; 1974; 2006]). Our main concern here is with the BHK clause for implication. It gives a necessary condition for the assertability of implicational propositions, but it is not clear whether it gives a sufficient condition too. We show that for Prawitz’s account [Prawitz 1971] of the BHK clause for implication it is possible to constructively assert a proposition that is not provable in intuitionistic propositional logic (IPC). In other terms, IPC would be incomplete. In order to pinpoint the problem that causes this mismatch, we will analyze the implication clause into two component clauses (A) and (B), where clause (A) is the problematic one. We will consider only the two logical constants of disjunction (∨) and implication (→).
- 1 We cite from the third edition of 1971. The first edition was in 1956.
2The BHK interpretation was stated in [Heyting 1971 as follows:1
It will be necessary to fix, as firmly as possible, the meaning of the logical connectives; I do this by giving necessary and sufficient conditions under which a complex expression can be asserted. [Heyting 1971, 101]
- 2 Whereas he would use the letters p, q, r as variables for mathematical propositions. For technical (...)
3Here we give only the clauses for disjunction and implication, where Heyting uses Fraktur letters p, q, r as abbreviations for mathematical propositions2 and to refer to their respective constructions:
[...]p ∨ q can be asserted if and only if at least one of the propositions p and q can be asserted.
[...]p → q can be asserted, if and only if we possess a construction r, which, joined to any construction proving p (supposing that the latter be effected), would automatically effect a construction proving q. [Heyting 1971, 102–103
4In addition to the clauses for the propositional logical constants, the following substitution clause is given:
A logical formula with proposition variables, say A(p, q…), can be asserted, if and only if A(p, q…) can be asserted for arbitrary propositions p, q,…; that is, if we possess a method of construction which by specialization yields the construction demanded by A(p, q…). [Heyting 1971, 103]
5The clauses are formulated using “if and only if”. This can be read either as logical equivalence or as indicating that the left side is defined by the right side. A rendering of the clauses in the latter sense can, for example, be found in [van Dalen 2008, 154], where the definition sign “:=” is used instead of “if and only if”. Such a reading seems to be intended by Heyting when he says that the conditions in the clauses are given in order to “fix, as firmly as possible, the meaning of the logical connectives” [Heyting 1971, 101].
6Heyting’s formulation considers constructions used to prove p or q and constructions r used to transform one construction into another in the case of implication. Furthermore he says:
It is necessary to understand the word “construction” in the wider sense, so that it can also denote a general method of construction [...].[Heyting 1971, 103]
7He connects the concepts of assertion, construction and proof:
[...] a mathematical proposition p always demands a mathematical construction with certain given properties; it can be asserted as soon as such a construction has been carried out. We say in this case that the construction proves the proposition p and call it a proof of p. We also, for the sake of brevity, denote by p any construction which is intended by the proposition p. [Heyting 1971, 102]
and:
Every mathematical assertion can be expressed in the form: “I have effected a construction A in my mind”. [Heyting 1971,19]
8Thus the expression “can be asserted” used in the BHK clauses means “can be proved by a construction”. In the case of p → q this is the construction r.
9Although [Heyting 1971] gives many distinct examples of mathematical constructions, what exactly is a construction is not further specified, except for the condition that in the case of construction r it should automatically effect a construction proving q, and the fact that there cannot be a construction proving the tertium non datur [Heyting 1971, 103f.].
10The substitution clause is usually omitted in newer expositions of the BHK interpretation. Notwithstanding, its addition is important in order to avoid certain problems that would arise for open formulas, since Heyting treats every logical formula as a mathematical proposition (cf. [Heyting 1971, 103]). By the substitution clause open formulas can be asserted, but only under the condition that all closed substitution instances can be asserted (cf. [Sundholm & van Atten 2008]).
- 3 For the sake of uniformity we use Heyting's notation throughout.
11Proposing a systematic account of the BHK interpretation, [Prawitz 1971] states clauses for inductively establishing when something is a construction of a sentence; here we give only his clause for implication [Prawitz 1971, 276]:3
[(i*)] r is a construction of p → q if and only if r is a constructive function such that for each construction r′ of p, r(r′) (i.e., the value of r for the argument r′) is a construction of q;
12Next he points out that this must be relativized to a system determining what are constructions for atomic formulas:
In accordance with constructive intentions, I shall assume that the constructions of atomic formulas are recursively enumerable, and the notion of a construction can then be relativized conveniently to Post systems [...]. [Prawitz 1971, 276]
13Prawitz continues:
I shall thus speak of a construction r of a sentence p relative or over a Post system S. When p is atomic such a construction r will simply be a derivation of p in S. In accordance to clause [(i*)] when relativized to S, a construction r of p1 → p2 over S where p1 and p2 are atomic will be a constructive (or with Church’s thesis: recursive) function that transforms every derivation of p1 in S to a derivation of p2 in S. [Prawitz 1971, 276]
14Here S is a Post system given by production rules of the form
- 4 The production rules are understood to be instances of a finite number of schemata for atomic formu (...)
where the pi are atomic propositions and the set of premisses {p1,…, pn} can be empty.4
15[Prawitz 1971, 276] observes that the above proposal (i*) of a definition faces a problem. For any proposition p1 not constructible in S (i.e., non-derivable in S) p1 → p2 is automatically constructible over S. Therefore, an extension S′ of S (which is obtained by adding some new production rules to S) might turn p1 → p2 into a proposition which is not constructible over S′.
16The solution [Prawitz 1971, 276f.] adopts consists in requiring that the transformation be preserved for extensions of S. He defines constructions of sentences over a Post system S by the following induction:
(i) r is a construction of an atomic sentence p over S if and only if r is a derivation of p in S.
(ii) r is a construction of a sentence p → q over S if and only if r is a constructive object of the type of p → q and for each extension S′ of S and for each construction r′ of p over S′, r(r′) is a construction of q over S′. [Prawitz 1971, 278; we omit his clause for the universal quantifier]
17According to clause (i), derivability and validity for atomic sentences in a Post system coincide. Extensions S′ of S are understood to be monotonic extensions. The idea is thus that when a construction of an implication is shown, it must remain for monotonic extensions of the underlying Post system.
18Heyting’s BHK clause for implication can be divided into the following two clauses, which are equivalent to Heyting’s when taken together:
(A) q can be asserted under the assumption p if and only if we possess a construction r, which, joined to any construction proving p (supposing that the latter be effected), would automatically effect a construction proving q.
(B) p → q can be asserted if and only if q can be asserted under the assumption p.
19Assertability of q by clause (A) is conditional on having only one assumption p. Although it would be more natural to allow for assumptions p1,…,pn (n ≥ 1) (cf. [Sundholm 1983, 9]), which would also require a corresponding modification of clause (B), we maintain only one such occurrence, since the modification would deviate from the original BHK clause. Anyway, clauses (A) and (B) taken together would be a special case of a reformulation with assumptions p1,…,pn.
20Assuming that constructions for atomic propositions are represented by Post systems, clauses (A) and (B) have to be reformulated into the following two clauses, respectively:
(A′) q can be asserted under the assumption p over S if and only if we possess a construction r, which, for each extension S′ of S when joined to any construction r′ proving p over S′ (supposing that the latter be effected), would automatically effect a construction r(r′) proving q over S′.
(B′) p → q can be asserted [by a construction r] over S if and only if q can be asserted [by a construction r] under the assumption p over S.
21Here the right side of the biconditional in clause (A′) results from using Prawitz’s idea from clause (ii) of requiring that the constructions hold for all monotonic extensions of Post systems. Prawitz’s clause (ii) could be split into two clauses likewise.
22The BHK clause for disjunction is:
p → q can be asserted over S if and only if at least one of the propositions p and q can be asserted over S.
23The construction proving p ∨ q is usually considered as an ordered pair (i, r), where i = 0 or i = 1 and r is the construction proving p, in case i = 0, or it is the construction proving q, in case i = 1.
24For the fragment {∨, →} we are considering here, only the given clauses (A′), (B′) and (C) are relevant.
25The following rule has been shown in [Mints 1976] to be non-derivable in IPC:
26We refer to this rule as Mints’ rule. Abbreviating its premiss by Mints-P and its conclusion by Mints-C, we have what we call Mints’ law:
Mints-P → Mints-C
27Next we will show that the fragment {∨, →} of IPC is incomplete with respect to the considered interpretation of the logical constants given by clauses (A′), (B′) and (C). This is done by proving constructively that Mints’ law for atomic propositions p, q and s is validated in this fragment.
28Actually, we are going to prove a stronger result. We allow for extended Post systems S* given by atomic rules with assumption discharge of the form
where the Γi are (possibly empty) sets of atomic assumptions that can be discharged. Thus production rules are a special case of atomic rules with assumption discharge. In the following theorem, we consider Prawitz’s clause (i) and clauses (A′), (B′) and (C) as being given relative to such extended Post systems S* (instead of the usual Post systems S of production rules only).
29Theorem 1. Mints’ law for any atomic propositions p, q and s is valid in the fragment {∨, →} of IPC for any extended Post system S*.
30Proof. In order to validate Mints’ law for every extended Post system S*, we give a construction showing how to validate Mints-C assuming Mints-P for any S* and then apply clause (B′). We assume that modus ponens is validated by the clauses (A′) and (B′).
We show that we possess a construction r such that for any extension of S*, if r1 is a construction of (p → q) → (p ∨ s) in , then r(r1) is a construction of ((p → q) → p) ∨ ((p → q) → s) in , according to clause (A′). Let be any extension of S* in which r1 is a construction of (p → q) → (p ∨ s). Thus, also according to clause (A′), for every extension of over which r2 is a construction of (p → q), r1(r2) will be a construction of p ∨ s in .
First case: As p is an atomic proposition, r3 is a derivation in the extended Post system , since for atomic propositions derivability and validity in extended Post systems coincide. We could just take r3 and substitute p → q for every application of and apply modus ponens to obtain a construction r4 which is a derivation of p depending on the open assumption p → q. Then r4 is a construction for (p → q) → p over . Thus (0,r4) would be a construction for ((p → q) → p) ∨ ((p → q) → s) over .
Second case: As s is an atomic proposition, r3 is a derivation in , again, because for atomic propositions derivability and validity in extended Post systems coincide. Apply the same procedure as given in the first case. Then r4 is a construction for (p → q) → s) over . Thus (1, r4) is a construction for ((p → q) → p) ∨ ((p → q) → s) over .
In consequence, given a construction r1(r2), we extract a construction r3 and substitute in it (p → q) for every application of . The result is either a derivation r4 of (p → q) → p or it is a derivation of (p → q) → s), depending on the case, and (i,r4) is a construction of ((p → q) → p) ∨ ((p → q) → s), for i = 0 or i = 1, depending on the case. The procedure of extending by adding the rule and then looking for a derivation of ((p → q) → p) ∨ ((p → q) → s) is the required construction r.
31As Mints’ rule is non-derivable in IPC, Mints’ law is not a theorem of IPC. By Theorem 1 there are valid instances of Mints’ law, namely all those in which p, q and r are atomic. Therefore IPC is incomplete with respect to validity as given by Prawitz’s clause (i) and clauses (A′), (B′) and (C).
32The incompleteness result might be prevented by a change in the notion of what are constructions for atomic propositions, but not without consequences. One way to do this is to change Prawitz’s clause (i) to the effect that validity and derivability for atomic propositions do not coincide anymore. This can be achieved by changing the biconditional “if and only if” in clause (i) to “if”. As a result, we would be left with only a partial explanation of what are constructions for atomic propositions. Another way is to give up the restriction to production rules in Post systems and to allow for extended Post systems of atomic rules with assumption discharge. That this is no way out is already shown by Theorem 1, which holds for such extended Post systems as well as for production rules. Alternatively, one could allow rules with atomic conclusions to have also non-atomic propositions as premisses, thereby extending the notion of constructions for atomic propositions even further. But the inductive character of the BHK interpretation would be lost if complex extensions of this kind were allowed.
33It is not guaranteed that the BHK clause for implication gives a sufficient condition for the assertion of an implication. Whereas clause (B) is fine and clause (A) gives a necessary condition, it is not clear that the latter also gives a sufficient condition.
34It has been remarked that the BHK interpretation has actually to be considered as a family of interpretations (cf. e.g. [Kohlenbach 2008, remark 3.2, 43]): depending on what kind of constructions is considered, we end up with different interpretations. In our criticism, we tried to show for the particular case where atomic propositions are given by Post systems (or even by extended Post systems of atomic rules with assumption discharge) that incompleteness of IPC follows. But our criticism is not restricted to this particular assumption about atomic propositions. It concerns the way in which the BHK clause for implication is formulated.
35Concerning the incompleteness implied by Theorem 1, several options can be considered. One option is to consider IPC to be constructively incomplete and to look for other ways of defining a new constructive logical systembetter suited. Another option consists in allowing for complex extensions. But then a constructive semantic characterization of the logical constants cannot be given as an inductive definition, since logical constants could be used to describe constructions proving atomic propositions in this case. In both cases no changes are made to the BHK clauses. A third option is to change these clauses, that is, to change the semantics. But this would change the way hypothetical reasoning is explained from the constructivist point of view.