What the Tortoise Said to Achilles (1895)
ditext.com
ditext.com
Particularly this quote:
The Wittgensteinian philosopher Peter Winch discussed the paradox in The Idea of a Social Science and its Relation to Philosophy (1958), where he argued that the paradox showed that "the actual process of drawing an inference, which is after all at the heart of logic, is something which cannot be represented as a logical formula ... Learning to infer is not just a matter of being taught about explicit logical relations between propositions; it is learning to do something" (p. 57). Winch goes on to suggest that the moral of the dialogue is a particular case of a general lesson, to the effect that the proper application of rules governing a form of human activity cannot itself be summed up with a set of further rules, and so that "a form of human activity can never be summed up in a set of explicit precepts" (p. 53).
I had searched 'What the Tortoise Said to Achilles' on Google, and ended up reading about the arrow paradox's rebuttals, which were really interesting.
But more to the point of the original article, it shows that there are definitely gray areas within morality, and it's impossible to use boolean logic to try to categorize humans.
So, instead of proof, I have to fall back on intuition and working code, with their severe limitations.
However... studying mathematical proof has at times informed and grown my intuition, by revealing new ways to see a problem and new (bizarre and unintuitive) ways to decompose it.
I might have been better off never having seen this story.
That's too bad, because the anecdote doesn't challenge the basis for mathematical proofs or logical reasoning, in fact it requires it as a precondition for the anecdote to move forward. Remember that Gödel's incompleteness theorems don't argue that there are no true statements, only that some of them cannot be proven true.
> So, instead of proof, I have to fall back on intuition ...
You might be better off reviewing the structure of logic and mathematical proof. Start here:
http://en.wikipedia.org/wiki/Euclid's_theorem
My reasoning is that, if there's one proof sufficiently transparent to win acceptance from a skeptic of logic, then there might be two ... ad infinitum.
Though I still don't feel fully convinced by it; I don't fully see it. It's entirely possible my obstacle is not so much my skepticism as my stupidity :-)
There seem to be 2 parts to the proof. If you have a list of primes:
You can generate another number from that list
You can always get a prime from that number to add to the list
As for 'stupidity', I wouldn't worry about it. The only people I've ever had call me a moron or question my intelligence in any way have always been people who were less intelligent than I am. And that's not because I'm a genius ;-)
But I'm seeing more: start with some primes. They needn't be consective or ordered, just some primes. Any old primes will do. eg 2 and 5 are OK (skipping 3).
Now multiply them all to get p. Obviously, p is divisible by all the primes we started with, because we just created it by multiplying them. eg 2 * 5 = 10
Note that p will generally be quite a bit bigger than the primes. Typically, you'll have the primes bunched up near the left of the number line, perhaps with some primes skipped between them, then a big gap to p, and continuing to infinity on the right.
Now we add one to p. This is just to the right of p on the number line. This p+1 is either prime or it isn't.
1. If it's prime, then there is a prime other than the ones we started with. eg 10 + 1 = 11
2. If it's not prime, it has divisors. This proof claims it must include divisors that are prime but are not among those we started with. <-- THIS IS THE BIT I DON'T GET
You can keep doing this, including that new prime (ie either p+1 itself or a prime divisor of it), showing there are infinitely many primes.
So, yes, it's the second part.
So this means: it has a divisor not in the initial primes (actually, I think it must have two). But why should it be prime?
I think a given divisor does not need to be prime; but it must not be divisible by an initial prime. I guess this means that either it itself is prime, or it has divisors which in turn are either prime or have divisors etc. None of these divisors are an initial prime, because then they would also be divisors of p+1, which we have established they are not.
So I guess that's the proof... but I don't feel sure of it. There are too many steps, and I'm not 100% sure of them, and can't see the whole. Perhaps I've not covered some possibility in some step - how could I be sure I've covered them all? Maybe as it becomes more familiar, I will come to see it.
To prove this for yourself, try assembling a composite number out of non-prime factors. Then, to make sure of your result, decompose your factors into the primes from which they were composed. Finally, restate your factorization by replacing your factors with the primes that compose them.
Example: the composite number 32 is normally factored as 2^5, i.e. four multiplications of the prime number 2. Let's say I want to falsify the idea that all positive integers are either prime or uniquely composed of primes, so I instead compose 32 using the nonprime factors 8 and 4.
Then I factor 8 and 4, and discover that their prime factors are also factors of 32 --
8 = 2^3
4 = 2^2
32 = 2^5
-- so I have proven the original thesis: all positive integers are either themselves prime or are uniquely composed of primes.
The idea I am trying to convey is that the original claim doesn't mean one cannot assemble a composite out of non-primes, only that the composite number is also representable by a unique prime factorization.
More depth here: http://en.wikipedia.org/wiki/Prime_factor
Ok, this is the heart of the issue. If the new number is a prime, all is well and good, but if the number isn't prime, why should it's divisors be?
The simple answer is: they don't have to be. If you have divisors that aren't prime, then keep dividing till you hit some that are. The definition of a prime number is one that can only be divided by itself, so for any non-prime number, you must be able to keep finding factors until they're all prime!
Let's take an example. Our list of primes is {5,7} which are nice small numbers to use. By following the rule of "multiply and add 1" we get:
5 * 7 + 1 = 36.
36 = 2 * 18
36 = 2 * 2 * 9
36 = 2 * 2 * 3 * 3
And you see (I hope) that none of these numbers could possibly be on our original list, because all the numbers already on that list give a remainder of "1" when we divide "36". Yet we must, inevitably, hit a prime number because we just keep dividing till we do!
I can't tell whether you're taking this position or ridiculing it, but if 2 isn't accepted as a prime number, this would falsify the Fundamental Theorem of Arithmetic for all even numbers.
http://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmet...
Quote: "In number theory, the fundamental theorem of arithmetic, also called the unique factorization theorem or the unique-prime-factorization theorem, states that every integer greater than 1[3] either is prime itself or is the product of prime numbers ..."
If your purpose was satire, then perhaps this post will inform other readers who may not detect your satirical intent.
The other primes do, in fact, quite like 2, and 9 is not in any way primier than 2 despite my previous assertion.
EDIT: Actually, there was a real point to ignoring 2, and it was just so I could carry on breaking down the factors as that seemed to be the bit that hyp0 was having trouble with. Perhaps it did confuse more than enlighten. I'm not sure.
In short, do you feel comfortable with the proof now?
> [...] divisors which in turn are either prime or have divisors etc. None of these divisors are an initial prime, because then they would also be divisors of p+1
Let me put it this way: I think I'd score 100% on an exam on this, but I don't "get" it.
The divisors of 18 are also divisors of 36, because 36 = 18 * 2. Could use a theorem here, that a divisor of a divisor (of x) is also a divisor (of x).
A way to put it: p+1 can't be divided by any initial primes; and, if we keep dividing divisors, we eventually can't divide any more, and that's the definition of prime (indivisible "atoms"!).
I like seeing the overall process as: each time you find a new prime, it could fill in a gap between primes in the list, or be greater than any of them. Or, be smaller than any of them:
3*5 +1 = 16 -> 2
\tangent
In contrast, the purpose of a proof is to convince me that it's true. Sure, if I accept the theorems, and I accept the proof given those theorems, then I accept the proof. But this means that in order to be convinced that the proof is true, I have to be convinced of all the levels.
The difference isn't code vs proof in themselves, but in their purpose. I demand a lot more of a proof!
\idea
You "run" the proof to check it; you can "step into" theorems (like a debugger or some theorem websites which hyperlink them), or collapse/hide them.
It would be set-based, and so fundamental in that sense. I'm not sure if it would actually create sets and operate like an algorithm on them; or if it would use theorems about sets. I think the latter is necessary for "proof", but it wouldn't be as convincing... Generating examples would be helpful, to show it "working". hmmm... some proofs work kind of "by example", but with variables. What makes it a "proof" is that it works for the full range of values needed. So emphasising that approach might help.
The language would enable you to divide up an issue into possibilities in various ways, and automatically check that each limb is addressed (this is the basis of proof to my mind: you divide up the issue, and show that this covers all possibilities; then handle each limb. e.g. the predicate "is prime" or not). You can nest divisions. Not far from pattern matching, as in ML/haskell.
The actual proof part would be chains of implies: given x, y is true. These can be theorems/libraries: in the stdlib, or a third-party library, or your own "app" (or, the language's built-in axioms and theorems). So you can't just magically go from one step to the next; you have to specify a theorem for that step (call it). Perhaps the most basic ones would be implicit (like implicit casts), to avoid too much tedium. You can then "step into" these calls, or collapse them. Actually, just defining a new theorem is a way to collapse it (debugger "step into", collapsable tree and hyperlinks are just UI choices - vim ^] is another way to navigate calls, conceptually expanding/collapsing).
A key convention here would be that it's not enough to be correct if it's a complex, confusing, tedious "spaghetti proof". You want clear proofs, that ideally formalize intuitive notions. You build libraries that might not be the most concise, but that give you theorems that "make sense" and are useful for building convincing proofs. Libraries can compete etc for the "best" formalisms.
That is: unlike mathematicians, we don't aim at brevity or elegance, but at being convincing, intuitive, easy to understand. Accessible to ordinary people - pop-proofs, like pop-science, pop-psychology, pop-art etc. And I wouldn't be doing this magnanimously, for the poor ignorant masses, but because I need it myself!
It wouldn't be doing anything very clever, just easing the cognitive burden of complex proofs:
record the detail (just document management alone is helpful); hide/reveal one part at a time; automatic checks; affordances whose existance guides you to sensible operations (e.g. divide it up; implies; implicit theorems). There's also the fundamental aid of helping you formally defining the problem in the first place... which can be hardest part of proving it.
\implementation
In a way this is bad, because you're having to explicitly type so much... in a regular program, you just call a function, and you don't need to show the returned result - it's hidden in the execution. We could do that here, but it would be less clear:
This unclear version would look like: a starting expression, then a sequence of transformation theorems/calls (specifying exactly how they're applied). You'd run it to see the sequence of expressions as it was transformed.
A problem is we'd have to specify tediously what we want. For example, given expression a and b and operator ->, it couldn't know whether we want a (or b) - or something else, because many things are implied. So the operations would to be very precise. Like, extract the first operand; extract the second operand. It's similar for trivial operations like commut/associate a and b and c - we must specify precisely which ones to permute. I guess we could have a "permute" rule that operates at a higher level (i.e. actually a theorem...); or even have an "operator" that specifies the operation via the result... so it's no longer really an operator, but a kind of declarative system that I first mentioned.
One option is some "live" editing environment, so we can get the result of the call automatically. A couple of problems: we might not want the literal result, but an implicitly transformed version (e.g. trivially, like re-ordered terms). We'd also have to specify exactly how the theorem was applied - this might be a problem anyway (if it's to be automated).
I'm thinking that the engine works out how to apply the theorem to transform the starting expression into the resulting expression... but that might be too hard; we may need to tell it exactly how to apply it (like positional arguments to a function).
But... I guess it might even be a good rule of thumb, that if we can't mechanically work out what the step is, it's too complex! And if the user really wants it as a single step, they can write a theorem, that breaks it down enough into smaller steps simple enough for the compiler to understand. That seems to serve our goal, of convincing... at least, in principle. It might be tedious in practice.
For implict theorems, it seems commutativity/associativity would be OK; maybe distributivity - but if a big change, might be hard to follow.
Inference: We might allow any theorem to be implicit, provided the engine can infer not just how to apply the theorem, but what the theorem actually is (i.e. find some way to justify the step). This is quickly heading towards an automatic theorem prover, at least for very simple proofs. A problem with this is that the step might be less clear - that is, although the engine can work it out, the user might not be able to. This could easily happen in practice, even if the engine isn't very clever, by it having a library of very advanced theorems that the user doesn't even know about (this might be partially mitigated in an active environment, where the engine suggests the theorem - like a tooltip, google suggest, autocompletion).
Two kinds of transform, equational (an equal expression) and implies (not equal, but some aspect of it e.g. a and b -> a)
The easy answer is for the user to only allow libraries that they've accepted.
I was thinking we might have an automatic check, that we never use a theorem which is stronger than the whole thing we're trying to prove - that is, which implies our whole proof). But that seems hard to check automatically (maybe undecidable in general).
But that's how prime is defined -- indivisible by any other numbers except 1. If you statement is true -- that a given number "must not be divisible by an initial prime", that means the number is itself prime.
Positive integers fall into precisely two categories:
1. Not divisible by any smaller numbers except 1.
2. Divisible by one or more smaller numbers.
Those in category (1) are prime. Those in category (2) are composite. There is no third possibility.
> I think a given divisor does not need to be prime; but it must not be divisible by an initial prime.
I will disprove by counter-example that not being divisible by an initial prime implies it is prime:
initial primes: 5 and 7
p = 5 * 7 = 35
p+1 = 36
This step of the proof invokes the Fundamental Theorem of Arithmetic [0]: the statement that every natural number can be expressed as a unique product of primes (uniqueness isn't the important bit here, just the fact that such a factorization exists).
So you need to accept the Fundamental Theorem of Arithmetic as true before you can fully understand this proof.
[0] http://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmet...
In order to be able to understand and appreciate mathematical proofs, you have to develop the ability to accept the truthness of a result - and to realize the consequences of it being true - even though you do not yet understand why it is true. You have to learn to accept the ensuing confusion as a natural state of mind (read [0] if this idea intrigues you).
[0] http://j2kun.svbtle.com/mathematicians-are-chronically-lost-...
I have to disagree. A trained mathematician understands why a proof is or it not valid, based on a combination of axioms and a logical sequence predicated on axioms, but with no gaps or overlooked assumptions.
Without knowing and explaining why, it would not be possible to write a proof that would pass muster with other mathematicians, people who by instinct and training refuse to accept fuzzy explanations.
This is why Gödel's Incompleteness Theorems came as such a shock, at a time when many people expected to be able to systematize all of mathematics and predicate it on a handful of unassailable logical principles (as Russell and Whitehead attempted to do in the early 20th century).
The Incompleteness Theorems show the degree to which mathematicians expect to know why something is true, and if they cannot, why not.
First off, to dispel any misunderstanding, I was talking about the process of becoming a mathematician, which you necessarily go through before you can call yourself one.
But even for full-fledged mathematicians, what I'm saying is true to an extent. For instance, although ZFC set theory is usually accepted as the basis for all mathematics, most mathematicians (precisely: those who do not study formal logics or other areas of metamathematics) do not state their results in terms of set theory, but instead write informal proofs that appeal to other established results in their field of study.
That is absolutely not the same as saying that their thinking is fuzzy or sloppy. The fact that I personally do not state (or, even, understand) all the details behind an established theorem X has no bearing on the validity of my proof for a theorem Y that hinges on X being true.
> The Incompleteness Theorems show the degree to which mathematicians expect to know why something is true, and if they cannot, why not.
This is a separate matter. Whether in theory it is possible for you to ascertain whether X is true or not, and whether you fully understand (down to first principles) why X is true before you use it as a stepping stone for other results are different issues.
>"Euclid is often erroneously reported to have proved this result by contradiction"
It simply says that if you are constructing a list of primes, you can always add one more to the list, therefore there are infinitely many.
But the impression I get from my (possibly biased) sample is that most non-trained people intuitively see proof by contradiction (or any form of nonconstructive proof, really) as a way of "cheating", because it asserts something does or does not exist without actually producing a (counter)example. YMMV, of course.
You can still do all the math you could do before -- and if Carroll or GEB gets you more interested in the fundamentals of math, you can do even more.
Yes, you have to accept some basis of mathematics, and you now understand that some true things will be unprovable in the basis you just accepted. But that doesn't stop you from proving things.
I think you might have just transferred your optimism about math to code instead. How do you know your programming language is doing what you asked it to? That you asked it to do the right thing at all? That the compiled code has the correct behavior? That your hardware works as advertised and is not failing at the moment? In both code and math, you have to accept some abstractions that you're not going to worry about, but the things you do with math are certainly more verifiable.
To add to your point, if someone begins to doubt the utility of mathematical logic and responds by refocusing his attention from logic to code, he's somehow overlooking the fact that code is built on a foundation of mathematical logic.
My "optimism" is more for my intuition; working code is experimental confirmation.
It's easier to be optimistic about code than proofs. Firstly, working code only needs to work in the specific cases you're using (that you test for); but a proof must work in every possible case. Thus, working code is simpler and easier to check, because it's aiming at less. My code almost always confirms my intuition.
Yes, it's also helpful to have the automatic, mechanical check of executable code; and as you say, this relies on compilers, OSes, silicon, hardware. (Though, anecdotally, I have noticed subtle problems that I eventually diagnosed and confirmed to be compiler and hardware bugs.) BTW, yes I have tried COQ (proof assistant; somewhat mechanical proof checking), but simple ideas become very complex to prove, and the problem of bugs in COQ itself etc is of greater concern, for the next reason:
Secondly, and relatedly, is that the standard is much lower for code. It just needs to work. Whereas a mathematical proof is supposed to be absolutely true. In other words, I don't ask as much from code. If there turns out to be a bug, it's just learning more about the problem; about the world. It's an engineering flaw. But if my proof is wrong, the game is lost.
An argument against my intuition is probably more telling. Though my faith in it has turned out to be justified many many times, I certainly can be wrong. My only real excuse is that, as a human being, I have nothing else to fall back on but my sense of reality and reason. That's my hardware; if it's wrong, I really am lost. So I might as well trust it. Fortunately, it's almost always right; probably because I try to see things from many angles and check them in many ways before my intutive sense is fully formed.
I'm not sure I understand why. If the tortoise had insisted that one plus one is three, would it have destroyed your ability to accept arithmetic?
I'm not sure what Carroll intended by this piece, but what I take from it is that there's no sense arguing with irrational people. One can certainly claim to accept A, and accept if-A-then-B, but deny B; one can also claim that up is down and the sky is candy-striped.