Abstract
The first half of the paper discusses recursive versus constructive functions and, following Heyting, stresses that from a constructive point the former cannot replace the latter. The second half of the paper treats of the Kreisel-Myhill theory CS for Brouwer’s Creating Subject, and its relation to BHK meaning-explanations and Kripke’s Schema. Kripke’s Schema is reformulated as a principle and shown to be classically valid. Assuming existence of a verification-object for this principle, a modification of a proof of conservativeness of Van Dalen’s, is shown to give a relative BHK meaning explanation for the Kreisel-Myhill connective. The result offers an explanation of why Kripke’s Schema can be used as a replacement of the Theory of Creating Subject when formulating Brouwerian counter-examples. It also shows that the Theory of Creating Subject is classically valid.
Originally published at https://www.academia.edu/3528209/Constructive_recursive_functions_Church_thesis_and_Kripkes_schema.© 2013 B.G. Sundholm. Reprinted with permission of B.G. Sundholm.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Stefan Zweig (1979, p. 191), apropos Calvin’s Institutio.
- 2.
I am happy to have Alonzo Church on my side here; see his letter to Yannis Moschovakis that is printed as an appendix. NB. One must not confuse relative computability (from an oracle) with computability that is not effective. Moschovakis has treated beautifully of relative computability and Church’s Thesis in his Heyting lecture at Amsterdam, September 2012.
- 3.
See Ackermann (1928). My Oxford supervisor Robin Gandy told me that during WWII, at Bletchley Park, Alan Turing proposed a challenging competition:
What is the largest natural number that can be written on a postcard?
Clearly transfinite hierarchies of fast-growing functions offer a promising way to attack the problem, and hence constructive notation-systems for large ordinals are called for, so as to be able to write terms for very large numbers, though I do not know the answer to Turing’s challenge. In correspondence Andrew Hodges pointed out that John von Neumann’s proposed something very similar to Stanislaw Ulam already in 1938, in connection with some ‘schemata of Turing’s’. The matter is dealt with by Hodges (1983, p. 145), and the pertinent letter from Ulam to Hodges can be found at http://www.turing.org.uk/sources/vonneumann.html.
These ‘schemata of Turing’s’ need not be the rules for building Turing-machines. In the present context of giving notations for large natural numbers they could equally well, or perhaps even better, refer to ‘the first rather general scheme for definition of number theoretic functions by transfinite recursion,’ which, according to Robin Gandy, was given by Turing in his dissertation, cf. Feferman (1988, p. 141, footnote 24). Furthermore, Von Neumann mentioned Turing to Ulam several times ‘concerning mechanical ways to develop formal mathematical systems.’ Since the works of Gödel and Gentzen the addition of schemes for proof by transfinite induction or for defining functions by means of transfinite recursion are well-known ways for obtaining stronger mathematical systems.
Robin Gandy was not at Bletchley Park during the war. However, in the early 1950s he was working on Gentzen’s First Consistency Proof, and would have had occasion to think about ordinal induction and recursion, cf. Kreisel (1955, footnote 9 at p. 38). His supervisor and friend Turing owned an offprint of Gentzen’s paper; he might well have told Gandy about the general scheme of recursion from his Princeton dissertation and of the Bletchley challenge.
- 4.
- 5.
I confine myself to mathematical examples and shall disregard such uses as ‘Neither his position, nor his conduct in the debate, could be called constructive’, where ‘constructive’ seems to mean apt or purposeful.
- 6.
Dummett (1975, especially at p. 231).
- 7.
- 8.
See Brouwer (1912). Brouwer’s position thus is an epistemic realism based on an Ontological Descriptivism with respect to an idealist ontology. Bishop Berkeley is another philosopher with a similar pair of positions. My own meaning theoretical stance is to the contrary an epistemic idealism, whereas my ontology is thoroughly Platonist; however, I do not found my semantic and epistemic norms of rightness therein.
- 9.
Such equations are deployed by Beeson (1981, p. 148).
- 10.
Tait (2006, p. 213). The quoted text was italicized in its entirety by Tait.
- 11.
The dependent function-sets are formed with the use of the set-theoretic dependent-product operator \(\Pi \), though for the sake of simplicity, I here confine myself to the → case where the set B does not depend upon the element of x: A. The elements of function-sets are known as courses-of-value or graphs, and require an application function ap in order to yield their values.
- 12.
Pascal gave his canon of definition in the manuscript De l’Esprit géométrique, but it became known through the Port-Royal Logic, Arnauld and Nicole (1662, Part IV, Ch. III). The notion of definitional (or criterial) identity a = b: A, with respect to the elements of the set A, must be clearly kept apart from the propositional function I(A, x, y): prop(x: A, y: A). From the judgement
$$\displaystyle{ a = b: A, }$$where the judgements a: A and b: A have to be already known as its presuppositions, we may, of course infer the judgement
$$\displaystyle{ I(A,a,b)\ \text{true}, }$$but not vice versa. The positions to the left of the judgemental colon are opaque in the terminology of Quine; there the terms carry ‘conceptual supposition’ (suppositio simplex in the medieval terminology) and do not stand for their referents. To the right of the judgemental colon the positions are transparent and the matching supposition is ‘referential’ (suppositio personalis).
- 13.
Curry and Feys (1958, p. 43).
- 14.
Together, of course, with other similar systems for typed lambda-calculus with dependent types. The richness of CTT allows one to distinguish three notions among what are commonly called functions in informal mathematics, to wit
-
(i)
Frege-Euler functions, that is, dependent objects of lowest type, for instance x + 5: N provided that x: N, where substitution takes care of application;
-
(ii)
Dedekind mappings, that is independent objects of higher type, for instance (x). x + 5: N → N, where application is a primitive notion;
-
(iii)
Graphs, or ‘courses-of-value’, for instance \({ \uplambda }(\mathbf{N},\mathbf{N}, (x).x + 5): (\Pi x: \mathbf{N})\mathbf{N}\), where application is effected by means of a separate application function ap(x, y) taking a course-of-value c and a suitable argument a into the value ap(c, a).
-
(i)
- 15.
- 16.
Already Kronecker insisted that definitions should be, in the words of his pupil Jules (Julius) Molk (1885, p. 8) ‘algebraic and not merely logical’. Molk also stressed that definitions by undecided separation of cases are inadmissible in his remarkable anticipation of Brouwer’s 1908 criticism of the Law of Excluded Middle in (1904, ‘§10. Point de vue de Kronecker’, at p. 160). Molk’s scoop is dealt with at some length in the introduction, written jointly with Mark van Atten, to our novel translation of Brouwer 1908. Already Largeault (1993, p. 81) noted these little-known points about Molk, but did not stress their importance.
- 17.
An example of the kind g was famously used by Hartley Rogers in his canonical textbook on recursion theory (1967, §1.2, p. 9).
- 18.
In Martin-Löf’s (1984) CTT, this is nothing but an application of the ∨-elimination rule.
- 19.
Undecided separation of cases is sometimes rejected also in other than mathematical contexts. Thus we do not accept—at least the fiscal authorities do not accept—the following as a definition of a human taxpayer:
$$\displaystyle{ \text{PM} = _{\mathrm{df}}\left \{\begin{array}{@{}l@{\quad }l@{}} \text{Tony Blair} \quad &\text{if the Riemann Hypothesis is true;} \\ \text{Gordon Brown}\quad &\text{if the Riemann Hypothesis is false.} \end{array} \right. }$$PM does not pay taxes and is not accepted as an individual. Classical mathematicians, though, are readily prepared to proceed similarly when defining functions or sets.
When I first visited Holland in 1979, Henk Barendregt told me of the following nice example from the game of chess. It concerns a famous problem in ‘retrograde analysis’ by Langstaff from Chess Amateur 1922, White to move and mate in two (found on line here: http://en.wikipedia.org/wiki/Retrograde_analysis). If Black is not allowed to castle, that is, if either King or Rook has already moved, then 1. Kf5-e6 allows mate on the next move, but if Black is allowed to castle,
then his last move was not with either King or Rook, and must accordingly be g7-g5, in which case 1. h5xg6 en passant allows mate on the next move. Tim Krabbé, the Dutch expert of the outré corners of chess, characterised the situation as follows (1985, p. 50–51): ‘If White attempts one solution Black has a defence which shows the other would have worked. Or to put it differently again: it is perfectly true g7-g5 and Rh7-h8 cannot both be Black’s last move, but White (or the solver) has no way of determining which one was. Whoever feels giddy should now consult his local syllogism breaker.’ Krabbé is right that something out of the ordinary is going on in logic here. A constructivist would classify this as a typical LEM failure and reject the problem as ill posed.
- 20.
For ease of exposition I display only the simplest form of the schema; each function may, of course, depend on a vector x 1, …, x k of further variables.
- 21.
The need for the known truth of the presupposition here constitutes another argument against classical mathematical practice: unless known, mere truth of the totality presupposition does not entitle one to introduce the minimalization in question as a function.
- 22.
Kleene’s indexing of the primitive recursive schemata of definition, and the diagonalization in question, can be found in his (1958).
- 23.
I have inspected 32 different presentations of Zorn’s lemma and its demonstration. The fine details may vary, but basically there are two proofs. The easy one proceeds by ordinal recursion, using the choice function for as long as it is possible to find larger elements in the set m, to pick a majorizing element and using it to define an injection from an initial segment of the ordinals into the set m. Since we deal with a set m, it is not equinumerous with the set-theoretic universe, whence at some stage it will no longer be possible to find yet another majorizing element in m. However, the question as to whether a larger element can still be found within the set m is an undecided separation of cases. The other kind of proof is modelled after Zermelo’s (1908) second, Dedekind-inspired, ‘algebraic’ demonstration of the well-ordering theorem and also here one finds definitions by means of undecided separations of cases.
- 24.
Kleene’s T-predicates (for all number of arguments), and other associated functions and predicates, are primitive recursive (1952, § 57). In fact, they are even Kalmár-elementary. However, analogously to the above considerations regarding + and its recursion equations, the significance of their Kalmár-elementary status depends on whether they are taken from a classical or a constructivist point of view: is it a mere factual property that happens to hold in the ontology or an essential means of introducing them?
- 25.
Church (1936, p. 351, footnote 10). That calculability of a recursive function may depend essentially on the character of the demonstration that it is (primitive) recursive was lucidly stressed by Arend Heyting in a series of writings, for instance (1954, pp. 81–82), (1958b, p. 106), (1961, p. 187), (1962, p. 196), and (1969, p. 4).
- 26.
Mendelson (1990, p. 226) stresses the classical origin of Church’s Thesis: ‘Thus, we are adopting a completely classical, nonintuitionistic stance’.
- 27.
Heyting voices a complaint of the kind alluded to by Church in (1954, pp. 81–82).
- 28.
Heyting made also this point on a number of occasions, including the pellucid (1958a). As observed by Thierry Coquand in his paper at the Joint Session, also Skolem saw that within constructivism the primitive notion of a function cannot be replaced by that of a general recursive function. Rózsa Péter (1959) is a third author stressing that the notion of a recursive function cannot constructively replace the notion of a constructive function.
- 29.
Beeson (1985, p. 90) presents a nice result of Troelstra’s that Extensionality and Formal Church’s Thesis are incompatible over type theory.
- 30.
See its Proceedings that were edited by Van Rootselaar and Staal (1968, Ch. 2, pp. 121–223).
- 31.
- 32.
Van Atten (2008) also prefers to work in terms of proofs and uses ‘The ideal mathematician has at time n obtained a proof of proposition p’. In his book (2004, p. 64) Van Atten, with an insignificant typographical change, uses ‘the subject has experienced A at m’, presumably in order to accommodate the Brouwerian view of truth (2004, p. 18): ‘To experience a truth is to experience that a certain construction has succeeded.’ This formulation might not be entirely felicitous: juxtaposing these passages, there seems to be no difference between experiencing a proposition and experiencing the truth of a proposition. In his joint paper with Van Dalen (2002, p. 522) he uses ‘the creating subject experiences A (has full evidence for A) at time m’, which appears to identify experiencing A with having full evidence for A. (For how to deal with evidence see further down the main text, around footnote mark 33.) The difference between the ‘evidence’ of earlier writers and the ‘full evidence’ of Van Dalen and Van Atten is intended to rule out readings that admit insufficient evidence. Furthermore, the notion of proposition that is at issue here is not clear to me. It will not be the BHK one. Instead Van Atten’s A would appear to contain assertoric force and be demonstrated.
- 33.
The responsibility for this ‘ethico-theological’ terminology is credited to Kreisel, though to the best of my knowledge it was first published by Myhill (1967, p. 296).
- 34.
I deal with the ambiguities of evidence in my (2011).
- 35.
In the review (1967, p. 248), Kreisel allows for the quantification over creating subjects. His notation is still the same
$$\displaystyle{ \Sigma \vdash _{n}A }$$but now with \(\Sigma \) as a variable over subjects, and the reading: ‘at time n the subject has evidence to assert A’. In (1970) he casts this as ‘A has been proved by the nth stage’. In (1971) Kreisel elaborates on the alternative formulation in terms of an \({ \upomega }\)-ordering of demonstrations (‘proofs’) and notes that Kreisel (1970, §4) ‘considers the schema KS which is inconsistent with C[hurch’s] T[hesis]. (The schema KS was derived by Kripke from Brouwer’s assertions about the thinking subject, or better from the postulate of an \({ \upomega }\)-ordering of levels of proofs.)’.
- 36.
- 37.
Geach (1965).
- 38.
The same worry might apply also to a Brouwerian use of the implication ⊃. For Brouwer, truth is truth known, ‘experienced’ truth, and accordingly an assumption that proposition A is true amounts to an assumption that A is known to be true. Van Atten (2009) contains a promising attempt at rescuing Brouwer’s position by reading implication A ⊃ B as essentially involving only relations between the proof-conditions, but not the actual existence of proofs, for the component propositions A and B.
- 39.
Here I part company with Van Dalen and Van Atten (2002, p. 522), who claim such evidence.
- 40.
Similarly it justifies the (open) consequence (‘conditional’)
if A is true, then B is true
that is, as the hypothetical judgement
B is true, on condition (hypothesis, assumption …) that A is true,
which we may symbolize with a Gentzen sequent arrow
A true ⇒ B true.
Constructively an open consequence (hypothetical judgment, Gentzen sequent) is verified by a hypothetical (‘dependent’) proof-object b: B(x: A).
- 41.
In order to prevent misunderstanding I here prefer to use the Van Dalen-Van Atten ‘modal’ notation for the Creating Subject connective rather than the Kreisel-Myhill-Dummett turnstile notation.
- 42.
- 43.
The letter from Moschovakis to Church printed in the appendix makes clear that Kripke’s reasoning was known in 1968, at the time of the Buffalo conference on Intuitionism and Proof Theory. The schema is clearly presaged in Kripke (1965).
- 44.
By ‘negative’ I understand using \(\neq _{\mathbf{Bool}}\mathbf{f}\) rather than \(= _{\mathbf{Bool}}\mathbf{t}\) when formulating the principle.
- 45.
Van Dalen (1982b, p. 174, my translation):
Kripkes Schema sieht ein bißchen aus wie ein triviales Komprehensionsprinzip. Das Komprehensionsprinzip postuliert eine charakteristische Funktion, die prüft, ob ein Element die Eigenschaft A(x) hat. Kripkes Schema postuliert eine Funktion, die prüft, ob A gilt. Klassisch ist das natürlich völlig trivial.
I am indebted to Mark van Atten, who drew my attention to this passage when informed of the classical derivation of Kripke’s Schema given above. Troelstra and Van Dalen (1988, Ch 4, §9) use second-level quantification, not just over functions in Bool → N, or in N → N, but also over sets (‘species’) instead and treat of Kripke’s schema in terms of the quantifier combination
$$\displaystyle{ (\forall X: prop)(\exists \upalpha: \mathbf{N} \rightarrow \mathbf{N})(\forall n: \mathbf{N}) }$$(where I have made quantificational domains explicit). From a constructive point of view this introduces yet another, and this time superfluous, complication into the Theory of the Creating Subject, namely that of impredicative quantificational domains, whence I prefer the earlier treatments in terms of functions, especially in the closed (BKP) form.
- 46.
As far as I know the precise proof-theoretic strength of Kripke’s schema is undetermined.
- 47.
Kripke, to the best of my knowledge, never published his treatment, and perhaps it was not even written up. Van Dalen (1978, p. 40, footnote 3) gave a nice exposition that is unfortunately marred by garbled printing. Van Dalen’s presentation was emended by Van Atten (2008), whose exposition I follow.
- 48.
Myhill refers explicitly and at length to BHK in (1967).
- 49.
This holds true also for quantification with respect to choice sequences; one would have had hopes for a uniform BHK account of quantification with respect to all quantificational domains and then an explanation of the notion of choice sequence such that, for instance, the various continuity principles can be read off by combining these explanations. Heyting’s brief treatment (1959, §6 pp. 70–71) is the only one by a Founding Father known to me. The issue is noted in my (1983, pp. 163–164) and (1984, pp. xiii–xiv).
- 50.
Dummett’s (1977, p. 353, formula (xxi*)) explains Van Dalen’s construction, but also does not give details.
- 51.
- 52.
In general, when P is a propositional function of the appropriate type, inferences of the kind
$$\displaystyle{ \frac{I(A,a,b)\ \text{true}} {P(a) \leftrightarrow P(b)\ \text{true}} }$$are valid. Accordingly, we define the function h: Bool → U, where U is the first universe, by Bool elimination:
$$\displaystyle\begin{array}{rcl} h(\mathbf{t})& =& \top: U {}\\ h(\mathbf{f})& =& \perp: U. {}\\ \end{array}$$Hence, from the assumption
$$\displaystyle{ [\mathbf{t} = _{\mathbf{Bool}}\mathbf{f}]\ \text{true} }$$we get that their respective values under the function h are propositionally equivalent, whence (⊤ ↔ ⊥ ) true, and so that ⊥ true under the assumption. Hence \((\mathbf{t}\neq _{\mathbf{Bool}}\mathbf{f})\) true. The crucial Peano axiom
$$\displaystyle{ [\mathbf{s}(x)\neq _{\mathbf{N}}0]\ \text{true} }$$is demonstrated by the same technique, that is, defining a function from N to the first universe U that is ⊥ on 0 and ⊤ on the numbers greater than 0.
In order to demonstrate the decidability of = Bool , assume x: Bool and y: Bool. By the Bool elimination rule we readily demonstrate
$$\displaystyle{ \forall z: \mathbf{Bool}(z = _{\mathbf{Bool}}\mathbf{t} \vee z = _{\mathbf{Bool}}\mathbf{f})\ \text{true.} }$$But then \(x = _{\mathbf{Bool}}\mathbf{t} \vee x = _{\mathbf{Bool}}\mathbf{f})\).
When (Case 1) (x = Bool t) true, we have two cases, (1a) (y = Bool t) true, and (1b) (y = Bool f) true.
In (Case 1a), (x = Bool t) true and (y = Bool t) true, whence (x = Bool y) true by = Bool rules, and so, by ∨ elimination, (x = Bool y ∨ x ≠ Bool y) true.
In (Case 1b), (x = Bool t) true and (y = Bool f) true. An assumption that (x = Bool y) true by means of the rules for = Bool yields t = Bool f, which gives a contradiction with the already demonstrated theorem that (t ≠ Bool f) true. Hence (x ≠ Bool y) true, and by ∨ elimination, (x = Bool y ∨ x ≠ Bool y) true also in this case.
When (Case 2) (x = Bool f) true, there are yet again two cases.
In (Case 2a) (x = Bool f) true and (y = Bool t) true. As in (Case 1b) we obtain (x ≠ Bool y) true and so, by ∨ elimination, (x = Bool y ∨ x ≠ Bool y) true. In (Case 2a) (x = Bool f) true and (y = Bool f) true, whence (x = Bool y) true. By ∨ elimination we obtain (x = Bool y ∨ x ≠ Bool y) true and two applications of \(\forall \) introduction with respect to the assumptions x: Bool and y: Bool establish the required decidability of ≠ Bool .
- 53.
Hull (1969, p. 241).
- 54.
The words are Troelstra’s (1969, p. 107).
References
Ackermann, W. (1928). Zum Hilbertschen Aufbau der reellen Zahlen. Mathematische Annalen, 99, 118–133.
Arnauld, A., & Nicole, P. (1662). La Logique ou L’Art de Penser. Paris: C. Savreux.
van Atten, M. (2004). On brouwer. Louisville: Wadsworth—Thomson Learning.
van Atten, M. (2008). The foundations of mathematics as a study of life: An effective but non-recursive function. Progress in Theoretical Physics, 173, 38–47.
van Atten, M. (2009). The hypothetical judgement in the history of intuitionistic logic. In C. Glymour, W. Wang, & D. Westerståhl (Eds.), Logic, methodology, and philosophy of science XIII: Proceedings of the 2007 international congress, Beijing (pp. 122–136). London: College Publications.
Beeson, M. (1981). Formalizing constructive mathematics: Why and how? In F. Richman, Constructive mathematics (Lecture notes in mathematics, Vol. 873, pp. 146–190). Berlin: Springer.
Beeson, M. (1985). Foundations of constructive mathematics. Berlin: Springer.
Brouwer, L. E. J. (1912). Intuitionisme en Formalisme (Inaugural lecture at the University of Amsterdam, October 14, 1912). Amsterdam: Clausen (Translated into English by Arnold Dresden as Intuitionism and formalism. Bulletin of the American Mathematical Society, 20, 81–96 (1913), reprinted in both editions of P. Benacerraf & H. Putnam (Eds.), Philosophy of Mathematics, Blackwell, Oxford, 1964, pp. 66–77, and Cambridge University Press, Cambridge, 1983, pp. 77–89.
Church, A. (1936). An unsolvable problem in elementary number theory. American Journal of Mathematics, 58, 345–363
Curry, H., & Feys, R. (1958). Combinatory logic (Vol. 1). Amsterdam: North-Holland.
van Dalen, D. (1978a). An interpretation of intuitionistic analysis. Annals of Mathematical Logic, 13, 1–43.
van Dalen, D. (1978b). Filosofische grondslagen van de wiskunde. Assen: Van Gorcum.
van Dalen, D. (1982a). The creative subject and heyting arithmetic. In Universal algebra and applications (Banach Center publications, Vol. 8, pp. 379–382). Warsaw: PWN Scientific Publishers.
van Dalen, D. (1982b). Braucht die konstruktive Mathematik Grundlagen? Jahresbericht der Deutschen Mathematiker-Vereinigung, 84, 57–78.
van Dalen, D., & van Atten, M. (2002). Intuitionism. In D. Jaquette (Ed.), A companion to philosophical logic (pp. 513–530). Oxford: Balckwell.
Dummett, M. (1975). The philosophical basis of intuitionistic logic. In M. Dummett, Truth and other Enigmas (pp. 215–247) London: Duckworth, 1978. Text of a lecture delivered at the Bristol Proceedings of the logic Colloquium’73, and originally published in the 1975 thereof.
Dummett, M. (1977). Elements of intuitionism. Oxford: Oxford University Press.
Enderton, H. (2010). Computability theory: An introduction to recursion theory. Burlington: Academic.
Feferman, S. (1988). Turing in the land of O(z). In R. Herken (Ed.), The Universal Turing Machine (pp. 113–147). Oxford/New York: Oxford University Press.
Fichte, J. G. (1797). Erste Einleitung in die Wissenschaftslehre. Philosophisches Journal, V, 1–47.
Geach, P. (1965). Assertion. Philosophical Review, 74(4), 449–465.
Haberthür, R. (1976). Normalizationssätze für Intuitionistische Theorien mit Wahlfolgen. Dissertation, Basel University.
Haberthür, R. (1978). Choice sequences and reduction processes. Archiv für mathematische Logik, 19, 31–49.
Heyting, A. (1954). Logique et intuitionnisme. In Actes du 2e colloque internationale de logique mathématique, Paris, 1952 (pp. 75–82). Paris-Lovain: Gauthier-Villars.
Heyting, A. (1958a). Blick von der intuitionistischen Warte. Dialectica, 12, 332–345.
Heyting, A. (1958b). Intuitionism in mathematics. In R. Klibansky (Ed.), Philosophy in the mid-century. A survey (pp. 101–115). Firenze: La Nuova Editrice.
Heyting, A. (1959). Some remarks on intuitionism. In A. Heyting (Ed.), Constructivity in mathematics (pp. 72–80). Amsterdam: North-Holland.
Heyting, A. (1961). Infinitistic methods from a finitist point of view. In Infinitistic methods (pp. 185–192). Oxford/Warsaw: Pergamon/PWN.
Heyting, A. (1962). After thirty years. In E. Nagel, P. Suppes, & A. Tarski (Eds.), Logic, methodology, and philosophy of science, proceedings of 1960 international congress, Stanford (pp. 194–197). Stanford University Press.
Heyting, A. (1969). Wat is berekenbaar? Nieuw Archief voor Wiskunde (3), 17, 1–7.
Hodges, A. (1983). Alan turing: The Enigma. London: Burnett Books.
Howard, W., & Kreisel, G. (1966). Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. Journal of Symbolic Logic, 31, 325–358.
Hull, R. (1969). Counterexamples in intuitionistic analysis using Kripke’s schema. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 15, 241–246.
Kalmár, L. (1959). An argument against Church’s thesis. In A. Heyting (Ed.), Constructivity in mathematics (pp. 72–80). Amsterdam: North-Holland.
Kleene, S. (1938). On notation for ordinal numbers. Journal of Symbolic Logic, 3, 150–155.
Kleene, S. (1952) Introduction to metamathematics. Amsterdam: North-Holland.
Kleene, S. (1958). Extension of an effectively generated class of functions by enumeration. Colloquium Mathematicum, 6, 67–78.
Kleene, S., & Vesley, R. (1965). The foundations of intuitionistic mathematics. Amsterdam: North-Holland.
Krabbé, T. (1985). Chess curiosities. London: George Allen and Unwin.
Kreisel, G. (1955). Models, translations, and interpretations. In Th. Skolem et al. (Eds.), Mathematical interpretations of formal systems (pp. 26–50). Amsterdam: North-Holland.
Kreisel, G. (1965). Mathematical logic. In T. Saaty (Ed.), Lectures on modern mathematics (pp. 95–195). New York: Wiley.
Kreisel, G. (1967a). Informal rigour and completeness proofs. In I. Lakatos (Ed.), Problems in the philosophy of mathematics. Proceedings of the international colloquium in the philosophy of science, London, 1965 (Vol. 1, pp. 138–186). Amsterdam: North-Holland.
Kreisel, G. (1967b). Review of Kleene and Vesley (1965). Zentralblatt für Mathematik und ihre Grenzgebiete, 123, 246–248.
Kreisel, G. (1970a). Church’s thesis: A kind of reducibility axiom for constructive mathematics. In A. Kino, J. Myhill, & R. E. Vesley (Eds.), Intuitionism and proof theory. Proceedings of the summer conference, Buffalo, 1968 (pp. 121–150). Amsterdam: North-Holland.
Kreisel, G. (1970b). Review of Myhill (1967). Zentralblatt für Mathematik und ihre Grenzgebiete, 187, 263–265.
Kreisel, G. (1971). Review of Kreisel (1970). Zentralblatt für Mathematik und ihre Grenzgebiete, 199, 300–301.
Kreisel, G. (1987). Church’s thesis and the ideal of informal rigour. Notre Dame Journal of Formal Logic, 28, 499–519.
Kreisel, G., & Troelstra, A. S. (1970). Formal systems for some branches of intuitionistic analysis. Annals of Mathematical Logic, 1, 229–387.
Kripke, S. A. (1965). Semantical analysis of intuitionistic logic I. In J. Crossley & M. Dummett (Eds.), Formal systems and recursive functions (pp. 92–130). Amsterdam: North-Holland.
Largeault, J. (1993). Intuition et intuitionisme. Paris: Vrin.
Martin-Löf, P. (1984). Intuitionistic type theory. Naples: Bibliopolis. Notes taken by Giovanni Sambin of lectures given a Padua, 1980.
Mendelson, E. (1963). On some recent criticisms of Church’s thesis. Notre Dame Journal of Formal Logic, 4(3), 201–205.
Mendelson, E. (1990). Second thoughts about Church’s thesis and mathematical proofs. Journal of Philosophy, 88(5), 225–233.
Molk, J. (1885). Sur une notion qui comprend celle de la divisibilité et sur la théorie de l’élimination. Acta Mathematica, 6, 1–166.
Molk, J. (1904, 1907). Nombres irrationnels et notion de limite. Translated, expanded, and emended version of A. Pringsheim’s German original, Chapitre 1–3. In J. Molk (Ed.), Encyclopédie des Science Mathématiques Pure et Appliquée (Vol. 1)—Arithmétique, Fascicule 1 (August 10, 1904, pp. 133–160), Fascicule 2 (May 20, 1907, pp. 161–208).
Myhill, J. (1967). Notes towards an axiomatization of intuitionistic analysis. Logique et Analyse, 35, 280–297.
Myhill, J. (1968). Formal systems of intuitionistic analysis I. In B. van Rootselaar & J. F. Staal (Eds.), Logic, methodology and philosophy of science III. Proceedings of the third international conference for logic, methodology and philosophy of science, Amsterdam, 1968 (pp. 161–178).
Myhill, J. (1970). Formal systems of intuitionistic analysis II: The theory of species. In A. Kino, J. Myhill, & R. E. Vesley (Eds.), Intuitionism and proof theory. Proceeedings of the summer conference, Buffalo, 1968 (pp. 151–162). Amsterdam: North-Holland.
Péter, R. (1959). Rekursivität und Konstruktivität. In A. Heyting (Ed.), Constructivity in mathematics (pp. 226–233). Amsterdam: North-Holland.
Rogers, H. (1967). Theory of recursive functions and effective computability. New York: McGraw-Hill.
van Rootselaar, B. (1970). On subjective mathematical assertions. In A. Kino, J. Myhill, & R. E. Vesley (Eds.), Intuitionism and proof theory. Proceeedings of the summer conference, Buffalo, 1968 (pp. 187–196). Amsterdam: North-Holland.
van Rootselaar, B., & Staal, J. F. (Eds.). (1968). Logic, methodology and philosophy of science III. Proceedings of the third international conference for logic, methodology and philosophy of science. Amsterdam: North-Holland.
Scarpellini, B. (1971). Proof theory and intuitionistic systems (Lecture notes in mathematics, Vol. 212). Berlin: Springer.
Sundholm, G. (1983). Constructions, proofs and the meaning of the logical constants. Journal of Philosophical Logic, 12, 151–172.
Sundholm, G. (1984). Brouwer’s anticipation of the principle of charity. In Proceedings of the Aristotelian Society, 85(1984–1985), 263–276.
Sundholm, G. (2011). The vocabulary of epistemology, with observations on some surprising shortcomings of the English language. In A. Reboul (Ed.), Philosophical papers dedicated to Kevin Mulligan, Genève. www.philosophie.ch/kevin/festschrift/Sundholm-paper.pdf.
Sundholm, G. (2013). Demonstrations versus proofs, being an afterword to constructions, proofs, and the meaning of the logical constants. In M. S. van der Schaar (Ed.), Judgement and the epistemic foundation of logic (pp. 15–22). Dordrecht: Springer.
Sundholm, G., & van Atten, M. (2008). The proper explanation of intuitionistic logic: On Brouwer’s proof of the Bar theorem. In M. van Atten, P. Boldini, M. Bourdeau, & G. Heinzmann (Eds.), One hundred years of intuitionism (1907–2007). The Cerisy conference. Basel: Birkhäuser.
Tait, W. (2006). Gödel’s interpretation of intuitionism. Philosophia Mathematica (III), 14, 208–228.
Troelstra, A. (1969). Principles of intuitionism (Lecture notes in mathematics, Vol. 95). Berlin: Springer.
Troelstra, A. (1980). The interplay between logic and mathematics: Intuitionism. In E. Agazzi (Ed.), Modern logic. A survey (pp. 197–221). Dordrecht: D. Reidel.
Troelstra, A., & van Dalen, D. (1988). Constructivism in mathematics (Vol. I). Amsterdam: North-Holland.
Vesley, R. (1970). A palatable substitute for Kripke’s schema. In A. Kino, J. Myhill, & R. E. Vesley (Eds.), Intuitionism and proof theory. Proceedings of the summer conference, Buffalo, 1968 (pp. 197–207). Amsterdam: North-Holland.
Zermelo, E. (1908). Neuer Beweis für die Möglichkeit einer Wohlordnung. Mathematische Annalen, 65, 107–128.
Zweig, S. (1979). The right to Heresy. In Erasmus and the right to Heresy. London: Souvenir Press (orig. edition Constable, 1936).
Acknowledgements
I was an invited speaker at the Joint Session in Paris and spoke on the notion of function in constructive mathematics. However, problems of health in 2007–2008 unfortunately prevented me from submitting anything to its Proceedings, whence it was a pleasant surprise, as well as a challenging task gladly undertaken, when Michel Bourdeau and Shahid Rahman requested that I write an introductory essay for the Proceedings volume. Accordingly, in these Afterthoughts I return to some of the things I said in my Paris talk in 2006, as well as present later reflections, caused by rethinking some of the issues and rereading many of the original sources. The material on Brouwer’s Creating Subject that is presented here was not part of my Paris lecture. It stems from research carried out during a Visiting Professorship at Lille, February to April 2012, and I am grateful to my host Shahid Rahman and his students for being such a keen audience. The criticism of the Kreisel-Troelstra-Dummett account was first presented in a Lille seminar April 5, 2012, with, appropriately enough, several of the participants of the Paris Joint Session also present, to wit, my Paris hosts Van Atten, Bourdeau, and Fichot.
I am indebted to Yannis Moschovakis for his valuable comments in the Paris discussion, but above all for sharing with me his correspondence with Alonzo Church and granting permission to publish this important document. I am also indebted to Thierry Coquand for discussion of Heyting’s views, as well as for providing me with a copy of the little known paper by Skolem that is referred to in his contribution to the present volume. Andrew Hodges and Tim Krabbé answered questions respectively on Alan Turing and on Langstaff. Michèle Friend gave helpful comments on the first, non-technical part. Furthermore, as always in recent years, I am indebted to Mark van Atten and Per Martin-Löf for stimulating conversations and valuable comments. In particular, Van Atten, by means of incisive questioning, forced me to revise my formulations on Leibniz and calculemus. He, as wel as Zoe McConaughey, helped greatly in producing the final draft of the manuscript. The IHPST, Paris, in the persons of Michel Bourdeau and Jean Fichot, offered generous hospitality on two occasions in May and November 2012.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Additional information
Dedicated to Dirk van Dalen on the occasion of his 80th birthday.
‘inexorable logic and resolute constructiveness’
Appendices
Appendix
Correspondence between Yannis Moschovakis and Alonzo Church in 1968.
Professor Moschovakis reviewed four papers on Church’s thesis for the JSL. The papers were ‘Quelques Pseudo-Paradoxes de la “Calculabilité Effective”’ by Jean Porte, ‘An Argument Against the Plausibility of Church’s Thesis’ by Laszlo Kalmár (1959), ‘Rekursivität und Konstruktivität’ by Rózsa Péter and On some recent criticism of Church’s Thesis by Elliott Mendelson (1963).
The review, which is highly relevant review to our topic, was printed in The Journal of Symbolic Logic, Vol. 33:3 (Sep., 1968), pp. 471–472. Many of the topics addressed in Moschovakis’ review and in the ensuing correspondence have been addressed in the main text of my paper, though I deliberately refrain from discussing Kalmár’s non-plausibility argument against Church’s Thesis that is conducted in terms of a purported counter-example. In his brief article Kalmár discusses or makes use of many themes that have been covered, for instance, the use of Kleene’s set K, definition of functions by means of undecided separation of cases, and the nature of assumptions that something is known. He also makes use of an assumption analogous to Kreisel’s reading of CS in terms of the existence of an ‘enumeration’ of demonstrations. A proper treatment of the complex dialectical structure of Kalmár’s reasoning, together with a review of the not inconsiderable discussion that was provoked by his paper, would double the length of the present paper. Accordingly, in order not to try the Editorial patience beyond endurance, it shall be left for another occasion.
I. Holograph letter from Moschovakis to Church, submitting the review of the four papers.
March 15, 1968
Dear Prof. Church,
…
You might be interested in one of the mathematical points that originally caused me some difficulty in writing this up and which I still have not resolved entirely to my satisfaction. Kalmár’s argument appears silly on first reading and may very well be silly through and through. It is rather close, however, to some of the arguments that Brouwer used in his later years concerning the so-called ‘creating agent’. Kripke has extracted from these arguments the following principle, whose formal version is sometimes called Kripke’s Schema:
if P is any proposition, then there exists a (constructive) sequence k 0, k 1, … of integers such that P is true if and only if some k i = 0.
Apparently Brouwer’s motivation is that the sequence k 0, k 1, … can be ‘constructed’ (empirically and not by a mechanical procedure) by the ‘creating agent’ in his effort to find proofs for P; he sets k n = 0 if at time n he has found a proof. This is very close to Kalmár’s argument, except that Kalmár uses classical reasoning to obtain his ‘paradoxical’ conclusion. This is a very big difference, since the entire justification for Kripke’s Schema (to the extent that it can be justified) lies in the inuitionistic interpretation of absurdity: P is absurd if no proof for P can be found (by any creative agent, in all time, presumably). In the end I decided that the explicit use of the classical ideas by Kalmár made his argument sufficiently different so I left the analogies with these ideas of Brouwer out of the review. But it is interesting to note that within the kind of intuitionistic mathematics that accepts Kripke’s Schema, Kalmár’s algorithm is acceptable. (Kripke’s Schema has been used to violate formal versions of Church’s thesis in systems with variables for ‘constructive’ sequences by Myhill and Kreisel, I believe.) I do not know if Kalmár knew of the Brouwer ideas and whether he was influenced.
Sincerely yours
Yannis N. Moschovakis.
II. Typed reply by Alonzo Church to the above letter.
April 15, 1968
Dear Professor Moschovakis,
This is just to thank you again for your review of Porte, Kalmár, et. al., and to make in partial reply to your letter the following historical remarks.
1. ‘Church’s Thesis’ was originally proposed (Bulletin of the A.M.S. vol. 41(1935), pp. 332–333) in the context of classical mathematics, with no thought of relating it to intuitionism or other form of constructivism, either in the sense of requiring a constructive proof or constructive interpretation of the existence proposition that was in question, or in the sense of using the thesis as a means of characterizing the (or a) notion of constructive proof. Indeed in the historical context of the date it might well be said that the notions of calculability (the adjective ‘effective’ is superfluous) and provability had long existed in a pre-formal way in classical mathematics. But it can at most very doubtfully be said that a notion of constructive provability existed in classical mathematics. Kleene later proposed to use the thesis in order to make a classical study of the notion of intuitionistic proof. This was done without altering the thesis by reconstructing its existential quantifier intuitionistically; and this led to objections from Heyting, who of course held that the existential quantifier must be so reconstructed.
2. Though I have no definite information, I think it unlikely that Kalmár’s argument was suggested or influenced by the ideas of Brouwer to which you refer. This is simply on the ground that Kalmár’s mathematical publications have never shown any great concern with | intuitionism. And certainly his argument in the paper under review, as you report it, is the very antithesis of intuitionism. That is, he assumes in effect that, for every x, either there is a proof of Ax (by some correct means) or there is a proof of the negation of Ax (by some correct means, in each case). And this is a special case of, and clearly kindred in spirit to, Hilbert’s principle of the solvability of every mathematical problem, which Brouwer once so roundly denounced. I am not familiar with the Myhill-Kreisel paper to which you refer, but I suppose that their proof can hardly proceed in a way that parallels Kalmár’s, or at least not unless they take Hilbert’s principle or some special case of it as an axiom.
Very sincerely yours
Alonzo Church.
Added Note, April 2014
-
1.
In the paper I follow Van Dalen’s use of the negative formulation of Kripke’s Schema. However, the ‘positive’ version of the principle
$$\displaystyle{ (X: \mathbf{prop})((\exists \upalpha: \mathbf{N} \rightarrow \mathbf{Bool})[X \Leftrightarrow (\exists k: \mathbf{N})(\upalpha (k) = _{\mathbf{Bool}}\mathbf{t})]) }$$is more elegant and, in view of the decidability of = Bool , would work as well.
-
2.
The function P: (Bool)prop that allows us to go from a boolean truth-value to the matching proposition.
$$\displaystyle\begin{array}{rcl} P(\mathit{true})& =& \top: \mathbf{prop} {}\\ P(\mathit{false})& =& \perp: \mathbf{prop}. {}\\ \end{array}$$It is well known that the Law of Excluded Middle
$$\displaystyle{ A \vee \neg A\ true\ (A: \mathbf{prop}) }$$is equivalent to having a (unary) truth-value function β: prop → Bool such that
$$\displaystyle{ [P(\upbeta (A)) \leftrightarrow A]\ true. }$$Per Martin-Löf (email March 30, 2013) commented that the analysis of the Theory of the Creating Subject weakens this version of the Law of Excluded Middle by replacing the demand for the unary function β from prop to Bool to the demand for a binary function α, from prop and N to Bool, such that
$$\displaystyle{ [(\exists n: \mathbf{N})P(\upalpha (A,n)) \leftrightarrow A]\ true }$$instead. ‘One could say’, so Martin-Löf, ‘that by an exact analysis of the mathematical content of the theory of the Creating Subject, you unravel it as a weakened form of the Law of Excluded Middle.’
-
3.
Mark van Atten (January 2014) drew my attention to the fine analysis of the theory of the Creating Subject offered by Anne Troelstra (1980) in ‘The interplay between logic and mathematics: intuitionism’. Troelstra notes (pp. 208–2099) that, with given function constants \({ \uppsi }_{A}\), the Kripke equivalences \(A \leftrightarrow \exists x({ \uppsi }_{A}x = 0)\) can be demonstrated from classical comprehension axioms, and that Kripke’s Schema does not contradict classical logic. My principal contribution here is to provide such closed Kripke functions using the classical verification-object for Kripke’s Principle.
Rights and permissions
Copyright information
© 2014 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Sundholm, G. (2014). Constructive Recursive Functions, Church’s Thesis, and Brouwer’s Theory of the Creating Subject: Afterthoughts on a Parisian Joint Session. In: Dubucs, J., Bourdeau, M. (eds) Constructivity and Computability in Historical and Philosophical Perspective. Logic, Epistemology, and the Unity of Science, vol 34. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-9217-2_1
Download citation
DOI: https://doi.org/10.1007/978-94-017-9217-2_1
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-017-9216-5
Online ISBN: 978-94-017-9217-2
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)