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.
I’d think that whatever Richard’s philosophy of constructivism is, ultimately it should have a clear formal meaning in terms of what is or isn’t a valid proof according to that philosophy, i.e., should have clearly specified rules of deduction etc. I’m curious: is this something you’ve worked out, Richard?
Since the discussion has run for 100 comments with seemingly no resolution in sight, I’d think it’s gotten to the point where the formal procedures had better be spelled out in order to make any progress (although I repeat that I’m not following all of this discussion in detail).
Urs: yes, thanks. I agree with you. The second paragraph of #101 is addressed to Richard. Is there a way to formalize exactly what he is objecting to in Matt F.’s proof (seeing that Toby is still mystified by what the objection is). Because it seems that Richard agrees (in #99) that the proof is formally correct according to a commonly accepted standard; my question to him is: have you tried to formalize your philosophical position?
In fact, let me try re-asking my question in a more stark and explicit form. (Edited, and edited again to be more 2nd person)
If I understand correctly, Matt F.’s proof has been accepted (by e.g. Mike) as a theorem which is valid when interpreted in a general topos. The proof given was cast in the language of ordinary set theory, but for about 40 years or so, category theorists have known formal procedures for checking validity of such statements in a general topos (Kripke-Joyal semantics). This seems to be a generally accepted state of affairs.
So, Richard: as for why you don’t accept the proof, I’m not quite getting it, but I consider two possibilities. (1) The proof given by Matt F., which was presented informally as most proofs are, has, when more fully formalized and explicated via Kripke-Joyal semantics, some subtle flaw in it. (2) There is no such flaw, but there is something wrong, or somehow ambiguous, about Kripke-Joyal semantics itself.
I’m guessing it’s (2), and if so I’m asking whether you could pin down in more formal (less philosophical) language what the problem is and what a proposed replacement might be.
But please correct me if I’m misreading the state of affairs.
Todd, it sounds to me as though Richard just doesn’t consider elementary toposes to be “constructive” enough for his taste. (Though like everyone else, I am mystified about why not.)
is this something you’ve worked out, Richard?
No :-). As I have already written, I did not set out in this discussion to write a treatise on my philosophical views, and indeed that they were brought up at all was an accident, due to my reading too much into what Mike called ’plain constructivism’ (i.e. I interpreted it philosophically, whereas Mike had in mind a specific formal system), and my consequently thinking a little about the statement from constructivism as I see it.
I could no doubt put down a more treatise-like exposition of my philosophical views, but I have no plans to currently try to do so. I do, however, try to follow my philosophical views in my own work. There is not much of this publically available, though :-).
ultimately it should have a clear formal meaning in terms of what is or isn’t a valid proof according to that philosophy
Not necessarily. We have become very used to formalism, but it is not the only way to do mathematics. In particular, the formalism is always secondary to the mathematics. There can be a philosophy about what a valid proof is, without that being fully captured by any particular formal system.
with seemingly no resolution in sight
I am not looking for any resolution, or trying to convince anybody; and, as I have already written several times, I am entirely content to bow out of the discussion. But if people show an interest in my views, then I am trying to reply. I have formed my views over a long period of time, and am quite secure in them :-).
Mike had explained the formalization issue in #23, had given the formalization of the stronger statement in the second paragraph of #27 and had explained in #31 that the stronger statement is false.
I believe that we have discussed this already. I am making a philosophical objection to a formal system: this cannot be rebutted by interpreting the objection in the formal system!
Todd, it sounds to me as though Richard just doesn’t consider elementary toposes to be “constructive” enough for his taste.
Yes.
I am mystified about why not.
Well. there are plenty of reasons that a perfectly orthodox constructivist might reject the notion. Just think of predicativity, for instance. But I’d rather not go down this road, because I think that my philosophical objections are more fundamental, and trying to pin down some notion of topos in which to express them is not going to lead us to much enlightenment, I feel.
as for why you don’t accept the proof,
I know that you have not been following closely the discussion, Todd, but still, I think that I have stated rather clearly what my issues with it are. Both are on the philosophical/meta-mathematical level rather than an issue with the logic of the proof as expressed in, say, an elementary topos.
If you would like a specific point to discuss, Todd, I would still come back to my meta-mathematical opposition to the trichotomy step in Matt F’s argument. The logic of this is as follows: we are in the middle of an induction, and in order to proceed, one of three things must be able to be demonstrated. Two of these things may not be possible to demonstrate. In this case, either the third must be able to be demonstrated, or we cannot proceed.
People keep kind of dodging this argument by giving me some argument in a model, but such arguments in a model are irrelevant, because if the model justifies an invalid argument, then it is the model that is at fault. Thus, as a somewhat neutral observer, Todd, I would respectfully like to ask for your opinion on the meta-argument of the previous paragraph, ignoring everything except the argument itself. Do you agree that it is valid?
Mike had explained the formalization issue in #23, had given the formalization of the stronger statement in the second paragraph of #27 and had explained in #31 that the stronger statement is false.
I am making a philosophical objection to a formal system: this cannot be rebutted by interpreting the objection in the formal system!
Formalization just means achieving clarity and precision. Mike’s simple observation about propositional truncation accurately formalizes the statement that you have been expressing, once more at the end of #106.
If we all agree that the meta-mathematical argument is valid, and that therefore Matt F’s argument is invalid from a meta-mathematical point of view, then we are in much more agreement than I thought. I don’t think that this is the state of affairs, however.
Just to clear up something simple before responding more directly to Richard: by ’formalization’ I mean something more in spirit with what Urs said in #107. We convince each other in mathematics by giving proofs (with agreed-upon rules for what constitutes a valid proof). Usually conflicts in mathematics are resolved very quickly that way (a signal virtue of mathematics in my opinion), and for that reason I wanted to see if we could move to a mathematicization of whatever philosophical point was in contention. So here, you could substitute ’mathematicization’ for ’formalization’.
So, for example, if Richard were to agree that it is overwhelmingly likely that Matt F.’s proof could be converted to a fully formal proof which is valid for a general topos according to the standard Kripke-Joyal semantics of statements written in higher-order intuitionistic logic, then I would feel much relieved. I think what this is asking is unambiguous enough that the whole kit-and-caboodle could be subjected to verification in a proof assistant, and then we should all agree on at least that. And I expect that you (Richard) would agree with the first sentence of this paragraph. If not, then I think we could quickly isolate what is the mathematical difficulty, and conflict resolution would probably be just around the corner.
More later.
From #106:
Well. there are plenty of reasons that a perfectly orthodox constructivist might reject the notion. Just think of predicativity, for instance. But I’d rather not go down this road, because I think that my philosophical objections are more fundamental, and trying to pin down some notion of topos in which to express them is not going to lead us to much enlightenment, I feel.
First of all, let me say thanks, Richard, for your overall patience in this discussion. I realize that you feel you have been repeating yourself many times, but I guess patient repetition may be necessary sometimes.
Predicativity is the only reason I can think of where a ’constructivist’ might take issue with the notion of topos. (In fact, I think of predicativity per se as going off in a different direction from core constructivist concerns; for example I think one could be a predicativist who accepts classical logic, etc. – but maybe the term ’constructivism’ is sufficiently vague and labile that it’s better not to argue over its meaning.)
Unfortunately, I still am not grasping other philosophical objections.
But actually, I’d think it could be a useful exercise or program to mathematicize any philosophical objections, and that it could lead to clarity and enlightenment. For example, there are notions of predicative topos, with some nice mathematical literature behind it, and for me such precise notions are very helpful indeed.
Now I’m not asking that you give a similar full-blown mathematical explication of your philosophical position here and now in this discussion thread. Such projects do take time after all. But I would like to encourage you to consider doing that at some point: if you feel your philosophical objections are fundamental, then they deserve to be mathematicized! It’s a way of taking one’s ideas very seriously.
If we all agree that the meta-mathematical argument is valid
The argument seems pretty mathematical to me (easily formalized), as Mike pointed out in #23 and #27. Under discussion is a constructive proof of a propositional truncation of a dependent sum, and your objection is that one should instead consider the stronger demand of constructing a term of the un-truncated dependent sum. One may indeed consider this, and the result is a statement that is precise enough that it may be subjected to mathematical argument: The stronger statement turns out to be wrong, as Mike explained in #31.
I know that you have not been following closely the discussion, Todd, but still, I think that I have stated rather clearly what my issues with it are. Both are on the philosophical/meta-mathematical level rather than an issue with the logic of the proof as expressed in, say, an elementary topos.
If you would like a specific point to discuss, Todd, I would still come back to my meta-mathematical opposition to the trichotomy step in Matt F’s argument. The logic of this is as follows: we are in the middle of an induction, and in order to proceed, one of three things must be able to be demonstrated. Two of these things may not be possible to demonstrate. In this case, either the third must be able to be demonstrated, or we cannot proceed.
People keep kind of dodging this argument by giving me some argument in a model, but such arguments in a model are irrelevant, because if the model justifies an invalid argument, then it is the model that is at fault. Thus, as a somewhat neutral observer, Todd, I would respectfully like to ask for your opinion on the meta-argument of the previous paragraph, ignoring everything except the argument itself. Do you agree that it is valid?
I’d like to flesh out a response, but I’ll need to feel my way into this, and ask you (Richard, again) some questions.
To me one of the most helpful comments in this thread was Toby’s #89, which actually put down a mathematical proof and was very specific. It was a dichotomy, not a trichotomy statement, but I feel that’s probably sufficient for the issue at hand:
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 .
This is one of those times in the discussion where I breathed a sigh of relief, where I felt “now we’re getting down to brass tacks!” It’s not a difficult proof or anything, but by being explicit, it should give you a firmly fixed target to aim your objections at.
Could I ask you (and begging your indulgence if this is repeating yourself) to pinpoint the exact spot in Toby’s argument where you shake your head, and why? (I did see that you mentioned Toby’s #89 later, but only indirectly AFAICT).
I can tell you what all this reminds me of: the distinction in topos theory between having an inhabited object and an object with a global section . I think we all know the canonical examples where the distinction is made explicit. For me, it’s “every complex number of norm 1 has a square root”, reinterpreted in the topos of sheaves over where the double cover is inhabited (the image is the full subobject ) but there is no term . The gut feeling I have through the discussion is that you want “ is true” to mean we can actually exhibit a witness term/section , which obviously isn’t the case in this example. Rather, in standard topos theory, witnessing truth is local: there are local sections when we pull back to small neighborhoods , and these small neighborhoods cover, and that’s the criterion in Kripke-Joyal semantics.
Similarly, when Toby gives his proof, I have in my mind’s eye a covering of by the subobjects and , and is all of , i.e., the map induced by the subobject inclusions is a surjection even without a section . Where Toby says “with enough work”, I take that to mean enough information (about a given real ) to give a small enough neighborhood containing for which we can write down a local section.
Now I think all of us know all this (really I’m just giving extra verbiage to support points already made by Mike and Urs), but I suspect it’s at the heart of the discussion. (Let me admit to being confused by some discussions of intuitionism I see which seem to ignore the distinction I’m trying to highlight, and say that existence baldly means producing a [global] witnessing term; it seems to me the issue is more subtle.)
Please (and this is to everyone) enlighten me if you think I’m confused.
I can tell you what all this reminds me of: the distinction in topos theory between having an inhabited object and an object with a global section .
Todd, this is exactly the difference between constructing a term of the propositional truncation of versus a term of , which Mike mentions in #23 and #27 as being the difference between the statement proven by Matt F. and the stronger statement that Richard says he should have proven.
Urs, yes, thanks for corroborating. (I was alluding to Mike’s comments and also yours in my penultimate paragraph.)
Richard, no one is “dodging” your argument. We have replied to it many times; you are the one who is ignoring the replies.
With regard to the distinction between being inhabited and admitting a global section , I should recall that there is the notion of local topos where the distinction vanishes. I suppose that a traditional (but non-predicative) categorical constructivist would regard any category worthy of the name as a local topos. But this doesn’t affect the substance of my earlier comments.
Mike: Toby and yourself have said something about the argument many times, but not as far as I can see actually replied to it as a pure logical argument; always the model is brought in, which has nothing to do with what is a pure piece of logic.
As far as I can tell, the last word on the subject was #90. Again, I don’t feel that this replies to the pure logical argument itself, it tries to circumvent it. Just take to be constant, either at , where is the first Mersenne prime between and , if there is such a prime, or at if not. Since we can algorithmically check (in principle) this, is constructively well-defined. Take to be . Now, we have no way of knowing at the present time whether or or . You seem to be claiming that Matt F’s proof magically produces a proof of one of these? (Of course, this does not satisfy the hypotheses of the aIVT, but the trichotomy step is something that is claimed to hold completely generally). Whereas as I am saying: no, what happens is that we cannot necessarily proceed to the next step in the induction; we get stuck, and cannot complete the proof.
#90 makes no reference to any model.
90 makes no reference to any model.
You wrote in #90:
my 84 and Toby’s 89 explain how.
These are arguments in the model. In other words, what was given in #90 was first a reference to some arguments in a model as justification for the trichotomy. Then came the following, which is a meta-mathematical argument in support of these arguments in the model.
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.
I am arguing that this is circumnavigation, and does not address my point. If we do not have a proof of any of three things, then if you wish to proceed in the proof, you have to magically produce a proof of one of them, or else you cannot proceed; and my objection is to this. Instead of responding to this actual objection, you circumnavigated around a detail of my phrasing: when saying that if we cannot prove two things, then we must have a proof of the third, I of course had in mind that the two things we cannot prove are such that it would be preposterous for something as trivial as the trichotomy argument to give a proof of one of them.
As for the final paragraph of #90, it should be clear that I am not assuming that it is impossible to give a proof of the two things, only that we do not know how to do so, and hence, if we do not know how to give a proof of the third either, then we are stuck.
There is a sort of objection that I would understand to using (approximate) trichotomy in an inductive proof. This is what Mike analysed in #23. Philosophically, I agree with Mike that this sort of thing is OK, since we are merely proving a proposition about already constructed things, rather than constructing a new thing by recursion (which would only be valid if we accepted Dependent Choice). Yet, if someone feels differently about that, then I could understand their position. In Richard's case, I almost want to say that I do understand.
But when Richard tries to clarify, I don't understand. Take #117, for instance. This involves a construction of a number that nobody here is physically capable of computing, which an ultrafinitist would not accept. Now, Richard is no ultrafinitist; he writes
Since we can algorithmically check (in principle) this, is constructively well-defined.
Fine. But then Richard goes on to write
we cannot necessarily proceed to the next step in the induction; we get stuck, and cannot complete the proof.
This sort of thing is why I thought for a moment a while back that Richard was ultrafinitist. Since you're not, why not instead say
we can (in principle) proceed to the next step in the induction; we can complete the proof.
If it is acceptable to use the result of an in-principle computation to define , why is it not acceptable to use the result of an in-principle computation to proceed with the induction?
In terms of my brass-tacks computation in #89 (conveniently quoted in #112), the objection that I understand says that is not determined uniquely by and , so it is not valid to pick such a in the course of an inductive argument in which different values of appear at different stages of the argument (or at any rate that doing so amounts to using Countable Choice). (There is no problem with or , since these can be chosen once and for all before the induction begins.)
But this is not the issue with Richard's example from #117, in which is already rational. (Note that the in this post and in #89/#112 is the in #117.) We don't know which rational number is, but whatever it is, we just use that for . (Note that the in this post and in #89/#112 is not the in #117.) So continuing on with my argument in #89/#112, I presume that Richard objects to saying
Since and are rational, either or .
Specifically (assuming that I didn't mess up), if there is a Mersenne prime between and , or if there is no Mersenne prime between and , then the second of these holds; otherwise, the first of these holds. I don't know which of these is the case, but since we're not being ultrafinitist, why can't I just say that we can (in principle) algorithmically check which it is?
Once we get past that, then in the first case we have (or in the language of #117), while in the second case we have (or in the language of #117), so there shouldn't be any further problems.
#84 and #89 are not “arguments in the model” either. I don’t know what “model” you are talking about.
The second paragraph of #90 works just as well for ignorance as for impossibility. And I don’t know quite what “preposterous” means (and phrases like “of course” and “it should be clear” are not helpful when you are trying to explain your position to someone who is trying their best to understand but to whom it is evidently not clear), but the same argument should apply no matter how you conclude that we don’t have proofs of the first two.
If it is acceptable to use the result of an in-principle computation to define , why is it not acceptable to use the result of an in-principle computation to proceed with the induction?
why can’t I just say that we can (in principle) algorithmically check which it is?
My view is as follows. It would be OK in some cases to proceed on an in-principle basis (this is an instance of what I mean by working intensionally). But it is not OK here, because here you are relying on being able to compute in order to carry out your argument. Whereas the definition of is not relying on anything, it just that: a definition. We could prove things about without relying on computing it, and that would be OK too. But that is not what you are doing in your argument. This is exactly why I keep emphasising the reliance in Matt F’s argument on extensionality. Again, if you take as an axiom that every intensional number can be converted to an extensional one, then there is no problem; but this is exactly what I am objecting to.
I don’t know what “model” you are talking about.
A model of constructive mathematics as you perceive it, eg, an elementary topos. ’Formal system for orthodox constructive mathematics’, if you prefer.
The second paragraph of #90 works just as well for ignorance as for impossibility.
I do not agree. Impossibility of two of the possibilities would imply that the third possibility must be provable if we are to proceed. Not being able to prove two of the possibilities (and the third as well, of course), allows for the possibility of getting stuck in the induction without implying anything about the third possibility. And we certainly we do not need an empty context to be able to get stuck in this way.
It is not possible to get stuck in the induction because we can prove that one of the three possibilities must obtain. You have not refuted the proofs of #84 and #89. Those arguments could of course be formalized in a formal system for mathematics, but on their own they are just mathematics, so if you disagree with them it is incumbent on you to say what exactly you object to about them, not dodge the issue by claiming that they are formalized in a system you disagree with.
I have attempted to do so perhaps twenty times now :-). In #89, the following occurs.
Now approximate and with rational numbers to within .
This relies on an extensional definition of , i.e. (in this context) an which has been computed. So the argument is stuck on/blocked by the computation of , which we do not know how to carry out. The issue is not specific to computation, it is more generally the problem of replacing an intensionally defined entity with an extensional one.
The definition of is not blocked by computation; indeed, computation has nothing whatever to do with it. And similarly, there are things we can prove about without computing it. But one cannot carry out the proof of #89 without computing it.
To repeat an idea I have also mentioned on several occasions (but perhaps it will be better understood now), my view is that #89 is a proof that is carried out in the context of being able to compute ; and this is not something that is always possible, so it is not a proof per se.
To emphasise once more, the point is that there is no method to tell us how to compute something. The example with Mersenne primes illustrates this quite nicely. These primes are not being found by brute force, using the definition of a prime, which is the only immediate notion of computation we can extract from the intensional definition. Rather, use will be made of the theory of Mersenne primes, no doubt with some algorithmic tricks from computer science thrown in as well (concurrency, not least).
So we are brought back to my main philosophical point: there is no method to replace an intensional definition by an extensional one.
Well, I suppose we are not going to get past this impasse, but I have to ask this: do you regard
as a valid (intensional) definition? I had been assuming that you were like other people who call themselves “constructivist” in rejecting this definition, but if you are willing to allow intensional definitions for which there is no method to replace them by an extensional one, then perhaps you are actually okay with this definition? If not, what do you object to about it?
do you regard…as a valid (intensional) definition
No. There is no method to decide whether the Riemann hypothesis is true or false. (Whereas there is a perfectly good method to construct the in my example of a few comments ago).
Okay, I give up. You do require a definition to be given by a method, but then you don’t allow anyone to make use of that method; so I think your philosophy is inconsistent.
Not at all. I require both definitions and proofs to be given by methods. If a proof relies on the method associated to a definition to be carried out (completely) without there being a method to carry it out, then we do not have a proof. The point is that a definition derives its meaning from the method itself which defines it, not from carrying it out. This is the very nature of the extensional vs intensional distinction.