The Horgan Surface and the Death of Proof
blogs.scientificamerican.com
blogs.scientificamerican.com
Even not that hard math proofs call on intuition pretty quickly, and I think it’s a legit question to ask when does it basically become empirical proof.
To my understanding maths has a common basis in set theory but set theory itself is just a common basis for maths (ie as opposed to “the truth”), but even so proofs are typically not given via set theory especially if the theorem is complicated.
The idea is that mechanising proof and making it more algorithmic will make it more like what the layman thought proof is , but it at the same time raises the question, what is this all for? Ie maths is what mathematicians do. I think it admits to no clearer a definition. So it’d probably make sense for mathematicians to decide, what precisely is the role of proof?
The author talks about this in addressing computer aided maths and the general recruitment of applied mathematicians to solve problems whilst caring less to advance “the science” whilst doing it. Chomsky spoke a lot about this in criticising the use of probabilistic models in science as ultimately scarcely contributing to causal understanding, which in itself is separate from being able to predict phenomena well. Ie you can do practical things without ever knowing what’s going on under the hood, but science wants to know what’s going on under the hood and so prefers different approaches to its advancement.
Can you give an example? Nothing jumps to mind from my years of studying mathematics.
Of course you could (in this example) prove it deductively since Peterson graphs have a specific size , or inductively otherwise but you’d first need to establish a framework... and not a “intuitive framework” at that. Well, all you’ve got then is something axiomatic in which case we arrive back at “intuition” for you axioms.
Here’s a whole line of argument about a large part of the proof we know:
https://en.wikipedia.org/wiki/Petersen_graph#Hamiltonian_pat...
I'm not sure what you mean by "intuition". Do you doubt that this proof has a straightforward translation into formal language?
I hadn’t seen the Wikipedia article you point out but Peterson graphs will be in many graph theory textbooks.
Again have a look at the article on constructionist proof for another angle on maths and intuition.
The plural here is confusing. Are you talking about the Petersen graph, on ten vertices? There does exist a constructivist proof of its non-Hamiltonicity: merely enumerate every cycle of length ten and show that none are Hamiltonian.
There is a class of objects called generalised Petersen graphs but these are usually Hamiltonian: https://core.ac.uk/download/pdf/82084439.pdf
Is the claim that the opposite of "formal" is "intuitive"? That's news to me!
I’d start like this : if you’re explaining something in English then you’re invoking and reliant on the readers common sense and intuition to do the work in your explanation. E.g a pipe is used to smoke tobacco. Pipe. Usage. Smoking. Tobacco. It’s left to the reader to define, disambiguate and on that basis accept. Contrast to: a pipe is used for transporting water.
A: I'll be pedantic and take it in baby steps:
Given: area = height * width
Given: area(c, d) = area(a, b)
c * d = a * b Because equivalencies of
equivalents are equivalent
(c * d) * x = (a * b) * x Equivalencies multiplied
by the same thing are
equivalent
A: Just bear with me...
x = 1 / d Because I say so
(c * d) * (1 / d) = (a * b) * (1 / d) Substitution again
... Blah blah blah
c = (a * b) / d Tadah!
A: (Chuckle) Division by zero isn't defined.
Q: Why not?
A: Well, we want division to be defined as the inverse of multiplication.
Q: Inverse?
A: If x * y = z, and we know x and z, what is y? x * y = z => z / x = y.
Q: So why can't we divide by zero?
A: Because if x is zero then y could be anything. It's not so much that division by zero is evil as it is that multiplying by zero does not have a unique inverse, and disallowing multiplication by zero would be just too weird.
Q: Why don't we just say that y has a whole slew of possible values?
A: Because we don't. Look, this is simple arithmetic, not some weird group thing. You wanted one equivalent rectangle and I gave it to you. If d is zero there's no c that could be big enough to equal a * b. (Before you ask, "infinity" is not a number.) Well, I suppose you could pick a number if...
Q: ... a or b is zero. I have no idea if a or b or d will be zero. Can I still use "c = a * b / d?"
A: Don't you have to wash the car or something?
[edit: consistent use of "c" and "d"]
You can avoid chuckling by pointing out that this is a nonsense question. A rectangle which has a height of zero isn't a rectangle at all - it's a line. And lines don't have areas.
(You can continue chuckling after someone asks why lines have no area, I guess.)
> Q: Wait, where did "x" come from?
A proof from intuition is not the same as a formal proof with an insightful step. I wager that many formal proofs (in Coq, say) would spur such "Wait, what is that for?" questions.
In this case, the selection of some arbitrary non-zero real "x" is a creative step, not an intuitive one. The missing proviso that "x" is non-zero is an oversight, but it's a "small error", and -- with some experiential intuition -- can be recovered.
(EDIT: The arbitrary variable is quickly overridden with a specific definition, but this is not typical unless there's a good reason to conceptualize it this way. If its value is obvious, define it up front and discuss why that value is the correct one.)
> What if "d" is zero?
This is (very nearly) a refutation, in the sense of Lakatos. We reflect and decide that our basic proof idea works for rectangles of positive area, and in some sense zero-area rectangles aren't really the objects we wanted to talk about. So we include this as an assumption.
The digression about division by zero, inverses, etc. is valuable, but missing the point that this is an algebraic representation of a geometric problem. There's a lot that could be said about whether geometry is intuitive or formal, but I think the issue of divisibility by zero is side-stepping most of the interesting stuff.
...anyway, this is quite a convoluted proof. We assume a priori that for any rectangle R, its "area" A(R) is well-defined and computable. We'll assume that the rectangles are axis-aligned with side-lengths R.x and R.y for each axis. We could have a separate discussion and proof about the invariance of area under a change of basis.
Theorem: Given a rectangle R with non-zero side-lengths R.x and R.y, and given a non-zero real number c, there exists a rectangle R2 with non-zero side-lengths where R2.x = c and A(R) = A(R2).
Proof: Because R2.x is already specified, we need only determine R2.y. We know that, for rectangles, A(R) = R.x * R.y. So we desire that R.x * R.y = R2.x * R2.y. Because R2.x = c and c is non-zero, we have the equivalent desire that (R.x * R.y) / c = R2.y. Thus, the rectangle where R2.x = c and R2.y = (R.x * R.y) / c will have the same area as R and will have the desired side-length c. []
English? Yes. But it has more similarity with legalese than informal English. Each clause makes direct appeal to some rule of logic, and it could be transformed into a Coq proof (or any other proof assistant) without much ceremony.
Agreed :)
> Theorem: Given a rectangle R with non-zero side-lengths...
And this is the key problem with the "proof" I laid out. My theorem does not specify non-zero dimensions. Therefore standard arithmetic division by a dimension is not well-defined. Since we're pondering intuition, it's interesting to consider how fixing the "proof" was approached. On the one hand, you fixed it by in effect back-progating invariants to the problem definition. Another approach would be to use a modified definition of "division" ("d = 0 if a or b are zero"--would still require the constraint "c !=0 unless a*b=0").
Mathematically, the former appoach is almost always what you're going to want, since a modified definition will be pretty useless to build upon consistently. From an application standpoint, the latter would be much more robust.
This is kind of one of the points made in the Sci Am article--pure vs. applied proofs are different.
The intuition behind this choice is, if we’re squishing the rectangle so hard that one side approaches 0 length, the constant area has to go somewhere. If the other side length approaches infinity, why not literally let its measure be infinity? One would argue that the real numbers are too impoverished to give a satisfactorily general answer to our original question.
Of course, we still obtain a zero area, so we’re no longer really solving the same problem as we started with. If we want a zero side length and a non-zero area, we may need to move into non-Euclidean geometries. It really depends on what we’re doing.
My point is that when an application needs to make changes to the foundation, usually there’s going to be a richer pure setting we can move to. And if there isn’t yet, that’s a great opportunity to find out how robust of a new foundation we can create.
Hiding edge cases away in an otherwise unobtrusive definition bothers me as both a mathematician and as a software developer. In all cases, I want to highlight the assumptions we’re making and find the right abstraction to tame them.
Mathematicians need to be convinced that in principle a proposition could be stripped down to axioms and syllogisms. It turns out that it's quite hard to do that stripping-down in practice.
I don't think it's really the case that all branches of mathematics really have a 'common basis' as much as that they're all equivalent. It's pretty common to map one branch to another, e.g. arithmetic to set theory, but then once that's been done there's no real reason to write proofs in a particular branch in the formalism of another.
> The idea is that mechanising proof and making it more algorithmic will make it more like what the layman thought proof is , but it at the same time raises the question, what is this all for? Ie maths is what mathematicians do. I think it admits to no clearer a definition. So it’d probably make sense for mathematicians to decide, what precisely is the role of proof?
"A New Kind of Science" has some insights about this that I appreciate greatly. Mathematicians don't bother to enumerate everything that's formally ('mechanically') true, even tho there are some interesting truths to be discovered in that fashion. They instead explore the 'tree of truths' based on history, intuition, and even fashion.
Ultimately, even the most mechanical formal systems are, or can be, nebulous and 'philosophically strange'. Consider the axiom of choice as but one example – there are different set theories depending on whether one accepts that axiom as 'reasonable' (or 'true') or not!
A particularly nice example is the Alexander horned sphere. https://en.wikipedia.org/wiki/Alexander_horned_sphere
One nice example of "pathological" behaviour came out of Cantor's study of the continuum [0]: he gave an example of a function that is continuous and has zero derivative almost everywhere (i.e. everywhere except at a set of isolated points), but that manages to increase from 0 to 1.