When is a proof rigurous 'enough' ?

[Damidami]

Do you think that a proof of a theorem can always be made more rigurous? Or there is a limit on how rigurous a proof can be?
I mean, what is today considered a rigurous proof of an established theorem, may not be a rigurous proof of tomorrow with more advanced techniques?

Or do you (anyone who reads this) think that a proof can be so rigurous that it can not be enhanced in any way?
What about alternative proofs? Do you think it is useless to find other proof of an established theorem? Do you think one proof will always be the better/more rigurous? Or that two proofs of a given theorem can have relative advantages in some sense over the other? (rigurous vs simple, etc)

What would be the point of finding a proof of an already established theorem? Can it be better in some way? In which sense? (elemental, simple, rigurous, short, elegant?) (It may be a matter of taste if a proof is more elegant than another, isn't it?)

One think that surprised me was to read that Gauss gave 6 different proofs of the fundamental theorem of algebra. Wasn't one good enough?

Thanks.

 

[Noxide]

A proof is considered to be rigorous if the validity of each step in the proof and the connection between each step is explicitly made clear such that the results follow with certainty

 

[Damidami]

A proof is considered to be rigorous if the validity of each step in the proof and the connection between each step is explicitly made clear such that the results follow with certainty

Thank you for your reply.
Then what is the point of finding 6 different proofs?

 

[Noxide]

What's the point in asking that question?

My question and yours share the same answer.

 

[Damidami]

What's the point in asking that question?

My question and yours share the same answer.

You mean it's completely useless to find alternative proofs?
My point in asking that question is I want to know what people consider a proof really is.
Maybe the point of finding 6 different proofs is because one may not be completely rigurous, or be too obscure.
And of course what makes the 6 proofs different? When two proofs of the same theorem are considered really different proofs? Changing a single word makes it another proof? (of course not) But I think there is a gray zone between rigurous and non-rigurous proofs.

I read some "theorems" that were proved in the past were later found to be wrong (finding counterexamples)
Maybe what we now consider a theorem is flawed too.
But people seem to think of proofs as white/black, either its correct or it isn't, while there is a (small) posibility that everyone is wrong.

Of course, no one cares, I was just curious.

 

[JSuarez]

I mean, what is today considered a rigurous proof of an established theorem, may not be a rigurous proof of tomorrow with more advanced techniques?

It happened several times; for example, when Hilbert and Poincaré started developing topology, their proofs were not rigorous by todays standards and were remade; the same happened in other fields of Mathematics, like Complex Analysis (with Riemann's works) and Algebraic Geometry. This seems more likely to happen with incipient fields, where the ideas are new and the correct way to handle them is poorly understood.

Or do you (anyone who reads this) think that a proof can be so rigurous that it can not be enhanced in any way?

There are theorems (in Number Theory, for example) whose proofs didn't change in thousands of years; still, it's possible that logical steps that today are considered elementary will be, in the future analysed further.

What about alternative proofs?

Alternative proofs can be very important in several respects: constructive vs. nonconstructive; one proof could contain ideas that may be applied to other problems; they may point to connections to other areas or a deeper understanding of the original theorem, etc.

One thing that surprised me was to read that Gauss gave 6 different proofs of the fundamental theorem of algebra.

This is not so uncommon (well, from a single author, it is). In this particular case, the problem was that nobody was able to come up with a purely algebraic proof.

 

[yossell]

Do you think that a proof of a theorem can always be made more rigurous? Or there is a limit on how rigurous a proof can be?

If a proof is a matter of logically deducing formula from axioms, then, with modern logic, I think proofs are as rigorous as can be, and that there's probably not much to talk of degrees of rigour.

However, different proofs might be interesting because they use different or fewer axioms, or fewer axioms, and we might not be equally convinced of all our axioms. For instance, we might have some doubts about the axiom of choice (people once did), and so some might prefer a proof that didn't use this axiom. Alternatively, we might be able to considerably shorten a proof by appealing to the axiom of choice - and since there's always the chance that we've made a mistake, we might find shorter proofs more convincing.

Finally, different proofs can just sometimes be interesting and informative, introducing a technique that enhances our understanding.

 

[ZQrn]

'Rigorous' is as meaningless as 'elegant' formally speaking, it doesn't exist, and the majority of mathematicians have never seen a truly 'correct' proof in their lives from start to finish. This is because they are ridiculously long.

What does exist is a formal proof and when you see things like 'formal definition of the limit' passing by or 'formal' in really just about any field except real unadulterated proof theory, it's pretty much abuse of the term. Formal as the name suggests deals with form, it does not deal with 'meaning'. The nihilists won that debate aeons ago, meaning simply does not exist technically speaking, or even more technical, there has never been any proof that it does, nor has the concept be defined.

Most mathematics is in the end what's called 'naïve', contrasting 'axiomatic', many things that are passed as axiomatic are in reality also naïve, what true axiomatic maths is is stating explicitly every rule you may use, you can simply not use a thing that's not stated you can use, down to the most literal sense of the idea. Things like $\{\neg \neg P\} \vdash P$ or even the mother of all $\{P \rightarrow Q,P\} \vdash Q$, the modus ponens are axioms, not absolute facts. The latter is particularity handy, it says that if we have as theorems a logical formula P, and a logical formula P->Q, then we may write down the logical formula Q as a theorem. Or more intuitively said 'If P is true, and P implies Q, then Q is true.'

What symbols like '->' or '¬' would 'mean' are outside of the scope of the debate of proof theory, proof theory defines how we may re-arrange them, nothing more.

This indeed does present us with an 'atomic' step that cannot be simplified any more and defeats the nihilists who will always say from every step 'Well, how do you know that ...', well, you don't!, and you don't need to. All formal proves are are manipulations of characters in strings, proof theory does not define what these characters would mean, all it defines is how, in the context of proof theory, we may re-arrange them. A proof is formal if in every step one of those legal rules, our axioms has been used. And this will mean that extremely elementary things will take up pages and pages of rules to derive the formula you want.

It is also formal because a machine can trace the proof and easily verify that each step was legal. Outside of proof theory 'formal' and 'rigorous' are essentially meaningless terms that carry no harder meaning than 'elegant'. They're buzzwords and all they mean is 'your argument was compelling enough to convince me that it's certainly true'.

 

[Hurkyl]

Nihilists? I didn't realize they had any contribution to mathematics.

Oh, I get it. It's that you don't like syntax, so you're trying to come up with some ridiculous, exaggerated label to try and poison the idea to others.

I have yet to understand the mindset that leads people to be so vehemently opposed to separating the notions of syntax and semantics.

 

[ZQrn]

Nihilists? I didn't realize they had any contribution to mathematics.

Without them formalism wouldn't have started really. Nihilists defeated 'meaning' long ago, 'form' they've yet to defeat.

Oh, I get it. It's that you don't like syntax, so you're trying to come up with some ridiculous, exaggerated label to try and poison the idea to others.

I've no idea what to make of this, care to elaborate term 'syntax' here?

I have yet to understand the mindset that leads people to be so vehemently opposed to separating the notions of syntax and semantics.

Now I don't get you at all anymore.

I was quite explicit in there being three different levels:

A: syntax, which strings of symbols are legal and which are not, probably generated by some, most often context free, grammar.
B: semantics, the rules by which new legal formulae may be derived from old by manipulating those symbols
C: meaning of the symbols, not a formal category and this is where the nihilists win, you simply have a string of symbols that you can move around but you cannot show they have any 'meaning'.

I mean, I can have the same syntax as FOL, as in, generated by the same formal grammar but give it a completely different semantics yes? I don't see where you're getting at.

I'm just pointing out that 'rigorous' is a vague word and not a formal concept. What makes a proof 'formal' is quite clear and what makes an 'atomic step' too, but very few mathematicians have ever read a completely formal proof from start to finish, but a computer can quite easily verify these. It's called compiling an OCaml program.

 

[JSuarez]

Nihilists defeated 'meaning' long ago, 'form' they've yet to defeat.

This is already too remote from the OP's question, and I suppose that there is no use in pointing out that Formalism, at least in its original form, is dead as a doorknob. Besides, I think that someone should warn the "Nihilists" that a lot of people continue to pursue the study of formal semantics, so "meaning" is still very alive.

I'm just pointing out that 'rigorous' is a vague word and not a formal concept.

Formal, no, but still analysable see, for example:

http://www.andrew.cmu.edu/user/avigad/Papers/understanding2.pdf"

 

[ZQrn]

This is already too remote from the OP's question, and I suppose that there is no use in pointing out that Formalism, at least in its original form, is dead as a doorknob. Besides, I think that someone should warn the "Nihilists" that a lot of people continue to pursue the study of formal semantics, so "meaning" is still very alive.

Formal semantics has nothing to do with 'meaning'. A formal language simply has two formal properties, its formal grammar. The subset of the permutation of the alphabet which is a legal sequence of symbols. And its formal semantics, which says how those symbols may be re-arranged to form new formulae.

Neither of which has anything to do with what those formulae may 'mean'. The formal semantics of the symbol $\rightarrow$ is simply governed by the fact that for any two formulae F,G, if we have $F$ as a formula (theorem) and $F \rightarrow G$, then we may write $G$ as a theorem. That's all, what $\rightarrow$ then would 'mean' is beyond the scope of formal denotation and we are not concerned with that or with what 'meaning' would even be or if such a concept can exist.

Formal, no, but still analysable see, for example:

http://www.andrew.cmu.edu/user/avigad/Papers/understanding2.pdf"

Sure, but then you can't argue that a proof is 'rigorous' or 'not rigorous', it is as vague as saying a painting is 'beautiful', sure, a lot of people will find the same painting beautiful. But if some one comes and says 'it's ugly', the only thing you can say is 'You're wrong, because I'm right!'

The only thing you can do when you say 'this isn't rigorous' is saying 'you 're wrong to find it rigorous, because I'm right when I don't find it rigorous', it's just your word against that of the other. Debating what is rigorous and what is not is therefore little more than an aesthetic effort.

However, if a proof is formal or not can be objectively justified.

 

[Hurkyl]

...

The formal semantics of the symbol $\rightarrow$ is simply governed by the fact that for any two formulae F,G, if we have $F$ as a formula (theorem) and $F \rightarrow G$, then we may write $G$ as a theorem.

...

You have confused semantics with syntax.

 

[JSuarez]

And its formal semantics, which says how those symbols may be re-arranged to form new formulae.

I'll side with Hurkyl here: you confuse inference rules with syntax. This is clear in your comments regarding modus ponens: they only for the material implication; if you try the same thing with, for example, modal logic or other types of conditional expressions, it fails.

Formal semantics has nothing to do with 'meaning'.

What?!

Debating what is rigorous and what is not is therefore little more than an aesthetic effort.

Ah, another death by Wittgenstein. Anyway, this is a useless polemic, to which I won't respond further...

 

[ZQrn]

You have confused semantics with syntax.

And is your perspective on 'syntax' in any way different from 'formal grammar'.

As far as I know, a formal syntax / syntax with respect to an alphabet A is nothing more than a set or rules which partition A* into elements which are considered grammatically legal, and those which are considered grammatically illegal.

A formal semantics is a completely different thing and depends on the context but in proof theory comes down basically to ones rules of inference.

What?!

Oh well, if I can't convince you, maybe wiki can:

According to formalism, the truths expressed in logic and mathematics are not about numbers, sets, or triangles or any other contensive subject matter — in fact, they aren't "about" anything at all. They are syntactic forms whose shapes and locations have no meaning unless they are given an interpretation (or semantics).

It's really the essence of formalism that the strings you manipulate in principle have no meaning, it's symbols you re-arrange, nothing more.

 

[yossell]

Ah, another death by Wittgenstein.

?

 

[Hurkyl]

And is your perspective on 'syntax' in any way different from 'formal grammar'.

Syntax deals with defining and manipulating languages; thus it includes proof theory.

Roughly speaking, anything that treats strings of symbols on their own merit rather than as stand-ins for some other notion falls into syntax.

rules of inference.

All issues of trying to precisely define mathematical fields aside, rules of inference are grammar, usually explicitly so.

Oh well, if I can't convince you, maybe wiki can:

Semantics is quite literally the study of meaning. At this time, Wikipedia has it right, so go look since you seem to take it as an authority.

Formal semantics is merely semantics as applied to formal languages and what-not. A typical mathematical application is model theory -- how to interpret strings of symbols as referring to mathematical objects or assertions about them.

It's really the essence of formalism that the strings you manipulate in principle have no meaning, it's symbols you re-arrange, nothing more.

Only a very extreme sort of formalism.

Formalism in general does not require a dogmatic assertion that one may not assign meaning to strings of symbols -- it only requires that you play the symbol pushing game as a symbol pushing game; no "cheating" by asserting some statement must be true by a non-symbol pushing argument. Either prove it by pushing symbols, or admit that you are simply adding it in as another hypothesis.

 

[ZQrn]

Syntax deals with defining and manipulating languages; thus it includes proof theory.

Roughly speaking, anything that treats strings of symbols on their own merit rather than as stand-ins for some other notion falls into syntax.

Well, then your definition of 'syntax' is what I call 'formal grammar' and 'formal semantics'.

http://en.wikipedia.org/wiki/Formal_syntax

Wikipedia, (which I do consider an excellent mechanism for catching the mainstream definition of terms) uses neither of our versions it seems, it uses 'formal syntax' for what I call 'formal grammar' and uses 'formal semantics' as I do. But calls both together 'formal grammar'.

All issues of trying to precisely define mathematical fields aside, rules of inference are grammar, usually explicitly so.

I would call rules of inference the formal semantics, but I guess this is probably a thing where many people use different words for same, so to completely clarify how I use my terms:

1: Formal grammar with respect to an alphabet A.
A subset of A*, which we will call 'legal', or the mechanism to define it.

2: Formal semantics with respect to a formal grammar G:
A set of rules which define specifically what subset of G is closed under the operation of inference, alternatively, the definition of the operation of inference on G.

3: Meaning
- vague -

Semantics is quite literally the study of meaning. At this time, Wikipedia has it right, so go look since you seem to take it as an authority.

Naïve semantics perhaps, but as Wikipedia in the article of formal grammar points out. 'formal semantics' is little more than some string manipulation rules in standard jargon.

I didn't invent the term, I just use it the same way the books I read do basically.

Formal semantics is merely semantics as applied to formal languages and what-not. A typical mathematical application is model theory -- how to interpret strings of symbols as referring to mathematical objects or assertions about them.

I think this is the part where you use your terms nonstandardly and what causes our confusion. Formal semantics, inherent to the word 'formal' says nothing about interpretation in standard usage of the term. The formal semantics of a formal language are string manipulation rules. This is a difference with an informal semantics.

Only a very extreme sort of formalism.

Well, this 'bottom' is the only that I call 'formalism', the rest can be called 'rigorous' I suppose, subjectively.

Formalism in general does not require a dogmatic assertion that one may not assign meaning to strings of symbols -- it only requires that you play the symbol pushing game as a symbol pushing game; no "cheating" by asserting some statement must be true by a non-symbol pushing argument. Either prove it by pushing symbols, or admit that you are simply adding it in as another hypothesis.

Of course, there is no difference if you assign some mental meaning to it or not. But the meaning itself is irrelevant and 'outside the scope of the debate', as I said before.