Vanilla 1.1.9 is a product of Lussumo. More Information: Documentation, Community Support.
I would like to argue in favor of reopening this question. It has already generated quite a productive conversation, it was asked honestly, and it seems like it could be of interest to, say, beginning graduate students.
I disagree. I think that the question comes off as embarrassingly naïve. Its sheer wrongheadedness makes me question whether or not the OP has ever even read or written a mathematical proof.
Harry, you seem a little belligerent today. Remember: it's the green pills in the morning and the red ones at night.
That said, I agree with your underlying point. I don't see any evidence that the OP really understands the true purpose of mathematical proofs (to forestall the usual anonymous comments, I'm not convinced that I understand it either. But I know what it isn't when I see it. Kevin's answer comes closest, though I think that I've seen Eugenia Cheng say something similar in a more polite way.).
If someone thinks that there is a genuine question underneath, but that the OP isn't communicating it well, then either edit the question or re-ask it. However, I suspect that there isn't a genuine question. What there may be is a blog post on the nature (and nurture) of mathematical proofs and that there are many different levels of understanding a proof, and to reach a certain level you (usually) have to do some activity relating to the proof. Off the top of my head, I would class the levels something like:
It looks alright to me.
Activity: I read the statement of the theorem, and the author once bought me a drink.
The main idea of the proof is ...
Activity: I read the proof all the way through and my eyes didn't glass over at all (honestly, well, apart from the point where the author came in and offered to buy me a pint if I didn't read the next paragraph too closely).
The proof depends on ... and leads to ...
Activity: I read the proof twice!
I could write out this proof without looking at it.
Activity: Make that three times.
I could rewrite this proof.
Activity: You can't make this claim (honestly) unless you have actually done it.
This proof generalises to the case of the analytic and algebraic topology of locally Euclidean parameterization of infinitely differentiable Riemannian manifolds.
Activity: Rewrite the proof in popular song form.
It is a serious question in foundations of mathematics
Such questions exist?
But in all seriousness, I think that you're reading far too much into the question. Let me schematically split your question into two parts:
1.) Questions the OP could have asked but didn't.
2.) Reprimanding those of us who closed it, because we're not logicians.
I'm sorry, I can't say that I agree with any part of that argument. Maybe if François or Joel were to come on here and voice a similar opinion, I would take notice, but your argument doesn't make any sense to me, and I don't think you have some kind of special insight into the OP's mind or the minds of logicians in general.
Now why do you think that you know it better than the OP (even if he/she is an undergrad student) what aspects of proofs are relevant for proofs of theorems in the area of foundations?
It seems like you're asserting that proofs in some areas of math are necessarily more rigorous (in theory) than proofs in others. I don't buy it. Even though the average paper in homological algebra may not be as rigorous as the average paper in a more foundational area, that doesn't mean that homological algebraists and mathematical logicians have a necessarily different conception of what constitutes a rigorous proof when push comes to shove.
I think Mathoverflow should have a policy that questions in logic shouldn't be closed by topologists (note: I am a topologist and not a logician). This is not the first time that this comes to my mind, prompted by strangely closed questions. In practice it could be that one cannot vote to close a question whose tags have no intersection with his "interesting tags" (and also one cannot add to somebody else's question a tag that's not among his "interesting tags"). Apparently one would think twice before changing his "interesting tags" just to close somebody's question.
I think that this is a dangerous precedent to set, and I get a visceral reaction just reading it. It kind of goes against everything that mathematicians hold dear and everything that mathematics is about.
To Gerry: That'll teach me to believe google ... (for the record, I put a similar faith in random MO questions so I've just checked and you're correct, at least as far as the 1960 version is concerned)
To Sergey: I did not vote to close the question, I certainly do not judge myself knowledgeable to decide whether or not a question in proof theory or logic is of a sufficient level to be on MO or not. My remarks, facetious as they were, had very little to do with the content of the question and everything to do with the perceived level of the original questioner. In a situation such as this, I wait until the experts have commented on a question. If it seems that the question is vague, I look at the response of the original questioner to the comments. That is something that I do feel qualified to judge. As yet, there is no real response so I have no inclination to vote to re-open the question. If you (or anyone else) feels that there is a real question underneath this one, then by all means edit or re-ask it!
I think that the suggestion in your last paragraph is off-beam. Certainly, in those areas where I do not feel that I am an expert then I am much more cautious about voting to close. But I still do so, and to reopen on occasion. I do so when it is clear that, however much there may be a good question underlying the one asked, the questioner themselves does not (appear to) appreciate that fact. This seems perfectly legitimate to me. To be a good MO question requires something of the questioner, not merely the question itself.
I do not want to see the fragmentation of MO into little ghettos according to some bizarre classification such as "interesting tags" (for one, I don't use those except to make the screen a little more interesting with random colours).
@Sergey: With all due respect, I think you are reading too much into the question. I don't see the question as being about foundations at all, and the OP doesn't say anything to indicate he/she is thinking along these lines.
"Such questions exist?" - Harry, that's exactly the problem I tried to point out: you're assuming too much of a field that's not yours. Would you next suggest to save on logicians' salaries since what they're doing is not serious enough for you (assuming that you know what they're doing)?
Yes, that was a joke. I was parodying your caricature of non-logicians.
No, that's not what I asserted. You need to replace "more rigorous" by "subject to more proof-theoretic scrutiny" and then that will be right.
Could you explain what such scrutiny would entail? It sounds like word-games to me. If you're not a logician, how could you assert such a thing anyhow?
@an_mo_user: Joel's comment addresses only the existence of software that does this. It doesn't address the main focus of the question, which is philosophical rather than technical (whence came the soft-question tag.)
If the question were posed in a way that made it evident that it was a software request, I wouldn't have voted to close it.
@Sergey:
Added later: For instance, have you heard of such a thing as "Reverse Mathematics"? This is all about analyzing proofs of various theorems, mostly in foundations, and I don't think they've got to look at any results of homology algebra yet. But theirs is a very low-level analysis: they just want to see exactly which axiom-like statements were used and things like how many quantifiers and what type of quantifiers are involved. If you care if Riemann Hypothesis might be independent of ZFC, ask these people: they might be able to prove that it's not independent just because its statement is sufficiently simple.
Yeah, but the problem posed by the OP has nothing to do with this sort of thing.
Proof theory is something of a higher-level analysis, and just to start doing such analysis on some specific proof (rather than a theoretical analysis of an unspecified proof) the first thing you need is to have your proof written up in a way that the OP speaks about. (Only he doesn't want a fully-fledged computer language, which could also work.)
That sounds like the opposite of proof theory to me. Proof theory takes the syntactic data of a proof and turns it into a combinatorial problem. What you're talking about is some kind of semantic analysis.
To summarize: you won't need your homology algebra proofs expanded in the way the OP talks about any time soon just because proof theorists are not that interested (yet?) to understand homology algebra proofs. But once they do want to work on some specific proofs, they do need such expansion. Take any textbook of proof theory, and quite likely in the opening pages you'll find a discussion of the difficulty that such expansions tend to be long and barely readable in practice, and still one has to work with them - usually with aid of the computer. So what's wrong with the OP wondering just how far he can go without a computer?
It's not an interesting mathematical question. We're human beings, not computers, and we can infer meaning from context. Computers must check that every statement follows from the previous one by means of a previously specified transformation.
I might be missing something (then hopefully proof theorists would correct me) but it seems to me that your voting to close the question as "not a real question" is almost equivalent to a suggestion to stop discussing proof theory at Mathoverflow because it's "not a real theory"...
My impression is that logicians don't get all that caught up in producing fully formal computer-verifiable proofs of their results.
See above. Once again, that's the problem: something sounds to you, but then other people can't discuss their "word-games" on MathOverflow. Are you aware that a chasing in a diagram of acyclic fibrations and cofibrations would be a very good example of what should sound like a word-game to most non-mathematicians?
Again, you misunderstood. I was saying that you were playing word games by trying to make a distinction between "logical rigour" and "proof-theoretic scrutiny", which I don't think means anything. If a proof is rigorous, it should survive any scrutiny, proof-theoretic or not.
Since there were already three votes to reopen, I used my moderator powers to supply the remaining two votes. In view of this discussion, I feel that I need to justify my decision.
It seems to me that most of the controversy is based on subjective readings of the question. Even I was guilty of that when I first read the question. However, after careful scrutiny, I came to the realization that this is actually a good question. Indeed, the question asks whether there is a bridge between standard mathematical proofs and formal proofs as defined in logic. The answer to that question is a non-obvious 'yes'.
1 to 20 of 20