Some points on mathematical logic and "rigor"

For the discussion of math. Duh.

Moderators: gmalivuk, Moderators General, Prelates

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Some points on mathematical logic and "rigor"

Postby Pietro » Sat Jul 11, 2009 7:12 am UTC

Dear forum,

quite recently, there were a couple of threads on "rigor" in mathematics, and the inevitable accompanying discussion of mathematical logic and its perceived achievements. At least one forum member felt that "rigor" is a newcomer to mathematics, originating only "100 years ago", presumably brought on by the development of logic.

Since I was not able to respond timely to the appropriate threads, and they seem to have reached the point of diminishing returns (too many posts, no one really reading it all), I thought I would clarify some points here. First, because there seems to be significant interest in these matters, even among non-mathophiles, with everyone and their grandmother constantly quoting Gödel's theorems, Douglas Hofstadter etc. Second, because these are my fields of expertise (I have BA in math, an MSc in mathematical logic, and will start a PhD in math in September), it pains me a little to see them oft misinterpreted. Third, being of a somewhat academic bent, it bothers me a little that people sometimes talk about things they have hardly looked into at all, and make grand, sweeping statements which, even if true, would take hundreds of pages to justify properly.

There are two main points that I wish to make:

(1) Mathematical logic did not bring into mathematics a rigor that was altogether lacking before. Moreover, the much-vaunted concept of a "formal system" is not the magic wand that many people outside of logic believe it to be. Casting a piece of mathematics in a formal system does not, and cannot, constitute an expression of ultimate, all-encompassing rigor and certainty. In particular, trying to make elementary number theory and combinatorics "rigorous" by formalizing them is a circular enterprise.

(2) It is meaningless to analyse the mathematics of the past in terms of the mathematics of today. Today we have not only new theorems, but new, and often incompatible, ways of expressing things. Further, the "unwritten rules" at play in our minds when we read math --- the larger context in which we understand the material --- are very different.

I will develop these points at length in succeeding posts.
Last edited by Pietro on Sun Jul 12, 2009 7:40 am UTC, edited 1 time in total.
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

User avatar
t0rajir0u
Posts: 1178
Joined: Wed Apr 16, 2008 12:52 am UTC
Location: Cambridge, MA
Contact:

Re: Some points on mathematical logic and "rigor"

Postby t0rajir0u » Sat Jul 11, 2009 7:24 am UTC

Pietro wrote:(1) Mathematical logic did not bring into mathematics a rigor that was altogether lacking before. Moreover, the much-vaunted concept of a "formal system" is not the magic wand that many people outside of logic believe it to be. Casting a piece of mathematics in a formal system does not, and cannot, constitute an expression of ultimate, all-encompassing rigor and certainty.

Hear, hear. The community standards for what constitutes an acceptable proof are just that; standards. They vary over time like any other set of standards.

Gian-Carlo Rota has a lot of good stuff to say about this subject. He observes in Indiscrete Thoughts, for example, that mathematicians constantly try to recast old results in terms of new axioms, and that some objects such as the real line have been axiomatized seven or more times. If you think making a result rigorous is the only reason to formalize it, you can't explain why mathematicians do this.

Pietro wrote:(2) It is meaningless to analyse the mathematics of the past in terms of the mathematics of today. Today we have not only new theorems, but new, and often incompatible, ways of expressing things. Further, the "unwritten rules" at play in our minds when we read math --- the larger context in which we understand the material --- are very different.

I'm not sure in what sense you mean this. Are you saying this along the same lines as a historian stating that it's meaningless to analyze the cultural standards of the past in terms of the cultural standards of the present? In that sense, I fully agree.

User avatar
skeptical scientist
closed-minded spiritualist
Posts: 6142
Joined: Tue Nov 28, 2006 6:09 am UTC
Location: San Francisco

Re: Some points on mathematical logic and "rigor"

Postby skeptical scientist » Sat Jul 11, 2009 7:46 am UTC

Pietro wrote:(1) Mathematical logic did not bring into mathematics a rigor that was altogether lacking before. Moreover, the much-vaunted concept of a "formal system" is not the magic wand that many people outside of logic believe it to be. Casting a piece of mathematics in a formal system does not, and cannot, constitute an expression of ultimate, all-encompassing rigor and certainty. In particular, trying to make elementary number theory and combinatorics "rigorous" by formalizing them is a circular enterprise.

Indeed. The reason formal systems are interesting objects of study is not because they are the perfect example of what mathematics is, but rather because they provide a good mathematical model of what mathematicians do, in the same way that (for example) manifolds are interesting because they provide a good mathematical model for curved space. A mathematical proof is not a formal deduction, but studying formal deductions is a good way of studying mathematical proofs because it they are concrete and well defined objects which are similar in nature to the proofs that actual mathematicians produce.
I'm looking forward to the day when the SNES emulator on my computer works by emulating the elementary particles in an actual, physical box with Nintendo stamped on the side.

"With math, all things are possible." —Rebecca Watson

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Sat Jul 11, 2009 7:48 am UTC

Let's tackle point (1). I'll start by reviewing a paradigmatic argument about the "lack of rigor" of earlier mathematicians, presented by forum member Gaydar2000SE's. It is well-known that Euclid's Elements contains a proof that there are an infinite number of primes. Gaydar2000SE contends that this proof is "not rigorous" in many ways, e.g. that Euclid does not state as an axiom, nor proves, that there is a total order on the natural numbers.

