# Given proofs of A → B and A, when do we get a proof of B?

In intuitionistic mathematics, a proposition is true only when a proof of it has been experienced. Following the BHK semantics, a proof of A → B is an algorithm that, when given a proof of A, will yield a proof of B. So, with a proof of A → B and a proof of A, there is an obvious way to get a proof of B.

My question, though, is about when a proof of B is experienced. Is it enough to think of the algorithm, think of the proof of A, and juxtapose the two? Or do I have to actually compute the proof of B into a normal form? Note that the question is recursive: given that the proofs of A → B and A are themselves proofs, must we have normal forms of these to conclude anything meaningful?

I'm thinking of this in terms of Martin-Löf type theory. There, we might think of this as a distinction between lazy evaluation and eager evaluation. Strong normalization holds for MLTT (and any reasonable type theory for use in mathematics), so there is no formal difference between them. However, if the proof `f` of A → B is complex and the proof `a` of A is large, we find quite a distinction between the unevaluated `f a` and the corresponding evaluated proof of B.

Maybe this is just a question of definition of “proof”, and both make sense. I can also imagine there being differing opinions by different philosophers, so I'm interested in any answers.

• Question: is "BHK semantics" the same thing as "Heyting semantics", the latter as discussed in "Proofs and Types", Girard,LaFont,Taylor irif.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/biblio/… Their discussion interprets (as I understand it) A-->B as a map from proofs of A to proofs of B, but not necessarily a constructive map. Whereas your discussion (and googling BHK) makes it definitely constructive.
– user19423
Sep 5 '16 at 3:40
• Yes, they are the same. “constructive” is implied in type theory. For the purposes of this question at least, proofs of A → B must be constructive. Also, if I'm thinking correctly, given that proofs are shaped like finite trees, the maps we can think of and constructive maps should coïncide. Sep 6 '16 at 17:56
• are you asking whether proofs must have normal forms, or whether the results of "evaluating" proofs must? insofar as a proof is an algorithm, I'm inclined to think proofs ned not have normal form, but their results must. think of 2+2 v. 3+1. normal form of result: 4. But you could use different algorithms in each case. I'm not sure if such algorithms could be reduced to a normal form algorithm. It doesn't feel right, but I admit it's over my head.
– user20153
Sep 8 '16 at 23:38
• @mobileink, I'm assuming that each proof has a normal form, and essentially asking whether imagining a non-normal form is enough to be able to say that the proposition is intuitionistically true. Sep 11 '16 at 13:50
• ok. let S be a proposition. suppose we have 2 proofs of S, p1 and P2. What would it mean for "each proof" to have normal form? if they have the same normal form, they're (effectively) the same proof in different forms, just like 2+2 v. 4. if they have different normal forms how can they prove the same thing? (fwiw I'm not sure, but i believe we cannot show that for every proposition there is at most 1 proof.) as to eval strategy (lazy v. strict), that has no effect on validity. if you can "imagine" a proof of any form that indeed constructs the conclusion then you can claim it is true.
– user20153
Sep 12 '16 at 3:33

Intuitionism is broader than the kind algorithmic constructivism you are identifying it with. The proof has to exist in the abstract sense that we are certain that given enough resources one could construct it. We don't have to construct it for every case, or provide a convergent single algorithm that handles all the cases uniformly. We just have to prove we could do so for any given case.

We have to experience closure about our ability to find the proof. We are only trying to be very certain that we are not courting potential contradiction of future intuitions by constructing the proof. We are not requiring that it be mathematically useful or fully formalize it in an algorithm. So just knowing A -> B and A really is enough -- not because of the formalism, but because given those, we know we can append the proofs and get a proof, whatever the arising issues of the actual expression happen to be (e.g complexities of the internal mapping issues between parameters used in the two algorithms.)

This becomes exceptionally relevant when it comes to saying things about real numbers. We can prove something intuitionistically about all real numbers by dealing with any arbitrary sequence of digits. But, of course, the entire proof could never be written without naming off the sequences, which is impossible. So theoretically, there could be an ever-increasing quantity of work lining up the variables in the two proofs, for larger and larger domains of application, and we don't want that to matter.

Most constructivists would require more: a convergent process with a fixed number of inputs that can get us as close as necessary to the result, so that simply executing it longer will always get us as close as possible. (So the concatenation step that joins the proofs of A -> B and A itself would have to actually be done, and any weirdness involving different numbers of parameters being mapped together could matter.)

In that kind of constructivism, the real numbers as points don't, in some sense, exist. Only the reals as a structured continuum do.

Brouwer, in his motivation from the two experiences of time, clearly thought that both were relevant. And he tried to explore the basic intuitions of the continuum in ways that modern constructivists usually consider non-constructive, via the intuition of 'lawless choice sequences'. Constructivists whose goals go beyond intuitionism would generally only consider 'lawful choice sequences' to have relevance, and consider a real number only as the artificial convergence point of a set of rationals.

• “But, of course, the entire proof could never be written without naming off the sequences”. Why? We prove stuff about all natural numbers all the time, without naming all of the natural numbers. The proof is an algorithm that takes an arbitrary number as input, and produces a proof for that number. All that changes in the case for real numbers is that the algorithm takes a real number (typically represented as a function of some sort, probably with some extra properties). We can talk about a function without explicitly listing out its range. Sep 6 '16 at 22:42
• Also, “We are only trying to be very certain that we are not courting potential contradiction”. That seems exactly not the point, unless you have some further explanation. Intuitionism is about being able to imagine any valid proof, not getting what we can out of mathematics until we reach ⊥. Sep 6 '16 at 22:46
• OK, but choice sequences are a different kind of representation of a real number than a modern constructivist would accept. It introduces a second layer of infinity, and you can only exhaust one. By constructivist standards there is no place for handling all infinite sequences of digits, in this way, without involving convergence. The constructive proof has to have a tolerance where it stops. The intuitionist one doesn't. I am trying to capture the distinction you are ignoring. The point in constructivism is being constructive. The point in intuitionism is safe elaboration of intuition.
– user9166
Sep 7 '16 at 1:50