Navigation – Plan du site
Logic and Philosophy of Science in Nancy (I)

A Critical Remark on the BHK Interpretation of Implication

Wagner de Campos Sanz et Thomas Piecha
p. 13-22

Résumés

On analyse l’interprétation BHK de constantes logiques sur la base d’une prise en compte systématique de Prawitz, résultant en une reformulation de l’interprétation BHK dans laquelle l’assertabilité de propositions atomiques est déterminée par des systèmes de Post. On démontre que l’interprétation BHK reformulée rend davantage de propositions assertables que la logique propositionnelle intuitionniste rend prouvable. La loi de Mints est examinée en tant qu’exemple d’une telle proposition. La logique propositionnelle intuitionniste devrait par conséquent être considérée comme étant incomplète. Nous concluons par une discussion sur l’adéquation de l’interprétation BHK de l’implication.

Haut de page

Texte intégral

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.

1 Introduction

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

2 The BHK interpretation

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

[...]pq 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(pq…). [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 A clarification of the BHK clause for implication

3.1 Prawitz’s account

  • 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

Image 100000000000007A0000002340C2C786.png

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

3.2 Analysis of the implication clause

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

4 Incompleteness of IPC

25The following rule has been shown in [Mints 1976] to be non-derivable in IPC:

Image 10000000000000F70000002F323823D5.png

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-PMints-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

Image 100000000000008F00000041CF0F9BE6.png

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 Image 100000000000000E0000000EC4C7B4B9.png of S*, if r1 is a construction of (pq) → (ps) in Image 100000000000000E0000000EC4C7B4B9.png, then r(r1) is a construction of ((pq) → p) ∨ ((pq) → s) in Image 100000000000000E0000000EC4C7B4B9.png, according to clause (A′). Let Image 100000000000000E0000000EC4C7B4B9.png be any extension of S* in which r1 is a construction of (pq) → (ps). Thus, also according to clause (A′), for every extension Image 100000000000000E0000000D2FCB1132.png of Image 100000000000000E0000000EC4C7B4B9.png over which r2 is a construction of (pq), r1(r2) will be a construction of ps in Image 100000000000000E0000000D2FCB1132.png.

  • 5 See clause (C) for an explanation of the ordered pair.

The construction (procedure) r is described in what follows. Let Image 100000000000000E0000000D2FCB1132.png be obtained from Image 100000000000000E0000000EC4C7B4B9.png by adding the rule Image 100000000000000D00000017F1EA5E2C.png. As constructions of atomic propositions are given by derivations in an extended Post system (according to Prawitz’s clause (i)), we can say that this rule corresponds to a construction r2 in Image 100000000000000E0000000D2FCB1132.png. This extension Image 100000000000000E0000000D2FCB1132.png can always be effected for any Image 100000000000000E0000000EC4C7B4B9.png. Therefore r1(r2) is a construction of ps over Image 100000000000000E0000000D2FCB1132.png. By clause (C) there are two cases. Either5 r1(r2) = (0,r3), and r3 is a construction of p, or r1(r2) = (1,r3), and r3 is a construction of s.

First case: As p is an atomic proposition, r3 is a derivation in the extended Post system Image 100000000000000E0000000D2FCB1132.png, since for atomic propositions derivability and validity in extended Post systems coincide. We could just take r3 and substitute pq for every application of Image 100000000000000D00000017F1EA5E2C.png and apply modus ponens to obtain a construction r4 which is a derivation of p depending on the open assumption pq. Then r4 is a construction for (pq) → p over Image 100000000000000E0000000EC4C7B4B9.png. Thus (0,r4) would be a construction for ((pq) → p) ∨ ((pq) → s) over Image 100000000000000E0000000EC4C7B4B9.png.

Second case: As s is an atomic proposition, r3 is a derivation in Image 100000000000000E0000000EC4C7B4B9.png, 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 (pq) → s) over Image 100000000000000E0000000EC4C7B4B9.png. Thus (1, r4) is a construction for ((pq) → p) ∨ ((pq) → s) over Image 100000000000000E0000000EC4C7B4B9.png.

In consequence, given a construction r1(r2), we extract a construction r3 and substitute in it (pq) for every application of Image 100000000000000D00000017F1EA5E2C.png. The result is either a derivation r4 of (pq) → p or it is a derivation of (pq) → s), depending on the case, and (i,r4) is a construction of ((pq) → p) ∨ ((pq) → s), for i = 0 or i = 1, depending on the case. The procedure of extending Image 100000000000000E0000000EC4C7B4B9.png by adding the rule Image 100000000000000D00000017F1EA5E2C.png and then looking for a derivation of ((pq) → p) ∨ ((pq) → 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).

4.1 Changing the notion of atomic constructions: a way out?

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.

5 Discussion

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.

Haut de page

Bibliographie

Dummett, Michael [1991], The Logical Basis of Metaphysics, London: Duckworth.

Heyting, Arend [1971], Intuitionism. An Introduction, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, 3rd edn.

Kohlenbach, Ulrich [2008], Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Berlin: Springer.

Mints, Grigori E. [1976], Derivability of admissible rules, Journal of Soviet Mathematics, 6, 417–421, doi:10.1007/BF01084082.

Prawitz, Dag [1971], Ideas and results in proof theory, in: Proceedings of the Second Scandinavian Logic Symposium, edited by J. E. Fenstad, Amsterdam: North-Holland, Studies in Logic and the Foundations of Mathematics, vol. 63, 235–307.

[1974], On the idea of a general proof theory, Synthese, 27(1–2), 63–77, doi:10.1007/BF00660889, reprinted in R. I. G. Hughes (ed.), A Philosophical Companion to First-Order Logic, Indianapolis: Hackett Publishing Company, 212–224, 1993.

— [2006], Meaning approached via proofs, Synthese, 148(3), 507–524, doi:10.1007/s11229-004-6295-2.

Sundholm, Göran [1983], Constructions, proofs and the meaning of logical constants, Journal of Philosophical Logic, 12(2), 151–172, doi:10.1007/BF00247187.

Sundholm, Göran & van Atten, Mark [2008], The proper explanation of intuitionistic logic: on Brouwer’s demonstration of the Bar Theorem, in: One Hundred Years of Intuitionism (1907–2007) – The Cerisy Conference, edited by M. van Atten, P. Boldini, M. Bourdeau, & G. Heinzmann, Basel: Birkhäuser, 60–77.

van Dalen, Dirk [2008], Logic and Structure, Berlin: Springer, 4th edn.

Haut de page

Notes

1 We cite from the third edition of 1971. The first edition was in 1956.

2 Whereas he would use the letters p, q, r as variables for mathematical propositions. For technical reasons, we use bold italic letters instead of Fraktur letters here.

3 For the sake of uniformity we use Heyting's notation throughout.

4 The production rules are understood to be instances of a finite number of schemata for atomic formulas.

5 See clause (C) for an explanation of the ordered pair.

Haut de page

Pour citer cet article

Référence électronique

Wagner de Campos Sanz et Thomas Piecha, « A Critical Remark on the BHK Interpretation of Implication », Philosophia Scientiæ [En ligne], 18-3 | 2014, mis en ligne le 19 janvier 2015, consulté le 22 juin 2018. URL : http://journals.openedition.org/philosophiascientiae/965 ; DOI : 10.4000/philosophiascientiae.965

Haut de page

Auteurs

Wagner de Campos Sanz

Universidade Federal de Goiás (Brasil)

Thomas Piecha

University of Tübingen (Germany)

Haut de page

Droits d’auteur

Tous droits réservés

Haut de page