For definiteness, here is an abridged version of Euclid's proof in modern notation (basically replacing things like "the segment AB" by "the number n"):

In The Elements, Book VII, Proposition 31, Euclid wrote:Every number greater than 1 is divisible by a prime number. (For Euclid, "number" denotes multiplicity, so any "number" is greater than 1; 1 itself is a/the "unit".) Proof: Let n>1. If n is not divisible by any 1<m<n, then n itself is prime, and, dividing itself, satisfies the Proposition. On the other hand, if some 1<m<n divides n, apply the same reasoning to m. Either m is prime, or there is 1<m'<m dividing m, etc. Proceeding in this way, we cannot obtain an infinite descending sequence of natural numbers n>m>m'>m''>..., because there are only n numbers between 1 and n. Therefore, in at most n steps we must obtain an m''' which is prime, and divides m'', which divides ... , which divides m, which divides n. Therefore, m''' is prime and divides n, as was to be shown. Q.E.D.


In The Elements, Book IX, Proposition 20, Euclid wrote:Prime numbers are more than any assigned multitude of prime numbers. Proof: Suppose there were only N prime numbers, and call them p1,p2,...,pN. Then the number q = p1*p2*...*pN + 1 is not divisible by any of these primes. However, by VII.31, it must be divisible by some prime, q'. Therefore, p1,p2,...pN,q' is a bigger set of primes than initially supposed. Q.E.D.


