**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 **p**_{1} → **p**_{2 }over **S** where **p**_{1} and **p**_{2} are atomic will be a constructive (or with Church’s thesis: recursive) function that transforms every derivation of **p**_{1} in **S** to a derivation of **p**_{2} 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 **p**_{i} are atomic propositions and the set of premisses {**p**_{1,…, }**p**_{n}} can be empty.4

15[Prawitz 1971, 276] observes that the above proposal (i^{*}) of a definition faces a problem. For any proposition **p**_{1} not constructible in **S** (i.e., non-derivable in **S**) **p**_{1} → **p**_{2}_{ }is automatically constructible over **S**. Therefore, an extension **S′** of **S** (which is obtained by adding some new production rules to **S**) might turn **p**_{1} → **p**_{2} 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 **p**_{1},…,**p**_{n} (*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 **p**_{1},…,**p**_{n}.

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).

29**Theorem 1**. *Mints’ law for any atomic propositions ***p***, ***q*** and ***s*** is valid in the fragment *{∨, →}* of *IPC* for any extended Post system*_{ }**S**^{*}*. *

30*Proof.* 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 **r**_{1} is a construction of (**p** → **q**) → (**p** ∨ **s**) in , then **r**(**r**_{1}) is a construction of ((**p** → **q**) → **p**) ∨ ((**p** → **q**) → **s**_{)} in , according to clause (A′). Let be any extension of **S**^{*} in which **r**_{1} is a construction of (**p** → **q**) → (**p** ∨ **s**). Thus, also according to clause (A′), for every extension of over which **r**_{2} is a construction of (**p** → **q**), **r**_{1}(**r**_{2}) will be a construction of **p** ∨ **s** in .

First case: As **p** is an atomic proposition, **r**_{3} is a derivation in the extended Post system_{ }_{}, since for atomic propositions derivability and validity in extended Post systems coincide. We could just take **r**_{3} and substitute **p** → **q** for every application of and apply *modus ponens* to obtain a construction **r**_{4} which is a derivation of **p** depending on the open assumption **p** → **q**. Then **r**_{4} is a construction for _{(}**p** → **q**) → **p** over_{ }_{}. Thus (0,**r**_{4}) would be a construction for ((**p** → **q**) → **p**) ∨ ((**p** → **q**) → **s**_{)} over_{ }.

Second case: As **s** is an atomic proposition, **r**_{3} 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 **r**_{4} is a construction for (**p** → **q**) → **s**) over_{ }. Thus (1, **r**_{4}) is a construction for ((**p** → **q**) → **p**) ∨ ((**p** → **q**) →_{ }**s**_{)} over_{ }.

In consequence, given a construction **r**_{1}(**r**_{2}), we extract a construction **r**_{3} and substitute in it (**p** → **q**) for every application of . The result is either a derivation **r**_{4} of (**p** → **q**) → **p** or it is a derivation of_{ }(**p** → **q**) → **s**), depending on the case, and (*i*,**r**_{4}) 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.