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.
Just some idle thoughts:
To quote from David C’s previous blog, an entry about a Wittgenstein conference:
What then of universal arithmetic statements? Well, their meaning is constitued by their proof, typically a proof by mathematical induction.
…
But this idea of a statement taking its meaning from its proof meets with problems. It suggests that a proposition has no meaning before it has been proved, and that we can’t say we have two different proofs of the same proposition.
Clearly one can get carried away and attribute to W. ahistorical ideas, but here I go anyway.
Compare the above idea, that the meaning of a proposition is carried by its proof, with that of homotopical type theory, that a proposition consists of its proofs. If a proposition is not inhabited, then it is not provable. In the world of HoTT, one sees a proposition as a type, and the fact it has different proofs really tells us something about the ’space’ (=’homotopy type’) that that proposition ’is’. When assuming, or imposing, proof irrelevance in one’s type theory, then we really only care about the binary situation exists/doesn’t exist a proof. But in practice, mathematics is not like this (cf Atiyah-Singer index theorem, 4-colour theorem etc). Rarely do people find a proof and then move on to the next proposition, using only the truth value they just discovered; they want to explore the ’space’ that is that proposition/type.
But the proposition, as an object, exists, prior to our answering the question of whether it is inhabited by any proofs.
I think that we’re conflating proofs that have been found with proofs that in principle exist.
Hmm, ok. Poor analogy then. :)
This theme has cropped up before, and when I have some time I’ll try to track down previous discussion. One point of view took the question of when we say two proofs are essentially the same to be very interesting, yet doubted a proof theoretic syntactic approach would shed much light. I certainly find it intriguing that one may clearly judge a new proof to be, say, a minor variant of an existing one or a radically new one, yet there seem to be no tools to formalise to this.
Just looked and see Gowers discusses this. My sympathies lie with the fourth approach Tao mentions in his first comment - the conceptual.
I do not find his comment sensible. Namely the entry is about the similarities between the proofs and Tao refers (when talking on conceptual) to the heuristics and sketching in proving as the bone of that. But these are two different things. Namely the sketch of the proof is a basis of search for the researcher but the finished proof often has the hardest twist in new details, not in general outline. There are some typical problems for which a general approach is known but nobody can do it. For example, when approaching motives one wanted to do decades ago by mimicking singular homology, but this gives nothing sensible in algebraic setup, it seemed so other approaches went on. Until Voevodsky came with Nisnevich sheaves with transfers and succeeded to get the derived category of motives just by outline analogous to the singular homology (look at the introduction to his 1994 article). So there is an analogy here, but the difficult part is really in understanding and getting things like Mayer-Vietoris gluing in Nisnevich topology, the usage of transfer (sheaves with transfer) and so on, what is really the meat of the proof. I do not want to call proofs similar if they have naive sketch the same but if the essential hard facts internally used are parallel. Furthemore word conceptual would to me mean the character of the objects involved, like the feeling one has about smooth functions vs. other function, about henselianess of ground ring when it is involved, the homotopical character of some construction (derived vs. 1-categorical limits for example) and so on. Those conceptual feelings of characters involved are on the other hand not LOGICAL steps as the outline of the proof is. So Tao puts at least three substantially different things under the same name of conceptual similarity of proofs including mixing heuristics/approach to find the proof with the meat/essence of the actual found proof.
I should also say that the wholel discussion at that blog there is not in my taste. Namely one thing is how to defined things with some absolute meaning and another is to say what is the essentially new with some proof at some stage of general knowledge of standard proof techniques in that area in community. For a mathematician real importance is the latter, not the first. This discussion there does not even make a clear distinction when one is trying to do the first and when the second (for the first one can either go with some metrics, what is not very fundamental or with dependence, but then it is in standard logics sense, not interesting for the kind of questions in focus). I would prefer if the discussion really went about the creative part of the proof, about what is new to the understanding, what brings systematic techniques and what is just an accidental trick, and what was known in other form and now takes a new form or gets crystalized to further clarity. Such things are questions which are I think more important, while they are not mathematical but truly about comparative heuristics.
1 to 6 of 6