(It's easy to forget just how elegant this argument is.)

It is quite true that Euclid does not state or prove that "any two numbers are comparable". One reason (foreshadowing point (2)) is that, for Euclid, "numbers" are multiples of a given line segment (in particular, all numbers are relative to some "unit"), and so are line segments themselves. Now, it is quite plain (for him) that any two line segments are either equal, or one is less than the other. He does not state as much in the Definitions, nor the Postulates, nor the Common Notions in Book I, and assumes it already in Proposition 3, where he gives a construction "to cut off from the greater of two given unequal straight lines a straight line equal to the less".

And not only is it plain to him, but should be plain to us, if we know what a line segment is: if we draw two line segments s,t starting from the same point P, and in the same direction (i.e. if s,t share at least one point other than P), then either they end in the same spot, or one "runs out" sooner. The only possible objection to the comparability of line segments, viz. "what if the two line segments start at different points, or go in different directions?", is dealt with by Proposition 2, which gives a construction "to place a straight line equal to a given straight line with one end at a given point". (Proving even this is, right there, more rigor than you'll find in the majority of textbooks or papers out there today.)

But I would like to pursue a different counter-argument, more directly related to (1).
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Sat Jul 11, 2009 7:58 am UTC

t0rajir0u and skeptical scientist: I'm glad you found my post to be of interest. I agree with both your statements on point (1), and they are important things to keep in mind. Nevertheless, I would like to address more directly the question "do mathematical logic and formal systems provide a greater degree of certainty of the results?" Sometimes this is the case; for example, a lot of the differential geometry that people do intuitively can be "formalized" in terms of real numbers and differentiable functions, on which we sometimes feel we have a better handle than on the original objects. However, a lot of people take this to extremes that do not stand up to close scrutiny, which is the case for elementary finitary reasoning. I hope to give concrete arguments for this view in a little while.

t0rajir0u, regarding point (2), I hope to make myself clearer in the following posts.
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

achan1058
Posts: 1783
Joined: Sun Nov 30, 2008 9:50 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby achan1058 » Sat Jul 11, 2009 7:58 am UTC

You do know that the thread was locked for a reason, right? Namely that he is so out of touch with reality of most mathematicians. There's no need to respond to it further, in my opinion.

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Sat Jul 11, 2009 9:36 am UTC

Continuing with point (1) and the objection that Euclid does not state nor prove the comparability of any pair of natural numbers. One thing the objector claimed was that this was dealt with by the advent of "rigor" a hundred years ago, where people started writing down explicit axiom systems and saying things like
[math]\forall x \forall y (x=y \lor x<y \lor y<x)[/math]
But does an axiom system really have this near-magical power of making our intuition of the natural numbers unnecessary? Well, let's look at the weakest axiom systems that can do much of anything, namely Robinson's Q or Peano Arithmetic. Both of these are expressed in the language of first-order logic with equality, with extra-logical symbols {S,+,*,0}. Both Q and PA have their own set of non-logical axioms (like "(Sx = Sy) → x = y"), but for the purposes of this argument it will suffice that they also include the usual axioms of first-order logic (like "x=y → Sx=Sy"), without which they could hardly deduce anything.

The thing about the axioms and rules of first-order logic (or propositional logic, or much any logic that anyone studies anywhere) is that they are schematic. Indeed, this is the entire point of logic: it is the study of those rules of reasoning that are independent of the subject matter reasoned about. So, for example, A→(B→A) is an axiom schema, meaning that it is not an actual axiom in the language, but that it will yield an axiom once we substitute any formulas in the language for A and B. For example, if a,b,x,y are variables in the language, then the following is an axiom:
[math]x=y \rightarrow (a=b \rightarrow x=y)[/math]
Similar comments apply to schematic inference rules like modus ponens (from A and A→B deduce B).

Now, if we want to use our axiom system to prove things, then we must certainly be able to recognize which sentences are axioms, and which are not. Otherwise, how would we know where to start our proofs? And here's the thing: how do you check that
[math]\begin{array}{cc}(((p \rightarrow q)\rightarrow (p\rightarrow r))\rightarrow(((u\rightarrow v)\land (v \lor (w\rightarrow x)))\lor(s\rightarrow(s\rightarrow t)))) \rightarrow ((((q \rightarrow p)\rightarrow (p\rightarrow r))\rightarrow(((u\rightarrow v)\land (v \lor (w\rightarrow x)))\lor(s\rightarrow(s\rightarrow t)))) \rightarrow \\ (((p \rightarrow q)\rightarrow (p\rightarrow r))\rightarrow(((u\rightarrow v)\land (v \lor (w\rightarrow x)))\lor(s\rightarrow(s\rightarrow t)))))\end{array}[/math]
is an instance of A→(B→A)?

Of course, there's an easy answer: you just count the parentheses (that's what they're there for) and find the formulas A,B which yield the sentence above when substituted into the schema A→(B→A). Counting --- that's the tricky activity you've been trying to formalize yourself out of, pretending you didn't know what the natural numbers were. Counting parentheses in the order in which they appear --- but weren't you pretending not to know that the natural numbers are totally (and discretely!) ordered? To avoid this, you could write a simple Turing machine program to do the checking for you. Hell, a pushdown automaton will do. But wait, how do you prove that it does what you want it to? There's an easy proof using induction on the length of the input --- and no other proof that does not involve some rather detailed knowledge of the structure of the natural numbers.

A formal system can be great for keeping track of how non-obvious things (like Croot's solution of the Erdos-Graham problem) follow from things you know, or for studying exactly what kind of logical principles are needed to prove a strong theorem. But it cannot, ever, explain to you what the natural numbers are, if you don't know. You would not be able to tell which strings of symbols were formulas, which formulas were axioms, or which sequences of formulas were proofs. (The order in which formulas appear in a proof is a crucial ingredient.) In fact, you would not even understand the definitions of these items, since they are all of the form "X is a sequence of Ys such that..."

Therefore, not stating nor proving that the natural numbers are totally ordered is not lack of rigor. Euclid's number theory is as (or more) rigorous as today's. The same goes for Euler, Gauss, and all those folks who lived before the 20th century.

[Edit: achan1058, hopefully other people besides Gaydar2000SE will find some of this clarifying. Hopefully he himself will too.]
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

phr34k
Posts: 58
Joined: Mon Dec 31, 2007 5:59 am UTC

Re: Some points on mathematical logic and "rigor"

Postby phr34k » Sat Jul 11, 2009 4:11 pm UTC

I am going to ramble on for a bit, mostly because my writing style is piss poor. Apologies for unreadable things.

Pietro wrote:(1) Mathematical logic did not bring into mathematics a rigor that was altogether lacking before. Moreover, the much-vaunted concept of a "formal system" is not the magic wand that many people outside of logic believe it to be. Casting a piece of mathematics in a formal system does not, and cannot, constitute an expression of ultimate, all-encompassing rigor and certainty. In particular, trying to make elementary number theory and combinatorics "rigorous" by formalizing them is a circular enterprise.


Heh, I remember the first time when I discovered that "formal systems" were not the magic I needed, which was when I started reading George Tourlakis' Lectures on Logic & Set Theory. Reading Vol. 1, I was made aware of the distinction between Theory and Meta-theory (meta-theory being the usual "English" in which we talk about math, theory being the abstract formal statements that we express as a language of variables, parentheses, conjunctions and quantifies, that that then is parsed along with some truth valuation, yadda-yadda). I remember reading that and thinking "Man... this is really cool, but it's also completely irrelevant from what I thought it would be!"; and what I thought formalism would be was a way to gain an understanding or an intuition about the various mathematical objects I was grapling with.

But no, formalism is not a means to understand (for me it's not anyway), it's a means to express, to communicate and write down things, which incidentally is, I realize now, what originally was the trouble that drove me to formalism to being with. In other words, the capital-P Problem of mathematics that knowing how to be rigorous and formal in your statements addresses is not the problem of whether a statement is true, but the problem of how to express and write down that same statement for someone else to understand.

So to me, the question of rigor is a question of communication, which harks back the point that the standards of rigor are the communal, but not universal. To recast what I'm going to term "the rigor wars" that raged from the 17th century until the middle of the 20th, what actually happened was that the mathematical community had not agreed on standards of rigor, and that disagreement took the form of seemingly legit modes of inference producing conflicting results (e.g. playing around with the terms of an arbitrary series used to be a commonly accepted technique, but it gave different answers to the same question, when employed on series that we know say don't converge absolutely). As time went on, the modes of inference got pushed down deeper and deeper into the framework until set theory came about (and set theory came about to account for the notion of infinitely big sets, which came to account for a definition of the real line (Dedekind cuts), which came to account for Weierstarss definition of limits/continuity, which came to dispense with/account for infinitesimals in calculus). Once set theory entered the scence, all modes of inferences were pushed down to logical problems and logical assumptions, leaving all higher mathematical structures free to be axiomatized in whatever way we want. Which is why nowadays we make distinctions that back then in the good old days were never made as they were commonly accepted.

To finish off, a quote from Scott Aaronson, regarding how rigor and proof and all that are plausibly subjective experiences; source is here: http://www.scottaaronson.com/democritus/lec4.html

Scott Aaronson wrote:Now, is there anything else that also produces the feeling of absolute certainty? Right -- math! Incidentally, I think this similarity between math and subjective experience might go a long away toward explaining mathematicians' "quasi-mystical" tendencies. (I can already hear Greg Kuperberg wincing. Wince, Greg, wince!) This is a good thing for physicists to understand: when you're talking to a mathematician, you might not be talking to someone who fears the real world and who's therefore retreated into intellectual masturbation. You might be talking to someone for whom the real world was never especially real to begin with! I mean, to come back to something we mentioned earlier: why did many mathematicians look askance at the computer proof of the Four-Color Theorem? Sure, the computer might have made a mistake, but humans make plenty of mistakes too!

What it boils down to, I think, is that there is a sense in which the Four-Color Theorem has been proved, and there's another sense in which many mathematicians understand proof, and those two senses aren't the same. For many mathematicians, a statement isn't proved when a physical process (which might be a classical computation, a quantum computation, an interactive protocol, or something else) terminates saying that it's been proved -- however good the reasons might be to believe that physical process is reliable. Rather, the statement is proved when they (the mathematicians) feel that their minds can directly perceive its truth.

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Thu Jul 16, 2009 7:08 am UTC

t0rajir0u wrote:Hear, hear. The community standards for what constitutes an acceptable proof are just that; standards. They vary over time like any other set of standards.


I sympathize with one possible reading of your post, but maybe there's room for misunderstanding. I don't think you misunderstand anything, judging by your extremely interesting math blog, but other readers might, so maybe a short clarificatory reply is in order.

Though the standards of proof do vary, they do not vary randomly. This is especially clear with elementary number theory and combinatorics, where the standards of proof have varied, well, not at all. More generally, the standards of proof change in response to perceived shortcomings in the current standards; and these can only be shortcomings relative to some higher goal, be it greater readability, precision or certainty in the resutl proved.

If this were not the case, you'd be left with the classic Euthyphro problem of "are some proofs correct because they follow the standards, or do the standards prefer those proofs because they are correct?"
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

User avatar
antonfire
Posts: 1772
Joined: Thu Apr 05, 2007 7:31 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby antonfire » Thu Jul 16, 2009 7:38 am UTC

Pietro wrote:Though the standards of proof do vary, they do not vary randomly. This is especially clear with elementary number theory and combinatorics, where the standards of proof have varied, well, not at all.
Standards for the loosest acceptable proof for a*0=0 vary from "it's obvious" to the full axiomatic proof with justifications for each step. Most people put it somewhere in between, but where in between depends pretty heavily on the person and the context.

For combinatorics, the variety is even greater. Some people are, e.g., unsatisfied with proofs that use generating functions because they want to see why an equality holds, which usually means constructing an explicit bijection between two sets. Some people will give up their generating functions only if you pry them from their cold, dead fingers.


As you say, though, these preferences generally aren't arbitrary. More or less like any other set of preferences.
Jerry Bona wrote:The Axiom of Choice is obviously true; the Well Ordering Principle is obviously false; and who can tell about Zorn's Lemma?

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Thu Jul 16, 2009 10:36 am UTC

antonfire wrote:Standards for the loosest acceptable proof for a*0=0 vary from "it's obvious" to the full axiomatic proof with justifications for each step.


I'm not sure if you meant to pick any example and went with "0=0" by accident, but it's not a good one. In fact, "0=0" is an equality axiom (a substitution instance of x=x), and "proofs" only range from "it's what we mean by equality" to "it's a logical axiom", the latter meaning much the same as the former. Perhaps your argument would work better with "1+1=2". [Edit: misread antonfire, forget this.]

Even under that interpretation, I don't agree with your point. The folklore 100+-page proof of "1+1=2" in Russel-Whitehead was not an attempt to establish the arithmetical fact per se, but a proof-of-concept of the idea that you can base all mathematics on logic alone (in a very technical and precise sense of "logic"). As I've argued above, you can't set up a formal system while pretending not to know anything about the natural numbers. (Functions and relations have arities!) Moreover, the entire "crisis of foundations" thing was a 40-year blip in the 2500+-year history of math. Outside of that, things have been pretty stable with elementary number theory.

antonfire wrote:For combinatorics, the variety is even greater.


The adjective "elementary" in "elementary number theory and combinatorics" was supposed to encompass "combinatorics" as well. Obviously, today you've got some high-powered combinatorics that depend on algebraic topology and even large cardinal axioms. I was talking about the kind of simple counting argument that is part and parcel of elementary number theory. The "set systems" papers of Erdos (Erdos-Ko-Rado, deBruijn-Erdos, Erdos's extension of Sperner's theorem in connection with the Littlewood-Offord problem etc) also fit that description. This sort of combinatorics has not seen any change in proof standards. (Look at Euclid's proof of the infinitude of primes, or pretty much anything in books VII--IX of The Elements; at Euler's work in combinatorics, or Gauss's Disquisitiones.)

As you say, though, these preferences generally aren't arbitrary. More or less like any other set of preferences.


Forgive me if my English is sub-par, but "preference" is a word with deeply psychological connotations for me. In a certain sense, I can "prefer" whatever I want and still be using "prefer" in its proper sense. However, you cannot "prefer" a proof of the Riemann hypothesis that is simply a check of the first 100 cases. That is not a proof at all. I believe that the word "strategy" would be a better fit: we have a goal in mind (establishing true and interesting results), and change our strategies to better achieve it.
Last edited by Pietro on Thu Jul 16, 2009 10:43 am UTC, edited 1 time in total.
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

Token
Posts: 1481
Joined: Fri Dec 01, 2006 5:07 pm UTC
Location: London

Re: Some points on mathematical logic and "rigor"

Postby Token » Thu Jul 16, 2009 10:38 am UTC

Pietro wrote:
antonfire wrote:Standards for the loosest acceptable proof for a*0=0 vary from "it's obvious" to the full axiomatic proof with justifications for each step.


I'm not sure if you meant to pick any example and went with "0=0" by accident, but it's not a good one. In fact, "0=0" is an equality axiom (a substitution instance of x=x), and "proofs" only range from "it's what we mean by equality" to "it's a logical axiom", the latter meaning much the same as the former. Perhaps your argument would work better with "1+1=2".

Umm... you've clearly quoted him saying "a*0=0", not "0=0".

Pietro wrote:Forgive me if my English is sub-par, but "preference" is a word with deeply psychological connotations for me. In a certain sense, I can "prefer" whatever I want and still be using "prefer" in its proper sense. However, you cannot "prefer" a proof of the Riemann hypothesis that is simply a check of the first 100 cases. That is not a proof at all. I believe that the word "strategy" would be a better fit: we have a goal in mind (establishing true and interesting results), and change our strategies to better achieve it.

I think antonfire was talking about preferences for different kinds of valid proofs, not preferring invalid proofs. That doesn't follow at all from what he was saying.
All posts are works in progress. If I posted something within the last hour, chances are I'm still editing it.

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Thu Jul 16, 2009 10:42 am UTC

To get back on topic, I just wanted to make clear my original point. I first said that "formal systems are not the holy grail", and t0rajir0u said something that could be read as, "yeah, everyone does math their own way, and formal systems are as good as anything else". (I don't think for one minute that he meant this, only that it could be read as such by someone less experienced.)

I just wanted to clarify that I had a very particular, concrete criticism of the view "formal systems give rigor to elementary number theory". It's not that they are as good as other approaches; it's that this view of rigor does not make sense, since you need to be capable of elementary finitary reasoning to even understand what a formal system is!
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Thu Jul 16, 2009 11:12 am UTC

Token wrote:I think antonfire was talking about preferences for different kinds of valid proofs, not preferring invalid proofs. That doesn't follow at all from what he was saying.


I don't think antonfire advocates invalid proofs. Antonfire is probably every bit as able at mathematics as I am, or more.

Nevertheless, when antonfire says "much like any other set of preferences", it invites comparison with, well, other sets of preferences. And the thing about preferences (as I understand them) is that they are completely subjective, which, I feel, makes for a poor analogy and choice of words. The fact that you're only supposed to prefer "valid" proofs shows that proof standards are not a simple matter of preference.

Feel free to write this off as pedantry.
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

User avatar
antonfire
Posts: 1772
Joined: Thu Apr 05, 2007 7:31 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby antonfire » Thu Jul 16, 2009 1:31 pm UTC

I think standards for validity have shifted slightly for proofs in elementary number theory and elementary combinatorics. This is an unimportant point, though, and I don't feel like arguing for it. It's clear, anyway, that overall standards of validity have shifted over the last few centuries (Euler's proof that [imath]\sum_{n\geq 1} n^{-2} = \frac{\pi^2}{6}[/imath] wouldn't be considered valid today, nor even Riemann's proof of the prime number theorem).

I very much do want to invite comparison of the "validity" of a proof to other properties by which we judge it. What makes validity (as we interpret that word today) so special? What do we even mean by validity?

What you said about standards of proof applies to just about any other way to judge one proof to be "better" than another. People's preferences for or against certain types of proofs vary, but they don't vary randomly. They're inspired by perceived shortcomings in a certain type of proof, and perceived advantages in some other type. Our preferences are not completely subjective, any more than our judgment of validity is.


Joseph McCombinatorialist might prefer a combinatorial proof that [imath]F_{n+2} = 1+\sum_{0 \leq k \leq n} F_k[/imath] to one with generating functions because it not only proves the equality of the numbers but also provides a useful bijection between two sets.

Doron Zielberger might prefer[ps] a proof for Fermat's Last Theorem which does not use real analysis, because he considers proofs that use non-finite concepts to be non-rigorous, because he believes that only discrete things are "real".

As Scott Aaronson points out, many mathematicians would prefer a human-readable proof of the Four-Color Theorem, despite the fact that the computer-checked one is as valid as any other, because they'd like their minds to directly perceive its truth.


Like it or not, whether a proof is valid is not the only standard by which we judge it. We reject invalid proofs, and we reject utterly incomprehensible proofs.[1] Some of us reject nonconstructive proofs, some of us reject infinity-based proofs. We prefer effective proofs, we avoid proofs by contradiction. Sometimes we strive for an elementary proof; sometimes we try to abstract away the details. Some of us adore "slick" proofs; some detest them.



Yes, I think a formally valid proof is sometimes preferable to the same proof written naively. I like a constructive proof better than a nonconstructive one as well. Neither of these is an arbitrary preference - both are motivated. But both are reflections of the way mathematicians like to do things today, not some universal timeless standard. Our preferences have simply shifted over time to align this way. Does this mean our preferences are useless, or arbitrary? Of course not.


[1]: We don't completely reject either, of course. Generally, we strive to modify both into valid, comprehensible proofs.
Jerry Bona wrote:The Axiom of Choice is obviously true; the Well Ordering Principle is obviously false; and who can tell about Zorn's Lemma?

ThomasS
Posts: 585
Joined: Wed Dec 12, 2007 7:46 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby ThomasS » Thu Jul 16, 2009 2:03 pm UTC

It is possible to build up and write down quite a bit of mathematics at a level so detailed that a computer could check it, starting with appropriately phrased Peano axioms, maybe the axiom of choice, and so on. I have heard it said that somewhere in Bertrand Russell's work there is the line "this is what we'll use to prove that 1+1=2", and it is this sort of project which makes such comments meaningful. While most theorem proving systems and examples are focused on topics related to computer science, HOL for example does come with a collection of theorems about arithmetic.

I like to think that the question today is whether the readers of a proof believe that a "true" formal proof can be found from what is written using techniques that the reader considers obvious or is otherwise willing to take for granted. I also like to think that if more than 1-2 mathematicians believe that a proof is valid in this sense, then it probably is. If the proof is valid in this sense, then we have some confidence that the proof is correct and that a counter example won't appear. However, incorrect proofs have been published and different subfields of mathematics have different standards and expectations.

User avatar
t0rajir0u
Posts: 1178
Joined: Wed Apr 16, 2008 12:52 am UTC
Location: Cambridge, MA
Contact:

Re: Some points on mathematical logic and "rigor"

Postby t0rajir0u » Fri Jul 17, 2009 4:57 am UTC

Pietro wrote:The fact that you're only supposed to prefer "valid" proofs shows that proof standards are not a simple matter of preference.

People who think this are under the impression that every accepted mathematical proof is 100% rigorous. In practice, very few proofs have undergone complete formalization a la MIZAR. Most mathematicians leave out unimportant steps in their proofs and the like, and occasionally this can lead to minor or even serious mistakes. Most important proofs have not been completely formalized.

A big question, then, is how much checking you're willing to do to make sure a proof is correct. In practice, proofs that were later found to have serious mistakes in them tend to be repairable, usually because the mathematician who made that mistake was using the correct "global" picture but got a few details wrong. We think of Euler as a great mathematician even though he doesn't stand up to modern standards of rigor because his "global" picture allowed him to work beyond the tools he currently had and give "proofs" of results that were later formalized in the appropriate setting.

The point here is that doing mathematics in an environment where Euler-style proofs are accepted or even encouraged is very different from doing mathematics in an environment where only formal proofs are accepted, and our location in the spectrum is a cultural fact about mathematicians now, not a universal fact about mathematics forever.

User avatar
Pietro
Posts: 42
Joined: Mon Jan 21, 2008 2:30 pm UTC
Location: Campinas -- Brazil
Contact:

Re: Some points on mathematical logic and "rigor"

Postby Pietro » Fri Jul 17, 2009 8:59 am UTC

antonfire wrote:I very much do want to invite comparison of the "validity" of a proof to other properties by which we judge it. What makes validity (as we interpret that word today) so special? What do we even mean by validity?


We seem to be talking at cross-purposes. I'm using "validity" of a proof to mean that the result it establishes is true, or, in less concrete areas, that it follows from common assumptions on the concepts involved. From what I said in my first posts, it should be obvious that I do not equate this with "proof in a formal system".

Validity is more special than any other aspect of proofs, since it is the whole point of having proofs. If you cared about brevity as much as about validity, you would be quite content to prove the Riemann hypothesis thus: "1+1=2. Therefore RH." But you don't see this published, whereas any 1000-page real proof of RH would be published instantly.

I don't think we're disagreeing over anything. I for one cannot disagree with anything from your previous post, other than the usage of "preference". I understand the meaning you assign to it, and agree with that; I would just use a different word (like "strategy"). Of course different people prefer different things, but, when it comes to mathematical proofs, their choices are so severely restricted by the requirement of truth that I find it odd to say "like any other set of preferences". (This brings to mind favorite colors, favorite dishes etc.)

To make an analogy, it would sound weird to me if someone said, "how you build a flying machine is a matter of preference". Well, yes, there is some preference involved, but surely the main aspect of the enterprise is overcoming gravity?

Pietro wrote:The fact that you're only supposed to prefer "valid" proofs shows that proof standards are not a simple matter of preference.

t0rajir0u wrote:People who think this are under the impression that every accepted mathematical proof is 100% rigorous.


Like most members who grace the Mathematics board, I have had an extensive education in math, and come into quite a bit of contact with research. It would be courteous not to assume that everyone is a high school student, with silly opinions and little information.

t0rajir0u wrote:Our location in the spectrum is a cultural fact about mathematicians now, not a universal fact about mathematics forever.


I never said anything contrary to this. I only pointed out that "proof standards are just that, standards" and "like any other set of preferences" are a very poor and superficial way to express the mutability of proof standards. (Again, I don't think that either of you actually holds a superficial view on the matter.)

Anyhow, my original comment on this topic was meant to be a very minor and obvious point to anyone moderately versed in mathematics, only designed to avoid misleading the casual lay reader. I'm not sure how it turned into such a long discussion, with everyone saying things that everyone knew, but somehow managing to disagree.

I hope to dispel the impression that I am a "proof standard nazi" in my next post, treating point (2). (Again, in a very concrete manner, with actual historical examples and evidence.)
I always wondered about the meaning of life. So I looked it up in the dictionary under "L" and there it was --- the meaning of life. It was not what I expected. (Dogbert)

User avatar
antonfire
Posts: 1772
Joined: Thu Apr 05, 2007 7:31 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby antonfire » Fri Jul 17, 2009 4:59 pm UTC

Pietro wrote: I'm not sure how it turned into such a long discussion, with everyone saying things that everyone knew, but somehow managing to disagree.
You must be new here.

I don't think we're really disagreeing on anything factual. I just like to ramble about this stuff as much as almost any person in this thread.

Pietro wrote:I'm using "validity" of a proof to mean that the result it establishes is true, or, in less concrete areas, that it follows from common assumptions on the concepts involved. From what I said in my first posts, it should be obvious that I do not equate this with "proof in a formal system".
Hah, but then "1+1=2, therefore Fermat's Last Theorem" is a valid proof. Yes, yes, I know this isn't what you actually mean by "validity", but it just goes to show how hard the concept is to define without bringing formal systems (or social facts about mathematicians) into it. Even if you do bring in social facts about mathematicians, I don't think it's that easy to define.
Jerry Bona wrote:The Axiom of Choice is obviously true; the Well Ordering Principle is obviously false; and who can tell about Zorn's Lemma?

AhIB
Posts: 18
Joined: Thu Nov 26, 2009 3:05 am UTC

Re: Some points on mathematical logic and "rigor"

Postby AhIB » Thu Nov 26, 2009 11:36 am UTC

I can't say anything about Wiles' proof of Fermat's last theorem, but I can give a short and easy reading direct proof of Fermat's last theorem :

Fermat’s Last Theorem :
« It is impossible to separate a cube into two cubes, or a biquadrate into two biquadrates, or in general any power higher than the second into two like powers. I have discovered a truly marvelous proof which this margin is too narrow to contain. »

Abstract :
A property P or notP is attached to all power a^n , P(a^n) or ¬P(a^n) :
P(a^n) = " power a^n is sum or difference of two like powers."
¬P(a^n) = " power a^n isn’t sum or difference of two like powers."

Use of rules of mathematical bivalent logic to establish a property inherited by coprime factors of power equal to sum or difference of two like powers.

Establishment of a reduction rule or "finite descent" method :
Theorem F (F : tribute to Fermat) :
If a power of degree n is sum or difference of two like powers, it is true also for its prime factors.

Abel’s conjecture :
( z, y, x, n € N+, n>2) (< z,y,x >=1, z^n = y^n + x^n)
---> none of z, y, x can be prime-powers.

Theorem A (A : tribute to Abel) :
A prime-power of degree n>2 can't be sum or difference of two like prime-powers.

Conclusion :
A power of degree n>2 can't be sum or difference of two like powers.

happy-arabia.org/FLT proof.pdf

Ahmed Idrissi Bouyahyaoui
Attachments
FLT proof.pdf.pdf
(474.91 KiB) Downloaded 61 times

User avatar
skeptical scientist
closed-minded spiritualist
Posts: 6142
Joined: Tue Nov 28, 2006 6:09 am UTC
Location: San Francisco

Re: Some points on mathematical logic and "rigor"

Postby skeptical scientist » Thu Nov 26, 2009 12:13 pm UTC

Before you try proving Fermat's last theorem, you may want to work on basic rules of quantifier logic. A good general rule is that it's best to understand at least a little undergrad math before trying to come up with an original proof of a theorem that took real mathematicians several centuries to prove.

For example, in your claimed "proof" of the reduction rule, you claim that [math](\forall \overline x) \, [ A(\overline x) \Rightarrow (B(\overline x) \lor \lnot B(\overline x))][/math] is equivalent to [math](\forall \overline x) \, [A(\overline x) \Rightarrow B(\overline x)] \quad \lor \quad (\forall \overline x) \, [A(\overline x) \Rightarrow \lnot B(\overline x)],[/math] which is very much not the case.

To see the difference, imagine that the [imath]\forall x[/imath] quantifies over cars in the world, A(x) is the statement "the car x is in Chicago", and B(x) is the statement "the car x is red". Then the first statement above asserts that every car in Chicago is either red or not red, which is true, while the second statement asserts that either every car in Chicago is red or every car in Chicago is not red, which is false.
Last edited by skeptical scientist on Thu Nov 26, 2009 12:20 pm UTC, edited 1 time in total.
I'm looking forward to the day when the SNES emulator on my computer works by emulating the elementary particles in an actual, physical box with Nintendo stamped on the side.

"With math, all things are possible." —Rebecca Watson

User avatar
Oort
Posts: 522
Joined: Fri Sep 29, 2006 10:18 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby Oort » Thu Nov 26, 2009 12:17 pm UTC

antonfire wrote:We prefer effective proofs, we avoid proofs by contradiction.

A little off-topic here, but do mathematicians try to avoid proof by contradiction? I imagined they were popular...

User avatar
skeptical scientist
closed-minded spiritualist
Posts: 6142
Joined: Tue Nov 28, 2006 6:09 am UTC
Location: San Francisco

Re: Some points on mathematical logic and "rigor"

Postby skeptical scientist » Thu Nov 26, 2009 12:28 pm UTC

Oort wrote:
antonfire wrote:We prefer effective proofs, we avoid proofs by contradiction.

A little off-topic here, but do mathematicians try to avoid proof by contradiction? I imagined they were popular...

No, not really, but there are times when a direct proof tells you more than a proof by contradiction. For example, the standard proof of Brouwer's fixed point theorem is a proof by contradiction, which tells you that a fixed point of certain functions exists, but doesn't really help you find it. On the other hand, the standard proof of the Banach fixed point theorem is a direct, constructive one, which tells you not only that a fixed point exists (under different hypotheses on the function), but also how to find it. Mathematicians generally prefer constructive proofs to non-constructive proofs because they actually give you more information, which is why direct proofs are sometimes preferred. So it's not a matter of avoiding proof by contradiction - a proof by contradiction is still a proof - but sometimes a direct proof is better.
I'm looking forward to the day when the SNES emulator on my computer works by emulating the elementary particles in an actual, physical box with Nintendo stamped on the side.

"With math, all things are possible." —Rebecca Watson

User avatar
Talith
Proved the Goldbach Conjecture
Posts: 848
Joined: Sat Nov 29, 2008 1:28 am UTC
Location: Manchester - UK

Re: Some points on mathematical logic and "rigor"

Postby Talith » Thu Nov 26, 2009 1:17 pm UTC

I would say that if a proof gives you more information than another proof then it's a proof of a more detailed theorem rather than it just being a 'better proof' of the original theorem.

Tirian
Posts: 1891
Joined: Fri Feb 15, 2008 6:03 pm UTC

Re: Some points on mathematical logic and "rigor"

Postby Tirian » Thu Nov 26, 2009 1:29 pm UTC

Oort wrote:A little off-topic here, but do mathematicians try to avoid proof by contradiction? I imagined they were popular...


They are, like candy. And, like candy, they're not as good for you as vegetables.

skeptical scientist raises a good point that constructive proofs are better than non-constructive proofs, but there is more to it than that, I think. If you have a direct proof that is 100 statements long, then every one of those 100 statements is true. Maybe some of those statements are lemmas that can branch off your knowledge of the field into new areas. But if you have a proof by contradiction that is 100 statements long where the first statement is "Assume x" and statement 99 is "Oops, we just reached a contradiction", then you have 99 statements of fantasy that only exist in an inconsistent mathematical model.

Don't get me wrong, that's fine if you actually needed the power of contradiction to make your case. For instance, the proof of the four color theorem (AFAIK) assumes the existence of a graph with a minimum number of vertices that cannot be four-colored and then finds all sorts of interesting properties that this graph must have culminating in proving that it also has the property of non-existence. :lol: But if you have an argument that could just as easily be phrased as a direct proof, then that is a more illuminating argument.

User avatar
skeptical scientist
closed-minded spiritualist
Posts: 6142
Joined: Tue Nov 28, 2006 6:09 am UTC
Location: San Francisco

Re: Some points on mathematical logic and "rigor"

Postby skeptical scientist » Thu Nov 26, 2009 1:40 pm UTC

Talith wrote:I would say that if a proof gives you more information than another proof then it's a proof of a more detailed theorem rather than it just being a 'better proof' of the original theorem.

You say "potato," I say "potahto."
I'm looking forward to the day when the SNES emulator on my computer works by emulating the elementary particles in an actual, physical box with Nintendo stamped on the side.

"With math, all things are possible." —Rebecca Watson

AhIB
Posts: 18
Joined: Thu Nov 26, 2009 3:05 am UTC

Re: Some points on mathematical logic and "rigor"

Postby AhIB » Thu Nov 26, 2009 2:06 pm UTC

There are two variables a , b and one predicate P , so the real reduction rule is :
for all (a,b)(P(ab,n) --> P(a,n) v P(b,n))
or in Fermat's speaking :
for all (a,b)(P(a^n*b^n) --> P(a^n) v P(b^n))

I don't see any connection with :
**
For example, in your claimed "proof" of the reduction rule, you claim that
for all ( x)[A(x) ---> (B(x) v notB(x))]
is equivalent to
for all ( x)[A(x) ---> B(x)] v for all ( x)[A(x) ---> notB(x)]
which is very much not the case.
**
Ahmed Idrissi Bouyahyaoui

User avatar
gmalivuk
GNU Terry Pratchett
Posts: 26836
Joined: Wed Feb 28, 2007 6:02 pm UTC
Location: Here and There
Contact:

Re: Some points on mathematical logic and "rigor"

Postby gmalivuk » Thu Nov 26, 2009 3:42 pm UTC

No, you really really didn't prove Fermat's Last Theorem. And this wasn't the thread to post about that in anyway.
Unless stated otherwise, I do not care whether a statement, by itself, constitutes a persuasive political argument. I care whether it's true.
---
If this post has math that doesn't work for you, use TeX the World for Firefox or Chrome

(he/him/his)


Return to “Mathematics”

Who is online

Users browsing this forum: No registered users and 17 guests