Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Mike asked a question on Math Overflow, and also on the constructive mathematics mailing list (where I saw it), concerning whether it is possible to prove, for any pointwise continuous map with , and any , that there is an such that .
My thought is that this might be neither true nor false. For it seems impossible that there could be a counter-example: how one could possible prove that a function is continuous if there is a provable gap in it?! That the IVT itself is provably false constructively is reasonable, because one can imagine that one can come provably arbitrarily close to zero, without provably hitting zero. But proving that there is a gap is a completely different matter; I cannot see any way in which one could possibly demonstrate continuity in that case.
On the other hand, giving a constructive proof seems very difficult as well. Continuous functions are just too wild locally in general. The only control that one has is around the points and . To be able to give a proof of the approximate IVT, one would need to be able to ’squeeze’ in towards . And it seems to me impossible to do this constructively in a way which ensures that one is squeezing above a certain distance each time; and if one does not have the latter property, then one cannot guarantee that one will end up sufficiently close to zero.
This is fairly common in constructive mathematics. Even in classical mathematics, it may be impossible both to prove that something is true and to find a counterexample; think of the continuum hypothesis, for example. But it happens a lot more in constructive mathematics.
Of course it’s impossible to construct a counterexample in constructive mathematics, since it is consistent to assume countable choice which makes the theorem provable. My question is therefore at the meta-level: is it provable, or if not, is there a countermodel (not an internal counterexample), analogous to the forcing models in which CH is false.
Sorry, I could have been clearer. What I was getting at is that:
1) I cannot imagine that there could be any model in which the approximate IVT admits a counter-example;
2) I also would be extremely surprised if it is provable.
This is the sense in which I meant that it might be ’neither true nor false’; more accurate, but long-winded, would have been ’not provable but not demonstrably so’. I do not know if there is a standard terminology for this?
The continuum hypothesis and the constructive on-the-nose IVT are slightly different, in that one can demonstrate that they are not provable (i.e. provide a model exhibiting falsity, as well of course as a model exhibiting truth, so that they are, in a sense, ’both true and false’).
Well, if it is not provable, then (in a classical metatheory) there is necessarily at least one model in which it is not true, namely the free topos, in which the true statements are precisely the provable ones. In general this is the content of “completeness theorems” – anything that is not provable admits a countermodel, and conversely anything that is true in all models is provable.
Such completeness theorems do seem to be very dependent on a classical meta-theory to me, and thus I would be inclined to not regard them as presenting an obstruction.
What is your feeling on the matter? Are you inclined to think that it is provable?
My own feeling is that if it is provable in completely plain constructivity, then it will not be through some wizardry. I think that either there is some simple idea which everyone through the ages has overlooked (which would be astounding), or it is not possible. One can possibly reduce and reduce the amount of choice involved so that one obtains a proof in a setting you are interested in, but a proof in completely plain constructivity would be remarkable.
But, to me, even such a proof would be blown out of the water by a counter-model. If there is some model of the real numbers (etc) in which can prove that a ’continuous function’ has a gap, then our intuition as to the definition of pointwise continuity has been woefully misled all these years, as I see it! Do you disagree?
I think you’re misunderstanding the nature of a countermodel. I certainly don’t expect that there is a model in which there is a particular pointwise-continuous function that has a gap. But I think the most likely situation is that there is a model in which the statement “every pointwise continuous function satisfies aIVT” is not assertable, not because there is a particular pointwise-continuous function that violates aIVT, but because the conclusion of aIVT cannot be asserted continuously/computably in its inputs.
However, I wouldn’t bet too much money on that being the outcome. I think it’s not too unlikely that there is a proof that hasn’t been found simply because no one was looking for it: few “constructivists” who are interested in things like aIVT seem to understand why anyone would object to countable choice.
In fact, I wouldn’t even be all that surprised if there is a proof already in the literature somewhere that no one has noticed because they weren’t looking for it.
But I think the most likely situation is that there is a model in which the statement “every pointwise continuous function satisfies aIVT” is not assertable, not because there is a particular pointwise-continuous function that violates aIVT, but because the conclusion of aIVT cannot be asserted continuously/computably in its inputs.
I’m not sure what you mean to say here. The well-known counter-model to the IVT is of the kind you mention. But it is still an actual counter-model, i.e. there is a model (the effective topos, for instance) where the IVT is demonstrably false, building from a weak counter-example which uses a specific function.
I am saying that I suspect that such a counter-model does not exist for the aIVT. I cannot make sense of what you are suggesting should be taken to be the meaning of a counter-model to the aIVT…could you elaborate?
I think it’s not too unlikely that there is a proof that hasn’t been found simply because no one was looking for it
I myself think that it is highly unlikely, but we can agree to disagree! If someone comes up with a proof, I would be delighted to see it: I can’t imagine how such a proof would go, without any use of choice, myself.
My intuition for computable models is not as strong; I’m not sure exactly what happens in the effective topos. But in the topological counter-models that I understand, there is not actually a specific function but rather a family of functions, such as where is constantly 0 on some subinterval . So has a root if and a root if , and each has a root, but the statement “each has a root” is not true internally to the model because there is a discontinuous jump in the position of the root. This is the sort of countermodel that I think is most likely to exist for the aIVT as well.
To be able to use a specific function, one only needs to know (i.e. it needs to be demonstrable in the model) that there is some such that we cannot decide whether or (i.e the negation of is demonstrable). Then we take exactly the single function that you describe, with . The point (the weak counter-model) is that we cannot determine a root of , because if we could, then we could determine whether or . So this example is not something exotic, but something really very natural in a constructive setting (the fact that there is an such that we cannot determine or is rather fundamental to constructive analysis). It is what I was getting at when I wrote that we cannot provably obtain (i.e. construct) a root.
Whereas the aIVT would seem to me to be of a very different flavour. In the above counter-model for the IVT, we begin with an obviously continuous function (what you called ). Something like this is clearly not possible for the aIVT. I cannot imagine that passing from a constructive to a non-constructive setting could ’close the gap’ of a discontinuous function. And I don’t think that one can play logical games here; I think that if there is a counter-model, there will be one for a specific function.
I don’t see any reason to believe that a counter-model would have to be for a specific function. In fact it’s precisely because, as you asy the aIVT has a different flavor, that I think a counter-model with a specific function is unlikely to work.
MO user Matt F. has posted a proposed proof, and I don’t see anything wrong with it yet. The idea is that at the point when we make a “choice” in the proof that uses countable choice, we can instead interpolate between the two options.
I would be delighted to salute human ingenuity if the proof holds (actually, either way I salute the ingenuity of the attempt)!
Everybody seems to think it does hold. However, I am not yet completely convinced about the definition of . For it seems to me that we can construct a weak counter-example to being constructable. As in #11, let be such that we cannot decide whether or (where this has the precise meaning that I described in #11). Let be any pointwise continuous function satisfying the hypotheses such that for some . It seems to me that we cannot decide constructively what should be in this case. For we need to be able to decide what is. For this, we need to be able to decide if or . But if we could decide this, then we could decide whether or not or . But this is demonstrably impossible.
What am I overlooking here?
Your arguments to min are not the same as in the proof. Not that this is a fatal flaw to your argument, but I trust the people who have said on MO the proof holds up. My query is also about the definition of max and min in the constructive setting. Perhaps we can define like so, but we don’t know what it is. Given a proof that such and such a number is separated from 0 and positive, then we could make a definite pronouncement about it… Is this right?
This was a typo (or more precisely something that I failed to remove after changing my mind half way about how to present things), thanks for spotting it! I have corrected the typo now, and also simplified things slightly.
“Deciding what is” doesn’t require deciding whether it is or . Otherwise we wouldn’t be able to “decide” what your is either.
Actually I don’t think “deciding what a number is” is a good phrase to use, since it invokes a feeling of some need like this. All that we need to do with is define it, which means to give either a Cauchy sequence converging to it or a Dedekind cut specifying it. In either case it’s straightforward to define the max and min functions.
I guess I was falling into the trap of trying to decide whether is equal to one or other of the two options. But this I not intuitionistically valid.
Let me try to elaborate, Mike. I agree of course that and can be defined constructively. But I don’t agree that we are then done. In particular, we are not necessarily able to prove what or are equal to.
For a constructive proof of the aIVT, we need to construct an such that . And to me it seems that this can’t be done in general, for the reason I gave: there might be a such that the negation of is provable, and such that . In this case, one cannot prove that or in the manner of the end of the proposed proof, so we cannot construct or , and hence we cannot construct .
In particular, I think that there may be a subtle error in the proof when it comes to trichotomy. What is true is that since , we can prove that either or . And similarly, since , we have that either or . But this is not the same as saying that we can prove that one of the following holds:
1) ;
2) ;
3) .
For suppose that we can prove that 3) does not hold. Then whether 1) or 2) holds depends on whether we proved that is not the case or that is not the case. Constructively, we cannot prove that one of these two things must not be the case.
The trichotomy of 1-3 follows from the two disjunctions that you mentioned before it. The two disjunctions put together tell us that either
My point is that there is no way to constructively to choose between these options, i.e., if one prefers to think of it this way, there is no algorithm which takes and and can tell us which of these four possibilities holds.
If we have a proof of the negation of , then three of these four possibilities contradict it. So the only thing we can possibly give a proof of in that case is that (3) holds. Hence we cannot construct or , etc.
there is no algorithm which takes and and can tell us which of these four possibilities holds.
It is certainly true that there is no function definable in constructive logic that will take as given a real number (nothing in the disagreement is relevant to whether is of the form ) and output “1”, “2”, or “3” with the property that the statement with that number is true, because if there were then it would define a nonconstant function which is not possible. However, for the same reasons there is no function that will take a real number and output “1” or “0” with the property that if it outputs “1” then and if it outputs “0” then , since that would be a nonconstant function . However, the nonexistence of this latter function does not prevent us from proving the true statement “every real number is either or ”, and likewise the nonexistence of the former function does not obstruct the desired trichotomy here.
This is one of the places where traditional “constructivists” often get tied up in knots, because they don’t understand the difference between the disjoint union and the disjunction , or more generally between constructions and proofs. In HoTT language, .
Of course, if we were going to give a definition based on which of the three properties held, then we would be stuck because we would need rather than just . However, that’s not what the proof does. The numbers and are defined without any need for the trichotomy. The trichotomy is only used in order to prove something about these numbers once they have been defined.
Thanks, Mike, this is helpful in clarifying our respective point of views. You agree, then, that this proof does not give any algorithm to produce an such that ? This is what I have been taking to be the meaning of giving a proof of the aIVT the whole time (I suppose that I am a traditional ’constructivist’ in this regard)! In particular, it explains why I do not consider the proof to be a proof in the sense I was looking for.
Indeed, I find the argument rather ’theological’, even when considered in the way you suggest. I mean, take . Suppose that we do not have a proof that or that . Then, since the proof still goes through, we must have a proof that . This meta-implication looks preposterous to me.
Richard, would you agree that (given any real and any positive real ) that or ? Do you conclude that if we do not have a proof that then we must have a proof that ? I don't see why the trichotomy in this proof is any more preposterous.
The proof produces an algorithm until the very end. There are precise formulas given for each value of , , , and , and we only have to make a finite number of nondeterministic comparisons to get the final result from the sequence .
In order to conclude that from the trichotomy we have to know that and are false. That’s very different from “not having proofs that they are true”. Indeed one might argue that that difference is at the very heart of constructivism.
It is an interesting question, though, whether we can prove aIVT with an untruncated existential. That is, Matt’s proof is that ; can we prove instead ?
Hi Toby, thanks for joining in the discussion. I am very interested to hear your thoughts.
Do you conclude that if we do not have a proof that then we must have a proof that ?
I would not make this conclusion. Recall that I am regarding proof as the same as a construction, i.e. having an algorithm. Then there is simply no relationship between not having a proof that , and having a proof that . I might not know enough about to be able to prove either of these things.
would you agree that (given any real and any positive real ) that or ?
I do not agree that there is an algorithm that given , tells me whether or .
I do agree that one can give a proof in a less constructive sense, which is the one everyone else is thinking of. This proof uses the fact that can be built out of rationals in some way. Now, given , I do not have an algorithm to find how it can be built out of rationals. So I do not know how to apply this proof.
A good example is something like the real number , for some real number . If we had an algorithm to find what is given , we would have an algorithm for showing that or for any , which is impossible. We only know that is built out of rationals in some way, and we have a proof that works for anything built of rationals.
So, in my view, one can see it as a form of choice, when proving something like or , that one is ’picking’ out a way to build from rationals, even though one doesn’t have an algorithm to do it.
I am actually really interested in people’s views on whether they consider the following preposterous. Forget about the background here for a moment, and just take the statement on its own.
if we do not have a proof that then we must have a proof that ?
Regarding the following…
The proof produces an algorithm until the very end.
…perhaps what I have written above helps explain why I do not agree.
There are precise formulas given for each value of , , , and .
Yes, they are precise formulas, so they define some real number, but, as above, there is no algorithm to tell us which real number they define, and so we do not get an algorithm with allows us to compute .
I’m not playing the contrarian here, these are my genuine views! I am very interested in others’ thoughts, and hope that people will continue to contribute.
Posted the above before reading Mike’s last comment.
In order to conclude that from the trichotomy we have to know that and are false. That’s very different from “not having proofs that they are true”. Indeed one might argue that that difference is at the very heart of constructivism.
Yes, I was very careful to use the term ’meta-implication’. I am not arguing that we can prove anything in the model. I think that I wrote is perfectly reasonable on the meta-level: we have a proof that one of three things holds, we do not have a proof that two of them hold, so if we are saying that the argument goes through, then there is only one possibility…
(Note that there is no (meta-)contradiction here. Whereas having a proof that one of three things holds and not having a proof of any of them is a (meta-)contradiction.)
Perhaps it will help if I paraphrase the meta argument. Suppose it is known for certain at the present time that there is a green ball, a red ball, or a blue ball in a bag. Suppose that it is not known for certain at the present time that there is either a green ball or a red ball. Then, since we are certain at the present time (i.e. we are not allowing the possibility of further information coming our way) that we must have one of the three balls, it must be a blue ball.
Re #30, no, that doesn’t follow at all. It is possible to know that one of three things must be true without knowing which of them is true. For instance, I know that at this moment there are either one, two, or three people asleep in my house, because there are four people total, Rena is asleep, and I am awake; but because Megan and Arthur are in another room I do not know which of the three possibilities obtains.
The “interesting question” in my #27 is false, by the way. Consider . For the only approximate roots (for sufficiently small) are , and for the only approximate roots are . If there were an untruncated proof of aIVT, then there would be a function assigning to each an approximate root of , but this is impossible to do continuously.
@Richard #28:
Do you conclude that […]
I would not make this conclusion.
But presumably you would hypothetically conclude that from
(given any real and any positive real ) that or ?
which you apparently do not really accept:
I do not agree that there is an algorithm that given , tells me whether or .
Although that's not exactly what I asked, because constructive mathematics isn't necessarily about algorithms.
Even in a computable model of constructive mathematics, an algorithm doesn't take a real number as input but rather takes a computable representation of a real number, and then there is an algorithm that tells you whether or (assuming that is also given by a computable representation and you have a proof that to refer to; I'll use for a positive integer to keep it simple).
I suppose that the details will vary with the model, but in the one that I keep in my head, a real number is given by an algorithm that, given a positive integer , returns an integer , in such a way that for each and . (The idea is that is within of the rational number .) Then to decide whether the real number given by such an algorithm is greater than or less than , it is sufficient to compute ; if , then , and if , then .
Of course, different algorithms can given equal real numbers. (The algorithms and define equal real numbers iff for each .) Certainly there is constructively no function (understood as an extensional function preserving this equality) that given , returns or such that if and if . It would be asking too much of the algorithm to expect it to be extensional like that.
But perhaps we should set that aside, since I think that I see a more serious issue …
@Richard #28 still:
A good example is something like the real number , for some real number . If we had an algorithm to find what is given , we would have an algorithm for showing that or for any , which is impossible.
I can't imagine why we would have such a thing.
It occurs to me that perhaps you are coming from outside the mainstream of Bishop-style constructivism, which is how I usually write, and so you might not know what we (meaning at least me, Mike, and Matt F.) mean by and . I agree that you cannot take a Kuratowski-finite set of real numbers, such as , and expect to find a literal minimum element in constructive mathematics. Yet when we write , it does look as if we expected to do that. However, when we write , we are actually merely extending the honest-to-goodness-minimum binary operation on the rational numbers to the real numbers, in the same way that we write to extend the addition operation on the rational numbers to the real numbers; perhaps it would be more honest to write instead. Anyway, it is not intended to be a constructive theorem that or , even if we call it . So we can compute without deciding whether or .
If you doubt this, then I offer you a challenge. Specify, in whatever way you feel appropriate, a real number , and I will specify in a similar way. Even if I can't tell you whether or . Then you will see I mean by that.
Once you understand what we mean by and , then I think that you'll agree that Matt F.'s proof is algorithmic until the end, and then we can get back to worrying about whether it is valid to say that or .
@Toby #32
That’s a nice representation of reals :-)
I will reply to other things later, but I just wished to say (assuming that I am making correct deductions from the first paragraph in #31): congratulations on the birth, Mike!
Thanks Richard! Rena Faye Shulman was born a few weeks ago.
Toby’s representation of reals as sequences reminds me of this one.
Regarding the meta-argument in 29-30, there is one situation in which it holds, namely the “disjunction theorem” of pure constructive mathematics: if we can prove in the empty context that , then either we can prove or we can prove . But this depends crucially on the context being empty, which is not the case here.
Indeed, congratulations to Mike and Megan! A boy and a girl: that’s wonderful (and what our family has as well). How old is Arthur now?
Arthur is 3 years and a bit — and harder to handle than his sister right now. (-:
Marvellous, I’m happy to hear the birth was successful!
Thanks very much again for your further thoughts, Toby. I’ll respond to things in bits and bobs.
For now, I’ll just respond to your challenge of #33. The issue as I see it has nothing to do with real numbers, it is rather the distinction between intensional and extensional definitions.
Let be defined inductively as follows. Begin with . At the -th stage, multiply by if is a (Mersenne) prime. Stop when, say, (or anything which gives us a number for which not all possibilities below it have been checked at the time of writing to be Mersenne primes or not).
Can you, using a definition of for rational numbers in general (the precise details you can choose as you like), say anything about ?
There’s no reason to stop! In any case, I think the answer is .
There’s no reason to stop!
Do you think so? I actually find that quite interesting. I mean, obviously the induction makes sense without stopping. But are you claiming that we still have a well-defined rational number in that case?
In any case, I think the answer is .
That’s also very interesting, thanks! I need to think some more about it. But if we assume it is correct, are you actually proceeding from a general definition of to obtain this? And if so, is your calculation dependent on something specific about my construction of , for instance the fact that it is inductive? Or are you proceeding more intensionally, using some characterisation of . In the latter case: which characterisation?
Let me also just raise one thing that I had in mind with this example. There could come a point where the computation of is such that we cannot distinguish it from . Maybe we do not have enough paper to write down all the digits to the right of the decimal point before we see a non-zero one. Maybe our computer hardware does not allow us to go beyond a certain proximity to zero. So we might not even be able to compute to an extensional rational number to which we can apply the general definition of , which relies on such an extensional description.
This is not ultrafinitism as such: the definition of makes perfect sense as a construction, it is just that we might not be able to arrive at something extensional by carrying out this construction.
Oh, I think I misunderstood your definition. Sorry, I should have read more carefully and thought longer. If you don’t stop, then I don’t think the definition is valid constructively, because without knowing whether the Mersenne primes stop (or even how quickly they peter out) we can’t give a modulus of convergence to make your sequence Cauchy. But if you do stop, then you’ve defined not only a real number but a rational number, and so if and if , since inequality of rational numbers satisfies trichotomy.
No problem! I appreciate that this may be considered heretical, but what I am arguing is that this is not reasonable even in the rational case. Reasonable in the case of being given extensionally (i.e. given as , however one wishes to define this in terms of the integers, for some and ): yes, for the reason you give. Reasonable in the case of being given intensionally: not necessarily, I am arguing.
In that case I guess you are an ultrafinitist. I don’t know of any other kind of constructive math in which inequality of rational numbers is not trichotomous.
Possibly, although I’ve never thought of my views that way. I touched briefly on this in the second praragraph of #42.
I would say more that I am arguing that the difference between intensional and extensional definitions should be taken seriously from a constructive point of view. Perhaps this viewpoint is closer to some kind of modal logic. I actually made a similar point once in a different setting, at the HoTT blog, where we had equal difficulties to here understanding one another, here!
My views actually strike me as an obvious point, I am amazed if others do not consider it so.
In reply to 42, we absolutely can arrive at something extensional by carrying out your construction; it’s just that we haven’t done it yet.
In any case, I think I have no more to contribute to this discussion, since we’re reached the point of philosophical rather than mathematical difference, and on most days I’m not interested in the usual philosophical justifications for constructivism anyway — for me, constructive logic is interesting because unlike classical logic it is preserved by internalizing in arbitrary toposes. But you should be aware that your views seem to be significantly at odds with the vast majority of philosophical constructivists too.
But you should be aware that your views seem to be significantly at odds with the vast majority of philosophical constructivists too.
Yes, I am perfectly aware that these are my views, informed by other points of view of constructivism, but not following any particular one :-)
for me, constructive logic is interesting because unlike classical logic it is preserved by internalizing in arbitrary toposes
I appreciate that, and am aware that you have been given an argument that allows you to prove what you need.
we absolutely can arrive at something extensional by carrying out your construction; it’s just that we haven’t done it yet.
Of course, any intensional constructive definition can in principle be computed to something extensional. My point is simply that we cannot actually carry out Matt’s proof in practise in general. For that reason, I do not consider it to be a constructive proof.
If we all feel that we understand each other, then I guess that we are indeed done. If not, I’ll keep an eye on the thread.
Well, Toby hasn’t said anything since #33, so he might have more to add.
I endorse Mike's answer to the challenge in #40. This is a better answer than the one in #43, since it makes fewer assumptions vis-a-vis finitism. Besides that, it's obtained by general principle, not anything specific to the example at hand.
In fact, I'd try to define as much as possible in the same way that you defined . So is defined inductively, although since we can't compute directly from , you have to keep track of some extra data (well, one extra datum). So begin with , and set the extra datum to . At the -th stage, multiply the extra datum by if is a (Mersenne) prime, and depending on whether the resulting number is positive or negative, let be that number or , respectively. Of course if we go on to, say, (or anything which gives us a number for which not all possibilities below it have been checked at the time of writing to be Mersenne primes or not), then nobody has yet calculated what is, but nobody has yet calculated what is either, so that's only fair.
I suppose that you might object to the step that depends on whether a certain as-yet-uncalculated rational number is positive or negative. But even an intensional definition is only required to say how you would calculate something if you got that far, and this calculation would produce some result if you got there, so we can compute anything that we are actually called upon to compute. (In fact, it's just a matter of whether the number of Mersenne primes below is even or odd, and that's an even simpler inductive definition than anything else that we're considering; it's the easiest of all calculations in this problem.)
Put differently, it’s easy to prove by induction that this definition of works. So if you object to it, you must also object to induction on natural numbers.
Regarding #51 and #52: it seems to me that my point of view still has not been understood. For it is exactly my point that the following course of action…
In fact, I’d try to define
…is not relevant. In Matt F’s proof, one needs a general definition of for a real number (let us change to ). This relies on a representation of as built out of rational numbers. Take any implementation on Matt F.’s proof that you like on a computer. I claim that I will always be able to define an for which that proof will fail to be carried out, because the computer will not be able to get from my intensionally defined to an extensional representation of evaluated on some real number. For that reason, I do not regard it as constructive in the sense I am looking for.
My objection even goes through for the integers. Just change the as I defined it to beginning with , and at the -th stage multiplying by if is a prime, and multiplying by if not.
The point is that can only be defined for a general integer using an extensional representation of as an integer. We do not have such a representation for the I gave. Because is not possible to define for an arbitrary intensionally given , it is essentially useless from the philosophical standpoint that I am taking.
Now, of course, one can define any old integer by hand for a particular , and call it . But there is no way that one can compare this to the defined in the general way. If one defines in a more intensional way, being dependent on being able to prove that or , then of course I accept the definition as valid. But with this intensional definition of , one cannot carry out Matt F.s proof, which relies fundamentally on the extensionality of the definition. I mean, if one imposes on that one can determine whether or for any , so that one can use the intensional definition of , then one is removing the principal difficulty of constructive analysis, and of course one will then be able to give a proof of the aIVT!
I’m afraid this discussion has gone beyond the point where it’s worth my time to try to make sense of what you’re saying. As I said, I’m not really a philosophical constructivist, and the proof is valid in all well-defined systems and models for constructive mathematics that I’m aware of.
As I already wrote in #49, that is fine by me. I am making a philosophical point; people can take it or leave it. Since new comments were made after #49 that indicate a lack of understanding of the point that I am making, I feel it reasonable to respond.
Should anybody be interested, it may help to know that the point of view that I am putting forward is certainly influenced by work on semantics in linguistics. I am very interested in the question of the nature of meaning in mathematics, and many discussions that I have been involved in on the n-café and here have been to do with this. I perfectly understand that most mathematicians are indifferent to the question of whether their daily work is meaningful :-).
Sorry, I should stick to what I said I was going to do and bow out, rather than continuing to stick my oar in and then contradicting myself by claiming that I really have nothing to say. (-:O
Richard, I just don't understand why you claim that the computation in the proof can't be carried out. As we work through your example, we do a bunch of primality testing, some multiplication, some comparison, but at no point are we unable to proceed with the computation. Yes, it's a laborious computation, since you gave a laborious example, but it can always be done.
The only point that I can get out of it is that the computation is not merely laborious but, when carried out far enough, something that literally nobody can actually complete in our physical reality. Fair enough. But I have three objections to the idea that this impugns Matt F.'s proof in any way:
By ’constructivism’, I am simply referring to the philosophy which regards a proof as a construction, a method/recipe. Now, one can take a particular formalist definition which follows this philosophy to a certain extent (which is essentially the setting that Mike is interested in) and call this ’constructivism’. My point of view is that the formalist definition of constructivism that Mike, and I believe yourself, are thinking of, is not truly constructive in the philosophical sense, because it equates intensional and extensional definitions, which I view as without justification (a form of choice).
This is not ultrafinitism (at least in any conventional sense). Ultrafinitism would reject the definition of my , for instance, whereas I regard it as perfectly well-defined. One could prove all kinds of things about , all of which I would regard as perfectly valid constructively. But just because something is well-defined (is intensionally meaningful) does not mean that it computed to an explicit (extensional) integer (or whatever). So we are not justified in replacing by an explicit integer. This much of my philosophy is influenced by ultrafinitism, certainly, but it is far from ultrafinitism per se.
So to write the following is to misunderstand my point of view.
You’re objecting to the function
there’s nothing wrong with the function . We can’t compute for the that you give, because we can’t compute itself.
There is nothing wrong with the function , i.e. I view it as perfectly well-defined (it has intensional meaning). There is a problem if we wish to use it in a way which requires an extensional , i.e. an explicit .
Similarly, there is no problem as such with the function from my point of view, it is just useless, because it relies on an extensional . There is a problem if we wish to use this function with an intensionally defined , because it is not justified to replace this by an extensional (i.e. explicit) integer. To get something useful intensionally, we should instead be looking at the function in context: for instance, .
This isn’t really about the Intermediate Value Theorem
It is entirely relevant. A proof has been proposed, which I am pointing out is not truly constructive from a philosophical point of view, because it relies on equating intensional and extensional definitions, which is not justifiable.
I am pointing out is not truly constructive from a philosophical point of view
You should say instead “I am pointing out is not truly constructive from my philosophical point of view”, because your views are clearly at odds with those of the vast majority of constructivists.
I wrote it the way I did after consideration. For 1) below is part of the definition of constructivism, and 2) below is a fact.
1) In constructivism, the giving of a proof is the providing of a method.
2) It is not possible to give a method to replace an intensionally defined integer (or whatever) by an extensional one
It then follows that a proof which relies on a method for replacing an intensionally defined integer (or whatever) with an extensional one is not constructively valid.
The only place where one’s own views enter is whether or not one chooses to disregard this observation or not. In the formalist approaches to constructivism that have been mentioned, one disregards it. My view is that it should not be disregarded. Whether or not that is a view shared by other people who think of themselves as constructivists is not really of any significance: philosophy is not populism!
Occasionally, however, a little humility is in order. As is a recognition that for better or for worse, a philosophical word like “constructivism” is defined by the consensus of its adherents, at least if meaningful conversation is to be possible.
I am not sure what you perceive as a lack of humility. I have worked with constructive mathematics for years, and am well acquainted both with the literature and with computer implementations. I feel free to form my own independent views. That I have my own view does not of course imply a denigration of the views of others; it is possible to have a viewpoint that is outside of the conventional one without having a lack of humility!
As is a recognition that for better or for worse, a philosophical word like “constructivism” is defined by the consensus of its adherents, at least if meaningful conversation is to be possible.
I have explained very precisely what exactly it is about ’constructivism’ that I am discussing, for instance in 1) of #60, and I think that the latter is not at all controversial. Point 2) may or may not be new, but it is not to do with what constructivism itself is: it is an independent observation. And when we put 1) and 2) together, we obtain something which we may choose to disregard, or may not, when claiming that a proof is ’constructively valid’. Valid in various formal systems that many people call ’constructive mathematics’: yes. Valid according to the philosophy that lies behind constructive mathematics: no, as I see it. Again, this is not a lack of humility, this is drawing a simple consequence from a fact.
By humility I meant a recognition that one might be wrong. In particular, I cannot make any sense of your “fact” (2); I do not know what an “extensional definition” is. I don’t really want to get into an argument about that, just to make the point that what seems self-evident to you may seem like nonsense to someone else.
I have to say that it’s hard for me to believe that you are well-acquainted with the literature and implementations of constructive mathematics, given that at the beginning of this thread you seemed unaware that your views were at odds with practically all other constructivists in the world. If you were aware of that, then I would have expected you to realize that Matt’s proof was given in the context of “standard constructivism” and that I and other readers were also evaluating it in that context and would probably be ourselves unaware that you hold a radically nonstandard philosophical position, and that therefore saying “there is a subtle error in this proof” would be much less helpful in communicating the actual state of affairs than something like “Personally, I would not regard this as constructive, although I’m aware that by the standards of traditional constructivism it is acceptable.”
Regarding intensional and extensional, if those adjectives are to be applied to definitions at all, I would say that all definitions are intensional. Usually however I think they are applied to constructions or properties of objects, an extensional property being one that depends only on the “behavior” of an object (what a traditional mathematician would call “the object being defined”) while an intensional one can depend on how it is defined. So if what you mean by (2) is that there is no method for determining whether two (intensional) definitions have the same behavior (i.e. “yield the same extensional object”), then that is not at all disregarded in ordinary constructive mathematics: in fact it is central to it, namely the fact that not all sets have decidable equality.
The definition of doesn’t require any such extensional information: it starts from an (“intensional”) definition of a number and produces another (“intensional”) definition of a new number . You gave a procedure for computing a number ; from that procedure we can deduce an analogous procedure for computing the number . Neither computation has been carried out, but if you regard the first procedure as defining then the second procedure should count just as well as a definition of . There’s no reason to hold the output to a higher standard of extensionality than the input.
On the other hand, if by an “extensional definition” you mean an expression in canonical form (e.g. a “numeral” like ), then in a variety of constructivism with strong normalization your (2) is false because of your (1): simply normalize a definition until it becomes canonical.
I have to say that it’s hard for me to believe that you are well-acquainted with the literature and implementations of constructive mathematics
I don’t know what motivation you think I might have for claiming this without it being the case! I am not in any case going to attempt to convince anybody of this. If you knew me in person, I think you would not have written this :-).
at the beginning of this thread you seemed unaware that your views were at odds with practically all other constructivists in the world.
The question I was interested in was (and still is) whether there is a constructive proof of the aIVT. By ’constructive’, I had in mind the standard philosophical notion (an aspect of which is 1) in #61). Now, we could avoided some confusion if I had been more attentive and noticed that you were interested in a specific formal system rather than the constructivism more generally: the fact that you used the term ’plain constructivism’, or something like that, was what I was responding to, since what came to my mind with the use of this term was the basic ’philosophical’ constructivism of which 1) in #61 is a part.
I was perfectly aware that my views on what philosophical constructivism allows in mathematical practise are apparently new. It took me a while before I was able to pinpoint where the difference was in the setting of this discussion, and how to put it in a way that would be understood (and the latter may still not have been achieved). In particular, the reason that I suggested that there may be a ’subtle error’ is because the step I was referring to in Matt F’s argument is to me so evidently non-constructive, and I have viewed it in that way for such a long time, that I had forgotten why my reasons that I regard the argument as not constructively valid may not be an obstruction in the formal systems that you are interested in; and, as this discussion is testimony to, the reasons that I regard the argument as not constructively valid seem to appear somewhat subtle to people.
By humility I meant a recognition that one might be wrong.
I am perfectly willing to acknowledge an error in my reasoning if I make one. Since it seems that no-one has actually understood the point I am making, which is a pre-requisite for giving a refutation of it, I’m not quite sure what you expect.
I am not going to respond to #65. I think that I have explained my point clearly enough now for it to be understood, and what is written in #65 does not understand it. I am not interested in endlessly repeating myself, only in having a discussion about something which I find interesting and important. If what I have written already is not sufficient to communicate my point, that discussion will not come about, I feel. In particular, I feel that what I have already written sufficiently addresses #65.
Richard, I believe that Mike is mostly interested in constructivism for its relationship to the internal language of elementary toposes and the like. I'm the one who's interested in it for more philosophical reasons. But I'm afraid that I really don't understand your philosophical position.
This isn’t really about the Intermediate Value Theorem
It is entirely relevant. A proof has been proposed, […]
I didn't mean that it's irrelevant; I meant that your disagreements with us can (and so should) be isolated in something more basic than the IVT. Such as the nature of . You certainly brought them up in an appropriate place.
I believe that I understand the difference between intensional and extensional definition. I'm thinking of the kind of issues in this Stanford Encyclopedia article (despite its focus on classical logic). If this is what you're talking about, then we're on the same page here. Nevertheless, I do not understand what
It is not possible to give a method to replace an intensionally defined integer (or whatever) by an extensional one
has to do with any of this. Where is anyone trying to do anything like that?
In particular, when you write
There is nothing wrong with the function , i.e. I view it as perfectly well-defined (it has intensional meaning). There is a problem if we wish to use it in a way which requires an extensional , i.e. an explicit .
I have no idea why you think anybody is trying to use in this way. I think that you should interpret the appearance of and in Matt F.'s proof in accordance with the well-defined intensional meaning of and , and what goes wrong with that?
Richard, I’m sorry; I didn’t mean to impugn your honesty. I just meant that what you wrote above doesn’t sound to me as though it were written by someone familiar with the literature. I think that if you hold very nonstandard philosophical beliefs that impact the way you do mathematics, it’s incumbent upon you to be aware of exactly how that difference manifests itself, and to check carefully whether that’s the problem before expressing any opinion about the correctness of other people’s proofs.
If this is what you’re talking about, then we’re on the same page here.
Great! I haven’t read through the link closely, but it certainly looks like the kind of thing I’m getting at.
I think that you should interpret the appearance of and in Matt F.’s proof in accordance with the well-defined intensional meaning of and , and what goes wrong with that?
I’m very interested in discussing this. What exactly do you mean by ’the well-defined intensional meaning of and ’? If you mean the one I suggested, where we are working in a context such as , then I mentioned already where I see the problem as being: we certainly do not have such a context for an arbitrary as in Matt F’s argument.
Otherwise, I am not sure what you have in mind. Let us consider again the case of integers, or even natural numbers, for simplicity. Suppose that we regard the natural numbers as defined inductively the usual way: we have a , and given an , we can construct an . Using this, one can define say for an arbitrary given extensional natural number , i.e. one defined strictly in terms of this definition: it is for and , and otherwise (where, to be precise, we use induction to make sense of this ’otherwise’). But this is not much use in practise, because we do not have a method to convert an intensionally defined into an extensional one. This does not have to be a matter of inability to compute, as suggested by ultrafinitism. It could be anything. A young child may for instance be able to count to ten, but may not actually be able to recognise three objects of a certain kind as corresponding to the ’three’ they reach when counting. Or an engineer may have a calculation dependent upon the number of dwellings in an area, which may in turn be dependent on an as yet unpassed piece of legislation, so that there is no way even in principle to replace this intensionally defined number by an extensional one.
As an aside, from this, hopefully it is evident that my answer to the last paragraph of Mike’s #65 would of course be that strong normalisation, which is after all a syntactic notion rather than a philosophical one, would not be something of relevance in the kind of constructive mathematics that I am envisioning.
It seems to me that when discussing children and engineers you have left the realm of mathematics entirely, but I think the point is still valid that you can get out something that’s just as good as what goes in. If the number of dwellings in an area depends on an unpassed law, then will also depend on that unpassed law, but it is just as good a number as is. If the law says that , then , whereas if the law says that , then and . In what sense is any less acceptable than ?
I just meant that what you wrote above doesn’t sound to me as though it were written by someone familiar with the literature.
I can certainly appreciate that it may not be easy to see how I have been approaching the discussion, and that this can have led to miscommunication. Mostly I have been approaching this as an on the fly discussion rather than a treatise on my philosophical views on constructivism, and I have been approaching it from the point of view of my own interest in the original question. Hopefully we can agree that this is natural enough, even if not optimal with regards to clear communication.
but I think the point is still valid that you can get out something that’s just as good as what goes in
And that is my point. Certainly is reasonable to consider in the context of the legislation having been passed. Because this piece of legislation provides us with a means to replace by an extensional natural number. Just as in Matt F’s argument, if we know that or , then of course there is no problem for this particular . But we cannot assume that in general, i.e. we cannot work in an empty context for Matt F’s argument.
It sounds as though you may still be hung up on the point that Toby addressed in #33, namely that “” is not defined by comparing to and checking which of them is bigger. If it were, then yes, certainly, constructivity would require that we know that one of them is bigger before we can make the comparison. The point is that we can define constructively by giving a representation for it as a real number of exactly the same sort as the representations that we are given of and , so that it is just as good of a number as they are, even without knowing that .
This is just like how is just as good of a number as is, even before the law is passed (and hence before we know “extensionally” or whatever “exactly what” and are). You haven’t explained in what sense you see as any less acceptable than itself. We don’t need an “extensional” definition of , whatever that means, in order to give an intensional definition of .
What exactly do you mean by ’the well-defined intensional meaning of and ’?
I wrote that since you claimed that there was one, but in light of
If you mean the one I suggested, where we are working in a context such as
that's not sufficient, at least for real numbers.
That said, is a theorem of Heyting arithmetic. So in that context, at least, when working with natural numbers, there should be no problem with and . This extends trivially to rational numbers, and then the real numbers have a more complicated definition that does not presume but builds on and for rational numbers instead.
one can define say for an arbitrary given extensional natural number
Similarly, is a theorem of Heyting arithmetic, so should be straightforward. Maybe your position is that Heyting arithmetic isn't really constructive by your philosophy, or that it only applies to extensional natural numbers?
Or an engineer may have a calculation dependent upon the number of dwellings in an area, which may in turn be dependent on an as yet unpassed piece of legislation, so that there is no way even in principle to replace this intensionally defined number by an extensional one.
Mike suggested that this is leaving mathematics, but I wouldn't say that. Applied math is still math, and it ought to be able to handle whatever we throw at it; or at least, we ought to have some idea of what we can throw at it that it can handle.
But I still don't understand the objection. If you're willing to accept the number of dwellings in a given area, even though it cannot be pinned down (and I think that one should be so willing), then why not accept the number ? It cannot also be pinned down, but it still has a meaning: the number of dwellings in the area or the number ten, whichever is larger. (It's also useful to prove by induction on that such a number exists, although I would argue that the expression has a meaning regardless.)
Yes, applied math is certainly still math. I guess this is getting into the realms of constructive philosophy that I’ve never understood; maybe some people would consider a child’s lack of understanding of numbers to be a reason that a number might not be well-defined, although to me that makes even less sense than the usual arguments about Goldbach’s conjecture or whatever.
Regarding #75: I consider the example that I gave about a young child’s understanding of numbers to illustrate the point that I am making quite well. The child can count up to say 10, so can define the number three extensionally. If asked, ’how many books are there on the table?’, they understand that the answer to the question should be a number, and they may well be able to answer correctly if the answer is one or two. So the answer for the child is , where has the intensional meaning: number of books on the table. But the child is not able to convert to the extensional number three. This illustrates the only point that I am really making: that there is no method to replace an intensional definition by an extensional one, and hence an argument which relies on having such a method is not, according to the philosophical definition of constructivism, constructively valid.
Regarding #73 and #74: it may be that my use of the context is contributing to confusion, rather than helping. I am perfectly aware that such a context is not needed for the usual (extensional) constructive definition of .
The point is that we can define constructively by giving a representation for it as a real number of exactly the same sort as the representations that we are given of and , so that it is just as good of a number as they are, even without knowing that .
This is true if and are given extensionally. It is certainly not the case if even one of or are given intensionally. Because there is no way to say anything in general what an intensional definition looks like, so there is no method for taking an intensional and/or and producing . This seems perfectly evident to me; it seems to me a basic point about the intensional/extensional distinction, which was already understood by Frege, and no doubt before that as well.
This is just like how is just as good of a number as is
Again, the problem is that, yes, for individual intensionally defined , we may of course be able to cook up a , but there is no method for this. Perhaps you are thinking that if can be defined in a certain context, then so can . But not all examples of the inability to replace intensionally defined numbers by extensional ones are like this. To return to the example of the young child, they may well understand the notion of larger and smaller than for collections of 3 and 5 objects, i.e. they have an intensional definition of , without being to convert these intensionally defined numbers into extensional ones.
I would not dismiss this kind of example, by the way. The literature of mathematical didactics is rich, and through observing the process of learning mathematics, we can understand a great deal about it; doing mathematical research is not the only way to obtain insight into mathematics.
But there are plenty of other examples. For my example involving inability to compute beyond a certain point, you yourselves gave earlier an intensional definition of which you appeared satisfied with at that point. Again, there is no context involved here. So, again, we may be able to define and intensionally, but there is no recipe for this; the three examples we have looked at are completely different from one another.
What exactly do you object to about the usual constructive definition of What about it appears to require and to be “extensional”?
Maybe your position is that Heyting arithmetic isn’t really constructive by your philosophy, or that it only applies to extensional natural numbers?
Exactly.
What exactly do you object to about the usual constructive definition of ? What about it appears to require and to be “extensional”?
Which setting are we working in? Probably it’s best to stick to the natural numbers, to avoid any possible confusion. I gave a definition (in a special case) for the natural numbers earlier in the thread, for . It uses fundamentally the fact that is given extensionally. One can give a similar definition for for arbitrary and . If you prefer a different definition, feel free to present it, and then I will reply.
If you regard a definition like “carry out X procedure for 1 million steps and output the result” as a valid intensional definition of an integer , then why isn’t “carry out X procedure for 1 million steps, if the result is negative then output it, otherwise output zero” just as valid an intensional definition of ?
It seems to me that to a philosophical constructivist, an “intensional definition” must consist of a method for producing an “extensional definition” (this is your (1) in #61). This is the point I intended to make with the comment about strong normalization in #65. A definition of is written in terms of extensional information about and , but it applies just as well to intensional and and produces an intensional result, because intensional definitions denote extensional objects.
why isn’t “carry out X procedure for 1 million steps, if the result is negative then output it, otherwise output zero” just as valid an intensional definition of ?
It is perfectly valid to give a definition of which involves carrying out a procedure for a million steps. However, if we have defined in an extensional way, and then wish to use this extensional definition, we need to first compute to an extensional number, which is not possible. This is very like using just a universal property to prove something about an object in a category, compared to using something ’extensional’ about that object, i.e. where we are using some structure of the object which is not visible from the point of view of category theory alone. We can prove lots of things from intensional definitions without needing to replace them by extensional ones.
an “intensional definition” must consist of a method for producing an “extensional definition”
No. Just think of a category with a natural numbers object. We can perfectly well speak of a natural number without specifying which one it is, and do lots of perfectly good mathematics concerning natural numbers. If we need a theorem about a specific natural number in practise which we can compute, we just plug it in.
In the example concerning legislation, we have a perfectly well-defined natural number intensionally, dependent on the piece of legislation. If we plug in a specific piece of legislation, we get an extensional natural number. But we can prove things about the intensional natural number without relying on any specific piece of legislation.
I would also like to not lose sight of Matt F’s argument here. I still think that my original weak counter-example of #14 is a valid objection. If you accept that there could be an for which it is not decidable whether or , which I would think would be completely uncontroversial in any form of constructive analysis, then I still think that, from a philosophical point of view, the logic involving trichotomy is nonsense: one cannot get something for nothing.
I mean, it is clear that if it is not decidable whether or , then two of the possibilities in the trichotomy are impossible to demonstrate. Would you really claim, therefore, Mike and Toby, that there is a method to show that is less than whenever or is not decidable? If not, then how do you proceed to the next step of the induction?
Would you really claim, therefore, Mike and Toby, that there is a method to show that is less than whenever or is not decidable?
The method is that you compute an approximation to that is sufficiently good to ensure that one of the three possibilities holds. The fact that is defined constructively means (by definition of “real number”) that it can be approximated arbitrarily closely by rational numbers, and we know how to compare rational numbers. In this case It suffices to get closer than . The difference with “ or ” is that no finite distance of approximation is sufficient to ensure that one of those two possibilities holds, essentially because they are closed rather than open conditions.
We can perfectly well speak of a natural number without specifying which one it is, and do lots of perfectly good mathematics concerning natural numbers.
It sounds like you are confusing the assumption of an arbitrary, unspecified, natural number with the definition of a specific natural number. To define a specific natural number, constructively, we must specify it. But we are free to assume a variable in the context without giving it a value, such as when proving a statement of the form “for all …”.
It is perfectly valid to give a definition of which involves carrying out a procedure for a million steps. However, if we have defined in an extensional way, and then wish to use this extensional definition, we need to first compute to an extensional number, which is not possible.
Are you saying you don’t have a problem with the definition of , but only object if it has to be “used extensionally”? What does “used extensionally” mean?
Regarding #84: I don’t think this answers my question. If we cannot prove that and we also cannot prove that , then we certainly cannot prove that either of the strict inequalities holds either. Now Matt F is using that either one of these two strict inequalities holds, or else ; and he relies on one of these three statements being true to proceed to the next step of his inductive argument. So either we have to conclude that , or we cannot proceed in this case to the next step of Matt F’s inductive argument.
@Richard #78:
Maybe your position is that Heyting arithmetic isn’t really constructive by your philosophy, or that it only applies to extensional natural numbers?
Exactly.
OK, that is very interesting. I think that it's fair to say that Matt F.'s proof is intended to apply to functions between numbers that can be approximated by [differences of ratios of] numbers to which Heyting arithmetic does apply.
I can accept that you have a notion of natural number for which Heyting arithmetic is invalid, in particular in which the theorem is invalid. I'm still not clear on your philosophical objection to the binary operations and on these numbers. While one certainly could consider a system of arithmetic that lacks them, I'm interested in your philosophical reasons why one should use a system of arithmetic that lacks them.
It's not merely that you can't define them using more primitive operations. Consider that in Robinson arithmetic, and even in first-order formulations of Peano arithmetic or Heyting arithmetic, one is unable to define addition and multiplication, so one puts them in as primitive operations. Similarly, if one is unable to define and , then they could be put in as primitive operations. I justify doing so on the grounds that they are even more basic than addition and multiplication; if arithmetic is about operations on natural numbers, then these are about the most basic operations that one could consider.
So I would ask you not to think of the definition of by cases depending on whether or . Instead, think of the intensional meaning of it, just as you would for or . You seem to do exactly this sometimes:
To return to the example of the young child, they may well understand the notion of larger and smaller than for collections of 3 and 5 objects, i.e. they have an intensional definition of , without being to convert these intensionally defined numbers into extensional ones.
It seems to me that we ought to say and here instead of and , since writing the latter suggests that we've identified these numbers extensionally, which is exactly what the child has not done. But still, the child is able to conceive of , perhaps even able to notice that in this instance. The child would conceive of in the same way that they would conceive of or , by the inherent intensional meaning of those operations.
Now I half expect you to say that you don't believe in or either, at least not when and are only given intensionally. In which case, you have several more fronts on which to attack Matt F.'s proof!
@Richard #83:
I would also like to not lose sight of Matt F’s argument here.
OK, but I'm going to interpret Matt F.'s proof as about real numbers that can be approximated arbitrarily well by rational numbers for which is true. Thus breaking the acceptance of it into parts: the stuff in my previous comment, and the stuff in this commment.
Would you really claim, therefore, Mike and Toby, that there is a method to show that is less than whenever or is not decidable? If not, then how do you proceed to the next step of the induction?
If we're talking about real numbers, then yes. I'm a little leery about accepting undecidability as a proposition; a fact known to be true should remain true even as I gain additional information, and undecidability doesn't behave that way. Still, yes, in practice, because I believe the (a priori stronger) statement that or , in the sense that I can decide which with enough work.
First, since , we have a natural number such that . Now approximate and with rational numbers to within . (If you can't do that, then to my mind, you don't have real numbers to begin with.) That is, I have rational numbers and such that and . Since and are rational, either or . If , then , so ; if , then , so . Either way, or .
You seem to be confusing “don’t have a proof of” with “know to be false”. My 84 and Toby’s 89 explain how, even if we don’t start out having a proof of or of , we can produce a proof of one of the three statements in the trichotomy. Depending on which of the three trichotomous statements we end up proving, it could be that we will end up also obtaining a proof of or of . But that doesn’t contradict the fact that we didn’t used to have a proof of either of those.
We have to be careful to separate the theory from the metatheory. If there is a real number definable in the empty context such that we can prove, as a meta-statement about our theory, that it is impossible to prove that and also impossible to prove that , then because we can prove that or , and because pure constructive logic satisfies the disjunction property for proofs in the empty context (if we can prove “P or Q” then we can either prove P or prove Q), it must be that we can prove . But this “reasoning about proofs” only works in the metatheory, and only in the empty context.
As for the legislation example, I would really prefer to restrict to mathematical statements, but I can try to translate over there. If we know for sure that the legislation will be passed (say) next summer, then there is a method to compute the number: just wait until the law is passed. If we don’t know that any relevant legislation will ever be passed, then the definition of the number is not constructively valid, just as the definition “ if Goldbach’s conjucture is true and if it is false” is not constructively acceptable.
I think that it’s fair to say that Matt F.’s proof is intended to apply to functions between numbers that…
Yes, absolutely, my interest is in whether it is constructive in the philosophical sense; I completely agree that it was not intended to address these concerns.
Other than that, I think we have reached a point of understanding, which I would like to summarise, and then bow out of the discussion, barring some very new point being raised.
1) In my view, due to meta-mathematical considerations (justified by an intepretation of philosophical constructivism), the logic of the trichotomy step in Matt F’s argument is not valid, for the reason I have already given several times, lastly in #87.
Note on 1): I entirely accept that the logic can be justified in the formal system that Matt F is working, and more generally whenever one can do the kind of things that Toby is doing in #89. But, contrary to you both, I do not see this as invalidating the meta-mathematical/philosophical considerations. This is not ’confusion’ on my part, this is just my point of view: I consider the meta-mathematical argument to be a valid objection, and if there is something in the model that validates it, then it is something in the model which is awry from a philosophical point of view.
2) Morever, I consider the ’s in Matt F’s argument to be well-defined only if we have a method to obtain extensionally in an empty context (because his definition of and relies on such an extensional definition). I claim that the assertion that we always have such a method to be a form of choice, because there is no method in general to replace an intensional definition (which may have some context) by an extensional one with no context.
Note a) on 2): we have discussed at length some examples intended to illustrate why I take this viewpoint. I am content to rest on what I have already written; I think the examples hold water in illustrating my point, and my feeling is that the objections that are arising are not sufficiently new from what has been written before for me to find the energy to keep responding. After all, this is a philosophical matter; one has to ’see’ it for oneself.
Note b) on 2): Yes, we could define/evaluate and in all sorts of ways, and yes, we could consider other settings, and, yes, for natural numbers, I consider them to have intensional meaning in and of themselves, and am not against taking them as primitive. But it is an absolute fact that Matt F’s definition of and relies on a rational approximation to , and, therefore, we need to be able to obtain such an approximation to proceed, which we (meta-mathematically; of course within the model this is fine, because it is assumed as part of the formal system) cannot in general, for reasons of the intensional/extensional distinction. Again, I do not wish to write any more about this; one may object, but these objections are, in my view, highly unlikely to address my point.
Indeed, this last sentence goes for both 1) and 2) for me; they are both philosophical points which I see as evident. I thank everyone for their contributions to the discussion; if anyone has obtained anything useful from the discussion, that is great! For my part, I stick to my original point of view on the aIVT from #1 (later clarified slightly), seen from my version of constructivism; but it has been interesting to attempt to illustrate my views in the context of Matt F’s argument!
In principle I of course agree that validity in a particular formal system has no bearing on a philosophical argument unless one believes for philosophical reasons in that formal system. For this reason, I have been trying to understand your philosophical arguments on their own merits, but I have been unable to make any sense of them.
Like Mike, I want to understand your philosophical point of view, especially because I want to develop constructive mathematics that will satisfy as many philosophical outlooks as possible. However, your last comment has only confused me more, particularly note (2)(b). (I can elaborate on that if anyone is interested.)
I’m interested, Toby.
I’m only a lurker here, and certainly haven’t attempted to master all aspects of this discussion, but since it seems that the mathematics of Matt F.’s arguments conforms to a commonly accepted standard of constructive mathematics which Richard objects to in parts, I wonder what constructive mathematics looks like according to a standard Richard does find acceptable. Has it been developed anywhere? Are there others who have the same outlook as Richard?
Toby, feel free of course to elaborate.
I wonder what constructive mathematics looks like according to a standard Richard does find acceptable.
I think a good example is any kind of category theory in which one fixes a certain doctrine (category with structure, eg, a category with products), and uses only that structure to prove things. I mentioned this kind of example in #82. One can do an enormous amount of mathematics in an intensional way in something like the 2-category of categories. Here, one is using only the intensional structure of the objects of the category/2-category; what the objects look like (i.e. their extensional definition) in any particular example of such a category is irrelevant.
Are there others who have the same outlook as Richard?
I am not aware of anyone. But I do think that anyone who has thought hard about formal semantics in linguistics should have a good feeling for the difference between intensional and extensional definitions, and I think the idea that there is a method to convert from one to the other would be preposterous to any such person.
Again, consider the previous example: if someone presents me with an example of a category with products, then, without knowing anything about what the products look like explicitly/extensionally, I can prove all kinds of things about particular objects that I am interested in. Yet, since I don’t know what the products look like extensionally, I don’t have any method to convert my constructed objects to extensional ones. You might say: well, in order for the category with products to be well-defined and meaningful, we have to be able to reduce it all to set theory or whatever, so in principle we can replace the constructed objects by extensional set-theoretic ones. But this is only one point of view. Although this is possible in principle, we might regard the resulting extensional definitions to be meaningless in their complexity and lack of intuitivity. And even though it is possible in principle, we are still relying on a choice of foundations (set theory, for instance), whereas all kinds of other foundations would do equally well; so we are led to the conclusion that the meaning of what I am doing in the category with products does not come from the ability to be able to understand the structure of the category with products extensionally. From considerations such as these, I reject, on philosophical grounds, the fact that we need a method to replace an intensional definition by an extensional one; and I find mathematics developed without such a method to be more meaningful.
To go further from this point of view to the statement that there is no method to replace an intensional definition by an extensional one, we can point to the fact that there is no single of choice of foundations from which to apply a reductionist technique. One can choose one, but the intensional definition has meaning beyond it. There is no method which can tell us which foundations to choose! It is exactly that: a choice. And, from this kind of way of thinking, I regard it as a form of choice to have as a part of one’s formal system that one can replace intensional by extensional definitions: one is relying on one’s choice of foundations, not the intrinsic meaning of the intensional definition.
To elaborate on what I said in #94:
Richard, you say in note (2.b) in #92
I consider [ and ] to have intensional meaning in and of themselves
which seems to contradict your objection in #53
The point is that can only be defined for a general integer using an extensional representation of as an integer.
Your objection to Matt F.'s proof seems to rely on your claim that we need to turn an intensional description of something into an extensional one (which is not generally a valid step) in order to apply the constructions in that proof, so I've been trying to understand what you mean by that and why you believe it is so, and so you can appreciate that the apparent contradiction cited above has only confused me further.
@Richard #96:
I'm not sure what sorts of categories-with-structure you consider to be doctrines (since that term is itself vague), but how about elementary toposes? If it has no mistakes, then Matt F.'s proof can be interpreted as a statement about that doctrine; indeed, that was what Mike asked for originally (and why he was unhappy with the first answer, which cannot be so interpreted). Is it fair to say that you accept Matt F.'s proof as a proof about elementary toposes, even if you don't accept it as a proof about functions between real numbers?
which seems to contradict your objection in #53
In #53, I was referring to the formal system in which Matt F is working, i.e., what is needed for his argument to go through. Whereas 2 b) in #92 is about constructivism as I see it philosophically.
Your objection to Matt F.’s proof seems to rely on your claim that we need to turn an intensional description of something into an extensional one (which is not generally a valid step) in order to apply the constructions in that proof
Actually, my principal specific objection to Matt F’s proof is what I see as the clear (meta-mathematical/philosophical) invalidity of the trichotomy argument from a constructive point of view.
But, yes, I do also object to the definition of . One cannot have it both ways. Either one gives some extensional definition of and , and then one needs to have a method to convert any real number to an extensional one in order to proceed, which I view as clearly impossible philosophically; or one has to work intensionally, in which case one will not be able to argue as in Matt F’s proof.
Let me try one more example to emphasise the choice aspect of intensional vs extensional real numbers. Take something like for some . There are lots of different ways to define this real number. Each different notion will give us a different method to approximate it with rational numbers, i.e. arrive at an extensional definition of it. These extensional definitions are not the same, and there is no method to tell me which one to choose: it is a form of choice. The intensional meaning of is something which includes as part of it all of these different ways of defining it.
Is it fair to say that you accept Matt F.’s proof as a proof about elementary toposes,
I have already written several times that I accept Matt F’s proof within the kind of formal system that he and MIke have in mind, such as this one.
Regarding the philosophical point: this would only really shift our discussion to what is non-constructive from my point of view about elementary toposes :-). I intended my example of intensional mathematics to be purely illustrative, not to suggest that I would accept all kinds of doctrines.
Some things are evidently constructively valid in any sense. Much of diagrammatic knot theory, for instance: everything can be described in a finite way, and has clear algorithmic content. More generally, a lot of piece-wise linear topology, where one is glueing together finite collections of simplices, cubes, etc. But smooth stuff I don’t, in my own work, touch with a barge pole :-).
Either one gives some extensional definition of and , and then one needs to have a method to convert any real number to an extensional one in order to proceed, which I view as clearly impossible philosophically; or one has to work intensionally, in which case one will not be able to argue as in Matt F’s proof.
Well, I would just like to stipulate that of course one should work intensionally. But even so, I have no idea what's wrong with Matt F.'s proof.