There is another goal in addition to minimizing the number/complexity of axioms. Some "axioms" like induction actually introduce an infinite family of assumptions, a so-called schema. So in addition to working backwards from our (incomplete) knowledge, we find certain axioms let us make arguments that are obviously valid but would be formally very tedious without them.
Axioms are also introduced in practical terms just to make proofs and results "better". Usually we talk in terms of what propositions are provable, saying that indicates the strength/power of these assumptions, but beyond this there are issues of proof length and complexity.
For example in arithmetic without induction, roughly, theorems remain the same (those which can still be expressed) but may have exponentially longer proofs because of the loss of those `∀n P(n)`-type propositions.
In this sense it does sometimes come back to intuition. If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition and doesn't really change "the game" we are trying to play. It just makes it more intuitive and playable.
I’m not sure what you mean by “theorems remain the same”. If you take away induction from Peano arithmetic, you get Robinson arithmetic, which has many more models, including (from https://math.stackexchange.com/a/4076545):
- ℕ ∪ {∞}
- Cardinal arithmetic
- ℤ[x]⁺
Obviously, not all theorems that are true for the natural numbers are true for cardinals, so it seems misleading to say that theorems remain the same. I also believe that the addition of induction increases the consistency strength of the theory, so it’s not “just” a matter of expressing the theorems in a different way.
I would agree more for axioms that don’t affect consistency strength, like foundation or choice (over the rest of the ZF axioms).
If I had to write again I might say "same theorems about natural numbers" and capitalize ROUGHLY. It is a conversation, what exactly I am weaseling around (not just nonstandard model theoretic issues), and I take your caveat about consistency strength - with that said would you still call it misleading? Why is it that eg x+y=y+x for x y given takes exponential length proof in Robinson compared to PA? For the reason stated, which is true in a very broad sense.
> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition
But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.
I think the crux of the matter is that we accept inductive arguments as valid, and so we formalize it via the inductive axiom (of Peano arithmetic). i.e., we accept induction as a principle of mathematical reasoning, but we can't derive it from something else so we postualte it when we come around to doing formalizations. Maybe that's what you mean by it coming down to intuition, now that I reread it...
Poincaré has a nice discussion of induction in "On the nature of mathematical reasoning", reprinted in Benacerraf & Putnam Philosophy of Mathematics, where he explicates it as an infinite sequence of modus ponens steps, but irreducible to any more basic logical rule like the principle of (non-)contradiction
>> If for all n we can prove P(n), then `∀n P(n)` should be an acceptable proposition
> But how can you prove that P(n) for all n without induction?
Just to be clear to all readers, the axiom of COUNTABLE choice is uncontroversial. Nobody is disturbed by induction.
The issue it that when you allow UNCOUNTABLE choice - choices being made for all real numbers (in a non-algorithmic way, I believe - so not a simple formula) - there are some unpleasant consequences.
> But how can you prove that P(n) for all n without induction? Maybe I misinterpret what you're saying, or I'm naive about something in formal languages, but if we can prove P(n) for all n. then `∀n P(n)` just looks like a trivial transcription of the conclusion into different symbols.
Of course it is likely that an interesting result about all positive integers, that is "really" about positive integers, is proved by induction, but you certainly don't need induction to prove P(n): n = 1.n, or, more boringly, P(n): 0 = 0. (These statements are obviously un-interesting, both in the human sense of the word and in the sense that they are just statements about semi-rings, of which the non-negative integers are an example.)
My understanding is that the difference between "For every positive integer n, I can prove P(n)" and "I can prove ∀n.P(n)" is that the former only guarantees that we can come up with some terrible ad hoc proof for P(1), some different terrible ad hoc proof for P(2), and so on. How could I be sure I have all these infinitely many different terrible ad hoc proofs without induction? I dunno, but that's all that the first statement guarantees. Whereas the second statement, in the context of computability, guarantees that there is some computable function that takes a positive integer n and produces a proof of P(n); that is, there is some sort of guaranteed uniformity to the proofs.
I think it may be easier to picture if connected with math_comment_21's analogy in https://news.ycombinator.com/item?id=44269153: the analogous statements in the category of topological spaces (I think one actually has to work about topos, but I don't know enough about topos theory to speak in that language) about a map f : X \to Y are "every element of Y has a pre-image under f in X" versus "I can continuously select, for each element of Y, a pre-image of it under f in X", i.e., "there is a continuous pre-inverse g : Y \to X of f."
Rejecting induction could be quite useful if you want to be very precise about the implications of your constructions wrt. computational complexity. This is of course only a mildly strengthened variant of the usual arguments for constructivism.
It's been longer than that, more than 2 years since Time ran EY's moron piece which put the whole field in disrepute and back on its heels basically. That the community spins out literal murder cults and assassins doesn't help.
What is an important question in the objective sense? Is life, or no because that just matter to life? It seems oxymoronic, "objective question", "objectively important".
I don't follow GP's sort of solipsist (?) take, but would say question of whether big bang took place in a black hole is pointless compared to life/experience and how they arise.
Artificial intelligence is a nourished and well educated population. Plus some Adderall maybe. Those are the key insights which represent the only scientific basis for that term.
The crazy thing is that a well crafted language model is great product. A man should be content to say "my company did something akin to compressing the whole internet behind a single API" and take his just rewards. Why sully that reputation boasting to have invented a singularity that solves every (economically registerable) problem on Earth?
The "fundamental limiter of human progress" is not energy/intelligence lol. No - surprise, it's people. Bear in mind he builds this "gentle singularity" in the great progressive UAE.
When you accept axioms randomly and reject even logical semantics, you wind up working with something like the so-called rado graph of Erdos. Call the first set of assumptions/structure meaningless and choose a new one, also having no grounding in reason - it turns out that would make no difference. "Almost certainly" you wind up with the same structure (the rado graph) in any case.
So you can reject meaning (identifying the axioms with simple labels 1, 2, 3, ...) and truth (interpreting logical relations arbitrarily), but in doing so you ironically restrict mathematics to the study of a single highly constrained system.
I only disagree somewhat though - it is all contingent. We do say something like
IF { group axioms } THEN { group theory }
and introduce even more contingencies in the application of theory. In a real problem domain these assumptions may not hold completely - but to that extent they are false, not having a meaningless truth value. Crucially, we then search for the right set of assumptions, and the conviction of modern science that there is a right set of assumptions is "effective" at least.
In the previous century there was an attempt to identify mathematics with formalism, but it defeated itself. We need to see truth in these systems - not individual axioms per se, but in systems composed from them. This is justified by the body of mathematics itself, to the non-formalist, the richness of which (by and large) comes from discoveries predating that movement.
I am accepting and rejecting axioms _arbitrarily_ depending on application, but not _randomly_, and definitely not i.i.d. random.
The Rado graph you mentioned does look very interesting as a mathematical object in its own right! But it has approximately nothing to do with what we discussed, exactly because it requires i.i.d. randomness.
> Crucially, we then search for the right set of assumptions, and the conviction of modern science that there is a right set of assumptions is "effective" at least.
Well, multiple sets of assumptions can be 'right' or right enough, or perhaps no set can be. Eg as far as we can tell, no clever sets of axioms will allow us to predict chaotic motion, or predict whether a member of a sufficiently complicated class of computer programs will halt. (However, we can still be clever in other ways, and change the type of questions we are asking, and eg look for the statistical behaviour of ensembles of trajectories etc.)
> In the previous century there was an attempt to identify mathematics with formalism, but it defeated itself.
I say it was extraordinarily successful! It actually managed to answer many of the questions it set out at the start. Of course, many of them were answered in the negative. But just because we can now proof that every formalism has its limits, doesn't mean that informal methods are automatically limitless. Or that there is any metaphysical 'truth'.
The 20th century saw enormous progress in terms of thinking about formalism abstractly (that's the 'self-defeat' you mention, thanks to giants like Gödel and Turing). But it's only in the last few years that we've seen progress in terms of actually formalising big chunks of math that people actually care about outside of the novelty of formalisation itself.
Btw, just to be clear: IMHO formalisation is just one of the tools that mathematicians have in their arsenal. I don't think it's somehow fundamental, especially not in practice.
Often when you develop a new field of mathematics, you investigate lots of interesting and connected problems; and only once you have a good feel for the lay of the land, do you then look for elegant theoretical foundations and definitions and axioms.
Formalisation typically comes last, not first.
You try and pick the formal structure that allows you to make the kind of conclusions you already have in mind and have investigated informally. If the sensible axioms you picked clash with a theorem you have already established, it's just as likely that you rework your axiom as that you rework your proof or theorem.
That bidirectional approach is sometimes a bit hard to see, because textbooks are usually written to start from the axioms and definitions. They present a sanitised view.
Rado has many interesting subgraphs, for example the implication graph of every countable theory. Are arithmetic propositions associated randomly? Not as we see it, but in some sense they could be (even iid). It is not the quite the same but I take the rado construction to be the logical extreme of the position there is no inherent/meaningful truth in such theories. You need to deal with this kind of many-worlds absurdity that falls out.
From your reply though I feel we are not really disagreeing so much. There is a kind of truth which is not propositional or self-evident but teleological. That is a sense in which I think the assigned truth values are meaningful.
The formalist movement was indispensable, I shouldn't have implied it was merely self-defeating. But I believe the philosophy that mathematics is fundamentally arbitrary mechanical symbol manipulation is wrong.
The generic unit of information is still the "bit", and the word "word" -- which is not a unit of information, depending on entropy of the encoding -- is still standard terminology in communication theory.
Would an alien encountering human language say "whatever it is not fundamentally different from the fact they shed skin cells in each other's space"?
> The research, published in Royal Society Open Science, found that these spikes often clustered into trains of activity, resembling vocabularies of up to 50 words, and that the distribution of these “fungal word lengths” closely matched those of human languages.
I'll be the one to admit I am surprised by this (if true), even with the understanding that any motion or byproduct whatsoever might be communicative.
The thought that an organism is totally isolated from its environment, itself and other organisms is absurd, sure - but no one said that!
