Peano arithmetic is enough, because Peano arithmetic encodes computation
math.stackexchange.com
math.stackexchange.com
It covers both the limits of what can be proven in the Peano Axioms, and how one would begin bootstrapping Lisp in the Peano Axioms. All of the bad jokes are in the second section.
Corrections and follow-up questions are welcome.
Can we not ruin every technology we develop with ads?
Also is this somewhat not just lining Google's/ad networks pockets? They won't care about even a large-ish number of people using this add on.
The larger adtech companies will have some form of bot-activity-detection, _but_ plenty will let it all just slip on by. (I've personally written a Babashka script at $job that checks performance of our publishers, and flags any fraudulent-seeming activity)
Fewer people went to pay. That’s the crux. Companies wanting mass market penetration, rather than just accept the natural size of the market.
Very reminiscent of the New Math pedagogy of the 1960s. Built up arithmetic entirely from sets. Crashed and burned for various reasons but I always had a soft spot for it. It also served as my introduction to binary arithmetic and topology.
(I am not suggesting that that very specific sequence of events happened in this case. It's just an example of how "I was looking this up for other reasons and then I saw something about it on HN" could genuinely happen more often than by chance, without any need for weird tracking-and-advertising shenanigans.)
https://justine.lol/sectorlisp2/
Also, lots of Lisp from https://t3x.org implement numerals (and the rest of stuff) from cons cells and apply/eval:
'John McCarthy discovered an elegant self-defining way to compute the above steps, more commonly known as the metacircular evaluator. Alan Kay once described this code as the "Maxwell's equations of software". Here are those equations as implemented by SectorLISP:
ASSOC EVAL EVCON APPLY EVLIS PAIRLIS '
Ditto with some Forths.
Back to T3X, he author has Zenlisp where the meta-circular evaluation it's basically how to define eval/apply and how to they ared called between themselves in a recursive way.
When it comes to bootstrapping a programming language from nothing, the two best options are Lisp and Forth. Of the two, I find Lisp easier to understand.
Then every modal logic becomes some mapping of 2^(N) to some set of statements. The only thing that matters is how predictive they are with some sort of objective function/metric/measure but you can always induce an "ultra metric" around notions of cognitive complexity classes i.e. your brain is finite and can compute finite thoughts/second. Thus for all cognition models that compute some meta-logic around some objective F, we can motivate that less complex models are "better". There comes the ultra measure to tie disparate logic systems. So I can take your Peano Axioms and induce a ternary logic (True, False, Maybe) or an indefinite-definite logic (True or something else entirely). I can even induce bayesian logics by doing power sets of T/F. So a 2x2 bayesian inference logic: (True Positive, True Negative, False Positive, False Negative)
Fun stuff!
Edit: The technical tldr that I left out is unification all math imho: algebraic topology + differential geometry + tropical geometry + algebraic analysis. D-modules and Microlocal Calculus from Kashiwara and the Yoneda lemma encode all of epistemology as relational: either between objects or the interaction between objects defined as collision less Planck hyper volumes.
basically encodes the particle-wave duality as discrete-continuum and all of epistemology is Grothendieck topoi + derived categories + functorial spaces between isometry of those dual spaces whether algebras/coalgebra (discrete modality) or homologies/cohomologies (continuous actions)
Edit 2: The thing that ties everything together is Noether's symmetry/conserved quantities which (my own wild ass hunch) are best encoded as "modular forms", arithmetic's final mystery. The continuous symmetry I think makes it easy to think about diffeomorphisms from different topoi by extracting homeomorphisms from gauge invariant symmetries (in the discrete case it's a lattice, but in the continuous we'd have to formalize some notion of liquid or fluid bases? I think Kashiwara's crystal bases has some utility there but this is so beyond my understanding )
There’s probably ten+ years of math education encoded in this single sentence?
Wish me luck!
https://github.com/ikrima/topos.noether/blob/master/discrete...
[EDITED to add:] This is worth noting because today's LLMs really don't seem to understand mathematics very well. (This may be becoming less so with e.g. o3-pro and o4, but I'm pretty sure that document was not written by either of those.) They're not bad at pushing mathematical words around in plausible-looking ways; they can often solve fairly routine mathematical problems, even ones that aren't easy for humans who unlike the LLMs haven't read every bit of mathematical writing produced to date by the human race; but they don't really understand what they're doing, and the nature of the mistakes they make shows that.
(For the avoidance of doubt, I am not making the tired argument that of course LLMs don't understand anything, they're just pattern-matching, something something stochastic parrots something. So far as I can tell it's perfectly possible that better LLMs, or other near-future AI systems that have a lot in common with LLMs or are mostly built out of LLMs, will be as good at mathematics as the best humans are. I'm just pretty sure that they're still some way off.)
(In particular, if you want to say "humans also don't really understand mathematics, they just push words and symbols around, and some have got very good at it", I don't think that's 100% wrong. Cf. the quotation attributed to John von Neumann: "Young man, in mathematics you don't understand things, you just get used to them." I don't think it's 100% right either, and some of the ways in which some humans are good at mathematics -- e.g., geometric intuition, visualization -- match up with things LLMs aren't currently good at. Anyway, I know of no reason why AI systems couldn't be much better at mathematics than the likes of Terry Tao, never mind e.g. me, but they aren't close enough to that yet for "hey, ChatGPT, please evaluate my speculation that we should be unifying continuous and discrete mathematics via topoi in a way that links aleph, beth and Betti numbers and shows how our brains nucleate discrete samples of continuum reality" to produce output that has value for anything other than inspiration.)
I'm not sure there's an argument I'm hearing here other than you seem to have triggered some internal heuristic of "this was written by an LLM" x "It contains math words I don't understand" => "this is bullshit"
which you wouldn't be wrong but I am making a specific constructionist modal logic here using infinity-groupoids from category theory. infinite dimensional categories are a thing and that's what these transfinite numbers represent
you have hyperreal constructionists of the reals as well which follows nonstandard analysis. you can also use the Weil cohomology which IIRC gets us most of calculus without the axiom of choice but someone check me on that.
so....again, not sure what your specific critique is?
(In a different comment I make some actual criticisms of what you wrote. I see you replied to my comment there, and that's a more appropriate place to discuss actual ideas. I don't see much point in criticizing LLM output in a field LLMs are bad at.)
Anyway: (1) no, it wasn't clear. I wouldn't generally take "I nerd-sniped myself. Here's a more fleshed-out sketch of ..." to mean "Here's something written for me by an LLM". I'd take it to imply that the person had done the fleshing-out themself. And (2) no, the problem wasn't that you used words I don't understand. It's certainly possible that your ideas are excellent and I just don't understand them, but I'm a mathematician myself and none of the words scare me.
aaaaaaaah, I think you finally helped me notice something subtle in the way I use LLMs than other people. It sounds obvious now that I think about it but I never considered people use LLMs like google whereas I use it more like a real time thought transcriber (e.g. Dragon Naturally Speaking but not shite :P) Since it's trained on a RAG based off of my own polished thoughts, I've set it up as a meta-circular evaluator to do linguistic filtration (basically Fourier kernels on clip embedding space that map to various measures of "conceptual clarity").
So the LLM-ness of it to me is a clear-flag that this is hastily dictated.
Aleph and beth numbers are related things, in the field of set theory. (Two sequences[1] of infinite cardinal numbers. The alephs are all the infinite cardinals, if the axiom of choice holds. The beth numbers are the specific ones you get by repeatedly taking powersets. They're only all the cardinals if the "generalized continuum hypothesis" holds, a much stronger condition.)
[1] It's not clear that this is quite the right word, but no matter.
Betti numbers are something totally different. (If you have a topological space, you can compute a sequence[2] of numbers called Betti numbers that describe some of its features. (They are the ranks of its homology groups. The usual handwavy thing to say is that they describe how many d-dimensional "holes" the space has, for each d.)
[2] This time in exactly the usual sense.
It's not quite true that there is no connection between these things, because there are connections between any two things in pure mathematics and that's one of its delights. But so far as I can see the only connections are very indirect. (Aleph and beth numbers have to do with set theory. Betti numbers have to do with topology. There is a thing called topos theory that connects set theory and topology in interesting ways. But so far as I know this relationship doesn't produce any particular connection between infinite cardinals and the homology groups of topological spaces.)
I think ikrima's sentence is mathematically-flavoured word salad. (I think "Betti" comes after "beth" mostly because they sound similar.) You could probably take ten years to get familiar with all the individual ideas it alludes to, but having done so you wouldn't understand that sentence because there isn't anything there to understand.
BUT I am not myself a topos theorist, nor an expert in "our human brain's sensory instruments". Maybe there's more "there" there than it looks like to me and I'm just too stupid to understand. My guess would be not, but you doubtless already worked that out.
[EDITED to add:] On reflection, "word salad" is a bit much. E.g., it's reasonable to suggest that our senses are doing something like discrete sampling of a continuous world. (Or something like bandwidth-limited sampling, which is kinda only a Fourier transform away from being discrete.) But I continue to think the details look more like buzzword-slinging than like actual insight, and that "aleph/beth/Betti" thing really rings alarm bells.
Aleph numbers = these are cardinals sizes of infinity; depending on your choice of axioms, ZFC or not, you have the continuum hypothesis of aleph0 = naturals, aleph1= 2^N = Continuum
Beth numbers are transfinite ordinals => they generalize infinitesimals like the 1st, 2nd, 3rd. so you can think of them as a dual or co-algebra (I'm hand waving here, it's been twenty years since real analysis).
Betti numbers are for persistent cohomology; they track holes similar to genus
I mean there's a lot to cover between tropical geometry, differential geometry, and algebraic analysis. So sometimes alarm bells are false alarms and your random internet commenter knows what he's talking about but is admittedly too sloppy but it's 5 pm on a Saturday and I wrote that in the morning while making breakfast eggs, not for submission to the annals of Mathematics!
Thank you for coming to my TED Stand Up Talk.
More math at the GitHub: http://github.com/ikrima/topos.noether
Also, if you're really that uptight, most of this is actually to teach algebraic topology to my autistic nonverbal nephew because I'm gonna gamify it as a magic spell system
So it'll be open source and that begs the question, if you use it to learn something, did that mean I just zero-proof zero-knowledge something out of you that I didn't even need to know by making a self referential statement across both space & time?
peace out my ninja!
It's certainly possible (as I explicitly said before) that my bad-math-alarms have hit a false positive here. You haven't convinced me yet, for what it's worth. (You need not, of course, care whether you convince me or not. It's not as if my opinion is likely to have any effect on you beyond whatever you might feel about it.)
For Beth numbers, the wikipedia article is plenty enough to get you started: https://en.wikipedia.org/wiki/Beth_number
I'm aware I'm being a bit dickish about this, which I regret, but I'm not sure how else to respond to what seem like repeated deliberate attempts to frame this as "ikrima, the expert, kindly condescends to provide some elementary mathematics education to gjm11, the novice" which doesn't appear to me to be an accurate characterization of the situation.
but also, i mean you are just flat out wrong on some very big parts. E.g.: i think in 2024 or 2023, there was a big breakthrough in geometrization of Langlands. IIRC, there was a second big break through on the discrete-continuum connection relating to primes in some manner but can't remember specifics off top of my head.
i think you're confusing maybe what Beth numbers are used for vs. what i'm proposing that they be repurposed for. You're right, no one is using them the way i referenced but that's kind of what math research is...?
I'm not sure how progress on geometric Langlands means I'm "flat out wrong on some very big parts". I certainly didn't say "there has been no progress on the geometric Langlands conjecture recently" or anything like that, nor did I say anything like "there is never any connection between discrete and continuous things in mathematics". (Not least because that's obviously very false.) So I don't understand what it is I've said that you think progress on the geometric Langlands conjecture is a counterargument to.
I understand that you're describing things that (you hope) could be done, rather than things that are already standard practice. But I don't think you've given any actual indication of how beth numbers in particular are going to be relevant. They're a very specific thing, and nothing you've said about them seems to make any contact with what they are in a way that would distinguish them from (say) the alephs or even the ordinals.
What I'm not seeing is any sign that there's more here than (1) a very general idea that could be stated perfectly well without any very advanced mathematics (e.g., "wouldn't it be nice to have a unified theory of how continuous and discrete things relate to one another, and apply it to human perception and cognition?") and (2) a bunch of buzzwords from various fields of advanced mathematics that have some superficial connection to #1, and (3) a handwavy assertion that somehow these things are all deeply connected ... without any actual deeper connection than "these things all sound like they might relate to one another".
What makes all that advanced mathematics worth the effort is its precision and rigour. Maybe all the precision and rigour is actually there and you just haven't chosen to show it to us. Maybe you have a deep enough intuition for these things that we should just trust that the details can be filled in precisely and rigorously. If it were, say, Terry Tao saying these things then I'd be inclined to trust him (though only provisionally; very smart mathematicians do sometimes have grand visions that never work out). Maybe, maybe, maybe. But as yet I haven't seen the evidence. And, whereas very smart mathematicians do sometimes have grand visions that never work out, the grand visions of amateurs unfortunately almost never turn out to have much substance. (Not literally never. Ramanujan was the real deal, for instance. But for every Ramanujan there are thousands of people who are, well, Not Ramanujan.)
Reformulating our entire ontology around relational mechanics is the answer imho. So Carlo Ravoli's RQM is right but I think it doesn't go far enough. Construct a grothendeik topos with a spacetime cohomology around different scales of both space and time with some sort of indefinite conservation and you get collision less Planck hyper volumes that map naturally to particle-wave duality interpretations of QM.
https://github.com/ikrima/topos.noether/blob/aeb55d403213089...
In the "Why Lisp?" section there is a bit of basic logic defined. The first of those functions appears to have unbalanced parentheses.
>(defun not (x) > (if x > false > true)
I have a compulsion that I can't control when someone starts using parentheses. I have to scan to see who does what with who.
You later say in the same section
>But it is really easy to program a computer to look for balanced parentheses
Okay. This is pretty funny. Thanks for the laugh. I realize that you weren't doing that but it still is funny that you pointed out being able to do it.
This later comment in the "Basic Number Theory" section was also funny.
>; After a while, you stop noticing that stack of closing parens.
I really enjoyed reading this post. Great job. Though it has been a long time since I did anything with Lisp I was able to walk through and get the gist again.
Are you saying that parentheses introduce the problem of having to scan to see what goes with what?
As in, if we don't have parentheses, but still have recursive/nested structure, we don't have to scan?
I automatically count and match even today, 40 years later.
And I'm glad that someone liked some of my attempts at humor. As my wife sometimes says, "I know that you were trying to make a joke, because it wasn't funny."
There are two places where you accidentally wrote “omega” instead of “\omega”.
I am away from my computer for the day, but I will fux it later.
I think the problem is that it's already fuxed.
I also find it super weird that Peano axioms are enough to encode computation. Again, this might be trivial if you think about it, but that's one self-referential layer more than I've thought about before.
One question for you btilly - oddly enough, I just recently decided to learn more Set Theory, and actually worked on an Intro to Set Theory textbook up to Goodstein sequences just last week. I'm a bit past that.
Do you have a good recommendation for a second, advanced Set Theory textbook? Also, any recommendation for a textbook that digs into Peano arithmetic? (My mini goal since learning the proof for Goodstein sequences is to work up to understanding the proof that Peano isn't strong enough to prove Goodstein's theorem, though I'll happily take other paths instead if they're strongly recommended.)
I don't have good suggestions for a good set theory textbook. Grad school was 30 years ago, and I didn't specialize in logic.
The best set theory book that I read was https://www.amazon.com/Naive-Theory-Undergraduate-Texts-Math.... But that one is aimed at people who want to go into math but do not wish to specialize in set theory, and not at people who want to actually learn set theory.
ChatGPT tells me that PA+"PA is consistent" is not quite enough. I believe that it has digested enough logic textbooks that I'll believe that claim.
> I think just PA+"PA is consistent" is enough?
It's not clear to me how. I believe PA+"PA is consistent" would allow a model where Goodstein's theorem is true for the standard natural numbers, but that also contains some nonstandard integer N for which Goodstein's theorem is false. I think that's exactly the case that's ruled out by the stronger statement of ω-consistency.
On the first question, how do you encode omega-consistency as a formula of PA? Just curious, it's not at all obvious to me.
I was also wondering about that, but going by the Wikipedia definition, it doesn't seem too complicated: you say, "For all encoded propositions P(x): If for every x there exists an encoded proof of P(x), then there does not exist an encoded proof of 'there exists an x such that ¬P(x)'." That is, if you can prove a proposition for each integer in the metatheory, then quantifiers within the target theory must respect that.
So I'm not convinced this is enough to conclude "forall x . P(x)" within PA itself, which is what you need to prove Goodstein's. We can merely conclude that there exists a (possibly non-standard) n coding for that statement.
https://en.wikipedia.org/wiki/%CE%A9-consistent_theory#Relat...
The Wikipedia article says T is omega-consistent if "T + RFN_T + the set of all true sentences is consistent", which should mean the same thing as "T + RFN_T is true".
Does anyone have recommendations for beginner-friendly resources that explain these encoding techniques?
Boyer and Moore wrote an automated theorem prover that goes with this theory. I have a working copy for GNU Common LISP at [2].
"It is perhaps easiest to think of our program much as one would think of a reasonably good mathematics student: given the axioms of Peano, he could hardly be expected to prove (much less discover) the prime factorization theorem. However, he could cope quite well if given the axioms of Peano and a list of theorems to prove (e.g., “prove that addition is commutative,” . . . “prove that multiplication distributes over addition,” . . . “prove that the result returned by the GCD function divides both of its arguments,” . . . “prove that if the products over two sequences of primes are identical, then the two sequences are permutations of one another”)." - Boyer and Moore
"That's because there are nonstandard models of PA which contain infinite natural numbers. So PA may be able to prove that it produces a proof, but can't prove that the proof is of finite length. And therefore it might not be a valid proof."
If PA proves "PA proves X" then PA can prove X. This is because the key observation is not that there are nonstandard models, but rather that the standard natural numbers model PA.
Therefore if PA proves "PA proves X", then there is in fact a standard, finite natural number that corresponds to the encoded proof of "PA proves X". That finite natural number can be used then to construct a proof of X in PA.
My logic is very rusty at this point, but if someone could give me an argument that you cannot move the 'Provable' outside the 'forall', I would really appreciate that, without making reference to Goodstein sequences. In other words, that in general for propositions 'P' it is not true that proving "forall n, Provable(P(n))" implies you can prove "Provable(forall n, P(n))".
Not true.
From PA we can construct a function that can search all possible proofs that can be constructed in PA. In fact I outlined one way to do this at the end of my answer.
With this function, we can construct a function will-return that analyzes whether a given function, with a given input, will return. This is kind of like an attempted solution to the Halting Problem. We know that it doesn't always work. But we also know that it works a lot of the time.
From will-return we can create a function opposite-return that tries to return if a given function with a given input would not, and doesn't return if that function would. This construction is identical to the one in the standard proof of the Halting Problem.
Now we consider (opposite-return opposite-return opposite-return). (Actually you need a step to expand the argument into this recursive form. I've left that out, but that is identical to the one in the standard proof of the Halting problem.)
PA can prove the following:
- PA proves that if PA can prove that opposite-return returns, then it doesn't. - PA proves that if PA can prove that opposite-return doesn't return, then it does. - PA proves that if it can prove everything that it proves that it can prove, then PA must have a proof of one of the two previous statements. - Therefore PA proves that if it can prove everything that it proves that it can prove, then PA is inconsistent.
This is a form of Gödel's second incompleteness theorem.
And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves".
If we assume PA to be sound, then indeed everything it proves is true.
> Not true.
Now you're saying PA is unsound.
But your article wasn't about PA proves "PA proves X", it was about "forall n : PA proves G(n)".
For PA not to prove "forall n: G(n)", there is no soundness issue, only a ω-consistency issue.
If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement.
If PA proves that it proves a statement, and then fails to prove it, PA is unsound.
There exist collections of statements such that PA proves that it proves each statement, and PA does prove each statement, but PA does not prove the collection of statements.
Our understanding of the last is helped by understanding that "PA proves that PA proves S" is logically not the same statement as, "PA proves S". Even though they always have the same truth value.
I think this is true (although I would like a significantly more succinct proof than one using Goodstein sequences as I mention here https://news.ycombinator.com/item?id=44277809), but regardless this is substantially weaker than your assertion that there are statements PA can prove that it can prove, but cannot itself prove.
In particular I can prove that for all propositions P, PA proves P if and only if P proves "Provable(P)" (i.e. "P is provable in PA").
Given PA proves P, take the finite proof of P in PA and do the usual Godel encoding to get a single number. That is a witness to the implicit existential statement behind "Provable(P)".
In the other direction, given P proves "Provable(P)", take the natural number witness of the implicit existential statement. Because the standard natural numbers satisfy PA (this is basically equivalent to the assumption that PA is consistent), we know that this natural number is in fact a standard, finite natural number. Hence we can transform this natural number back to a proof of P in PA.
This equivalence is precisely the reason why the provability relation (more accurately for our purposes stated as "provability in PA") "Provable" is valuable. If the equivalence didn't hold it would be very weird to call this relation "Provable".
In particular, this means PA proves P if and only if P proves "Provable(Provable(P))" (and so on for as many nestings of Provable as you'd like).
> If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement.
I kind of think I know what you mean by this, but definitely your conclusion is way too strong. In particular, it is true in a certain intuitive sense that PA cannot "use" the fact of "Provable(P)" to actually prove P. It is in a sense a coincidence that every P for which PA can prove P, PA can also prove "Provable(P)", since that equivalence is carried "outside" of PA. But that's not really anything to do with PA itself, but that's just rather the nature of any encoded representation.
Even what tromp is saying is quite strange to me (in apparently implying that it's normal for PA to have an omega-consistency issue). It would be very strange to assert PA is omega-inconsistent. It is tantamount to saying PA is inconsistent, since stating that PA is omega-inconsistent is saying that the standard natural numbers are not a valid model of PA.
Indeed I mis-spoke. While for all n, PA can prove P(n), it cannot prove "for all n: P(n)". I don't know if there is a name for this, but it's not an omega-inconsistency. It would only be omega-inconsistent to have PA contradict "for all n: P(n)", i.e. to prove "there exists an n: not P(n)".
But if it is an infinite collection, then a nonstandard model of PA will have statements in that collection that are not in the standard model, and they generally don't encode for correct proofs. (For one thing, those proofs tend to be infinitely long.)
"If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement."
When you say "PA proves that it proves a statement," this usually means that it proves the existence of a Gödel number of the proof of the statement. If PA proves such a Gödel number exists, then via completeness one must exist in the standard model, and this number will be a standard natural number encoding a valid finite length proof.
If the above somehow doesn't apply to the argument you are making: how?
The existence of a Gödel number in a model of PA, does not imply the existence of a proof corresponding to that Gödel number. PA can only prove the existence of the Gödel number.
Now consider a function, definable from PA, named prove-gn. It is defined such that (prove-gn n) is the Gödel number for a proof from PA that G(n) terminates. This function is somewhat complicated, but it absolutely can be constructed. And from PA we can prove that the function works as advertised.
Suppose that we are in a nonstandard model of PA. For every standard natural n, (prove-gn n) will be a standard natural, and will correspond to an actual proof. So far, so good.
But any nonstandard natural n, and this model has many, will result in (prove-gn n) being a nonstandard natural. That Gödel number does not correspond to a valid proof. And therefore, in this model, PA will prove that it proves a statement, that it does not actually prove.
Therefore, from PA, we may prove that PA proves a statement, even though it does not prove that statement. In fact the statement may even be false. And absolutely none of this causes any contradiction or consistency problem, so long as the statement in question is a statement about a nonstandard natural number, and not a standard one.
Because there is no way from PA to determine if we are in the standard model, or a nonstandard model, from PA we cannot conclude that "PA proves that it proves" implies "PA proves". They really are different concepts. And we will cause ourselves no end of confusion if we confuse them.
I don't believe this is true. I don't know what result you're using here, but I think you're mixing up "provable" and "true".
In particular your line of reasoning violates Lob's Theorem, which is a corollary of the second incompleteness theorem.
For any sentence S, if first-order PA (or any first-order theory) proves S, then that means that S holds true in every model of that theory, via the completeness (not incompleteness) theorem.
The statement "PA proves x" is equivalent to saying "there exists a natural number N which is a Gödel number encoding a proof of x." The letter "x", here, is a natural number that is assumed to encode some sentence we want to prove, that is, x = #S for some sentence S.
The above is a predicate with one existential quantifier: Provable(x) = there exists N such that IsProof(N, x) holds true, where IsProof says that N is the Gödel number of a valid proof ending in x.
If PA proves "Provable(x)", that means that the predicate "Provable(x)" holds in every model of PA. This means every model of PA would have some natural number N that satisfies IsProof(N, x). Of course, this number can vary from model to model.
However: the standard model, which has only standard natural numbers, is also another model of PA. So if PA proves "Provable(x)," and Provable(x) thus holds in every model, it must also hold in the standard model of PA. This means that there must be a regular, standard, finite natural number N_st that encodes a proof of x.
Since the standard model is an initial segment of every other model of PA, then every other model includes the standard model and all the standard natural numbers. Thus, if PA proves Provable(x), then the standard number N_st must exist in all models.
So we cannot have a situation where PA proves Provable(x) but all proofs of x must be nonstandard and infinite in length. This would mean no such proof exists in the standard model of PA - but then, via completeness, PA would not be able to prove "Provable(x)".
Suppose that we're in a nonstandard model. For all standard n, there really will be a proof. For nonstandard n, there may or may not actually be a proof.
And so PA cannot prove from the fact that it proved the existence of a proof, that PA actually proves it.
"And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves"."
It seems that for each standard n, PA proves that the Goodstein sequence terminates for that n. If also proves that it proves that the Goodstein sequence terminates for all n, and so on. But this is very different from saying "PA proves that it proves the sentence 'for all n, the corresponding Goodstein sequence terminates,'" which is what I thought you were saying.
My earlier claim is that for each n, "PA proves that it proves that G(n) terminates". But in logic there is an important distinction to be made between "PA proves" and "PA proves that it proves". From the second, you cannot conclude the first. You must actually present the proof, and then verify it.
And the reason is this. It is true that, for all standard n, "PA proves that it proves" implies that "PA proves". But for nonstandard n it does not. Since PA cannot itself distinguish standard n from nonstandard n, PA cannot follow that implication to a proof.
(All of this is based on long conversations with my logic professor back in grad school. To the extent that I get it right, https://faculty-directory.dartmouth.edu/marcia-j-groszek deserves the credit. To the extent that I get it wrong, I deserve the blame.)
In particular I'm not relying on the consistency of PA. If PA is inconsistent, "If PA proves 'PA proves X' then PA can prove X" also holds (trivially), because then PA can prove anything.
> This is because the key observation is not that there are nonstandard models, but rather that the standard natural numbers model PA.
This fact (that the standard natural numbers model PA) implies that PA is consistent, so your argument is implicitly assuming that from the outset, right? If PA is consistent then this is not something that PA can prove, so I don't see how you could run your proof in PA itself. And certainly not how you could do it in a weaker theory. Logic is subtle though... so what am I missing?
As far as I know what you're describing (namely that "Provable(X)" implies "X") is called the uniform reflection principle and added to PA is much stronger than PA alone.
> so your argument is implicitly assuming that from the outset, right?
No. My argument implicitly has a fork at the beginning.
If PA is consistent, run the usual standard natural number argument I made.
If PA is not consistent, then PA can prove everything.
Hence the statement "If PA proves 'PA proves X' then PA can prove X." goes through either way. It does not depend on the consistency of PA.
The truth predicate for PA is undefinable in PA, I agree, but you can represent the reflection principle as an axiom schema: for each formula A(x) the axiom "forall x. Provable([A(x)]) -> A(x)".
(which has the intended meaning at the meta-level, "if A(x) is provable in PA then it is true")
This is consistent with PA but much stronger. In particular it proves Goodstein's theorem, and hence consistency of PA too via cut elimination.
(or flavours of that, there are many reflection principles, but the basic idea is not to represent it as a single formula - quantify at the meta level, if you will)
Yes I agree.
All of this spun from the original comment on Math Stack Exchange, which got distilled down to this (https://news.ycombinator.com/item?id=44277936).
> > If PA proves "PA proves X" then PA can prove X.
> Not true.
As for the following
> The truth predicate for PA is undefinable in PA, I agree, but you can represent the reflection principle as an axiom schema
got it, thank you!
The main thing I'm wondering is whether this is provable in PA: "forall x, IsSentence(x) -> Provable(g(Provable(x))) -> Provable(x)", which I think it is, but haven't had the opportunity to write enough of the formal details to be 100% confident.
It was interesting because they were asking "is this all you need? What about the Peano axioms? Is there anything more primitive than the inductive data type?"
I bring it up because it's good not to take for granted that the Peano axioms are inherent, instead of just one design among many.
I believe that the natural numbers are more primitive than inductive data types, since all inductive data types may be constructed from the natural numbers alongside a small number of primitive type formers (e.g. Π, Σ, = and Ω).
I think there are two primitive sets for dependent type theory. The one with omega, and then the one with inductive types. None of them need axioms like the Peano axioms.
The work linked here doesn't show that PA is inconsistent, however: what it does is to define a new, weaker notion of what it means for PA to “prove its own consistency” and to show that PA can do that weaker thing.
Interesting work for sure, but it won't mean anything to you unless you already know a lot of logic.
I imagine their reputation problem (nobody wants to post things there because it just gets deleted) plus the 15 point requirement precludes many people from upvoting over there.
That is: Real numbers describe real, concrete relations. For e.g., saying that Jones weighs 180.255 pounds means there's a real, physical relationship -- a ratio -- between Jones' weight and the standard pound. Because both weights exist physically, their ratio also exists physically. Thus, from this viewpoint, real numbers can be viewed as ratios.
In contrast, the common philosophical stance on numbers is that they are abstract concepts, detached from the actual physical process of measurement. Numbers are seen as external representations tied to real-world features through human conventions. This "representational" approach, influenced by the idea that numbers are abstract entities, became dominant in the 20th century.
But the 20th century viewpoint is really just one interpretation (you could call it "Platonic"), and, just as it's impossible to measure ratios to infinite precision in the real world, absolutely nothing requires an incomputable continuum of reals.
Physics least of all. In 20th and 21st century physics, things are discrete (quantized) and are very rarely measured to over 50 significant digits. Infinite precision is never allowed, and precision to 2000 significant digits is likewise impossible. The latter not only because quantum mechanics makes it impossible to attain great precision on very small scales. For e.g., imagine measuring the orbits of the planets and moons in the solar system: By the time you get to 50 significant digits, you will need to take into account the gravitational effects of the stars nearest to the sun; before you get to 100 significant digits, you'll need to model the entire Milky Way galaxy; the further you go in search of precision, the exponentially larger your mathematical canvas will need to grow, and at arbitrarily high sub-infinite precision you’d be required to model the whole of the observable universe -- which might itself be futile, as objects and phenomena outside observable space could affect your measurements, etc. So though everything is in principle simulatable, and precision has a set limit in a granular universe that can be described mathematically, measuring anything to arbitrarily high precision is beyond finite human efforts.
Rationals > irrationals on computing them. You can always approximate irrationals with rationals, even Scheme (Lisp, do'h) has a function to convert a rational to decimal and the reverse. decimal to rational.
This entire discussion is about mathematical concepts, not physical ones!
Sure, yes, in physics you never "need" to go past a certain number of digits, but that has nothing to do with mathematical abstractions such as the types numbers. They're very specifically and strictly defined, starting from certain axioms. Quantum mechanics and the measurability of particles has nothing to do with it!
It's also an open question how much precision the Universe actually has, such as whether things occur at a higher precision than can be practically measured, or whether the ultimate limit of measurement capability is the precision that the Universe "keeps" in its microscopic states.
For example, let's assume that physics occurs with some finite precision -- so not the infinite precision reals -- and that this precision is exactly the maximum possible measurable precision for any conceivable experiment. That is: Information is matter. Okay... which number space is this? Booleans? Integers? Rationals? In what space? A 3D grid? Waves in some phase space? Subdivided... how?
Figure that out, and your Nobel prize awaits!
There are plenty of ratios that are ratios of other things than integers, so they are not rational numbers.
Ratios of collinear vectors are scalars a.k.a. "real" numbers, ratios of other kinds of vectors are matrices, ratios of 2D-vectors are "complex" numbers, ratios of 2 voltages are scalars a.k.a. "real" numbers, and so on.
In general, for both multiplication and division operations, the 3 sets corresponding to the 2 operands and to the result are not the same.
Only for a few kinds of multiplications and of divisions the 3 sets are the same. This strongly differs from addition operations, which are normally defined on a single set to which both the operands and the result belong.
In practice, multiplications and divisions where at least one operand or the result belong to another set than the remaining operands or result are extremely frequent. Any problem of physics contains such multiplications and divisions.
Wat? Vectors do not form a division algebra. You can't "divide" vectors! Perhaps you're thinking of the dot product, which returns a scalar.
Also, you're conflating physical/engineering concepts (such as units of measure) with mathematical abstractions such as number spaces, which don't have units.
Physical measurements exist in the real world, with its limitations, units, and practicalities.
Mathematical numbers exist in a pure theory space that is completely and totally independent of any physical reality. They're just axioms and rules. Definitions and logical conclusions.
Don't mix up the two!
On the contrary, there exists a huge number of kinds of division operations, but only very few division algebras.
For any kind of multiplication operation you can define an associated division operation (or 2 associated division operations, for non-commutative multiplications), which accepts as input the product as the dividend and one factor as the divisor, and which returns the other factor as the quotient.
In general, the division operation can never be defined for all pairs of product with factor for which the multiplication is defined, not even in a division algebra, where division by zero remains undefined. Nevertheless, in almost all cases a division operation can be defined for many of the possible product-factor pairs.
While there are some vector pairs for which the division operation is undefined, for most vector pairs the division operation is perfectly defined. Given such a pair of vectors there exists a unique matrix that will produce the dividend vector when multiplied with the divisor vector. Every kind of division is the inverse of some kind of multiplication, and this kind of division is the inverse of the matrix-vector multiplication.
The division of vectors is quite important in practice, for example for finding the rotation that will transform one object into another object, which is identical, but rotated.
Any physical measurement is a division that is not performed in a division algebra, because the operands belong to the set of values of the measured physical quantity, while the result belongs to a different set, i.e. it is a rational number that approximates the scalar a.k.a. "real" number that corresponds to the measured value.
Saying that a measurement is a division operation is not some kind of metaphor, but it is a concrete description of how to implement it. For example, there are a very large number of kinds of analog-digital converters, which are used for voltage measurement. Because they must compute the division between the measured voltage and a reference voltage, each of the many possible structures (e.g. flash converters, successive-approximation converters, pipelined converters, cyclic converters, ramp converters, sigma-delta converters, etc.) corresponds to one of the algorithms that can be used for computing a division, even with pen and paper.
All the useful parts of mathematics are not isolated of the physical world, but they abstract the properties of the physical world, to enable the description of the physical world by models about which one can reason formally.
What are called now "real numbers" were called "measures" by the ancients (who called "numbers" only the values that can be obtained by counting). The theory of "measures", i.e. "real numbers", has not been conceived in a dream, separated from the physical world, but it was conceived as an axiomatic model that attempted to match the perceived behavior of the physical quantities, such as lengths.
Similarly all the other valuable mathematical concepts have been conceived for using them in mathematical models of the physical world.
Once a useful axiomatic framework existed, there have also been many mathematical researches that were motivated only by intellectual pleasure disconnected from immediate practical necessities, like in the case of many results in number theory, or in the study of systems where only less axioms are used or some axioms are replaced, in comparison with any system applicable in practical mathematical models.
However, completely "pure" mathematical research, where one would study the consequences of some random axioms completely unrelated to the physical world (i.e. which would not use any of the mathematical concepts abstracted from the physical world, e.g. numbers, topologies etc.) has been very rare and it has not produced interesting results.
This requirement is necessary to allow the definition of a division operation, which has as operands a pair of values of that physical quantity, and as result a scalar a.k.a. "real" number. This division operation, as you have noticed, is called "measurement" of that physical quantity. A value of some physical quantity, i.e. the dividend in the measurement operation, is specified by writing the quotient and the divisor of the measurement, e.g. in "6 inches", "6" is the quotient and "inch" is the divisor.
In principle, this kind of division operation, like any division, could have its digit-generating steps executed infinitely, producing an approximation as close as desired for the value of the measured quantity, which is supposed to be an arbitrary scalar, a.k.a. "real" number. Halting the division after a finite number of steps will produce a rational number.
In practice, as you have described, the desire to execute the division in a finite time is not the only thing that limits the precision of the measured values, but there are many more constraints, caused by the noise that could need longer and longer times to be filtered, by external influences that become harder and harder to be suppressed or accounted for, by ever greater cost of the components of the measurement apparatus, by the growing energy required to perform the measurement, and so on.
Nevertheless, despite the fact that the results of all practical measurements are rational numbers of low precision, normally representable as FP32, with only measurements done in a few laboratories around the world, which use extremely expensive equipment, requiring an FP64 or an extended precision representation, it is still preferable to model the set of scalars using the traditional axioms of the continuous straight line, i.e. of the "real" numbers.
The reason is that this mathematical model of a continuous set is actually much simpler than attempting to model the sets of values of physical quantities as discrete sets. An obvious reason why the continuous model is simpler is that you cannot find discretization steps that are good both for the side and for the diagonal of a square, which has stopped the attempts of the Ancient Greeks to describe all quantities as discrete. Already Aristotle was making a clear distinction between discrete quantities and continuous quantities. Working around the Ancient Greek paradox requires lack of isotropy of the space, i.e. discretization also of the angles, which brings a lot of complications, e.g. things like rigid squares or circles cannot exist.
The base continuous dynamical quantities are the space and time, together with a third quantity, which today is really the electric voltage (because of the convenient existence of the Josephson voltage-frequency converters), even if the documents of the International System of Units are written in an obfuscated way that hides this, in an attempt to preserve the illusion that the mass might be a base quantity, like in the older systems of units.
In any theory where some physical quantities that are now modeled as continuous, were modeled as discrete instead, the space and time would also be discrete. There have been many attempts to model the space-time as a discrete lattice, but none of them has produced any useful result. Unless something revolutionary will be discovered, all such attempts appear to be just a big waste of time.
The Heisenberg uncertainty principle is just a trivial consequence of the properties of the Fourier transform. It just states that there are certain pairs of physical quantities which are not independent (because their probability densities are connected by a Fourier transform relationship), so measuring both simultaneously with an arbitrary precision is not possible.
The Heisenberg uncertainty principle says absolutely nothing about the measurement of a single physical quantity or about the simultaneous measurement of a pair of independent physical quantities.
There is no such thing as a quantity that cannot be measured, i.e. the set of its values does not have the required Archimedean group algebraic structure. If it cannot be measured, it is not a quantity (there are also qualities, which can only be compared, but not measured, so the sets of their values are only ordered sets, not Archimedean groups; an example of a physical quality, which is not a physical quantity, is the Mohs hardness, whose numeric values are just labels attached to certain values, a Mohs hardness of "3" could have been as well labeled as "Ktcwy" or with any other arbitrary string, the numeric labels have been chosen only to remember easy the order between them).
Various proposals exist in which the fundamental physical structure of space form a kind of "quantum foam". And so, somewhere near the Planck length, it doesn't even make sense to talk about distance.
What you have in mind about "ranges of values" has nothing to do with Heisenberg, but with the formalism of quantum mechanics as developed by Schroedinger, Dirac and others (not counting the matrix mechanics of Heisenberg, which was an inferior mathematical method, soon forgotten after superior alternatives were developed, and which is something completely else than the Heisenberg principle of uncertainty).
In the various variants of the formalism of quantum mechanics, the correspondent of a single value in classic dynamics is a function, the so-called wave function, but even those functions cannot be called "ranges of values". There are several interpretations of what the "wave" functions mean, but the most common is that they are probability densities for the values of the corresponding physical quantity.
Depending on the context, in quantum mechanics the value of a physical quantity may be unknown, when only the probability of it having various values is known, but the value may also be known with absolute certainty, usually in some stationary states.
In both cases the value of the physical quantity can be measured, but in the former only an average value can be measured, which nonetheless may have unlimited precision, while in the latter case the exact value can be measured, exactly like in classical dynamics.
There are pairs of physical properties, connected by a Fourier transform, that cannot both be known at once. Therefore each property is, in general, only known to be in a range. And therefore we cannot always compare these properties between different particles.
As for measurement, in the Everett interpretation the values are not known after measurement either. All that is knowable are correlations due to entanglement.
But now we are far afield. You made an a priori statement about physics. Physics is not required to oblige you. My understanding of physics says that it does not. But even if I am wrong, and it currently does oblige you, it is still not required to.
A priori assertions do not have a good history. For an example, look at Kant's assertion that reality must be described by Euclidean geometry. He was not in a position to understand the ways in which he would prove to be wrong.
Granularity is implied by some, but not all, post standard model physics. It's a very open question.
> You can measure any value to arbitrary precision
Quantum mechanics lets you refine one observable indefinitely if you are willing to sacrifice conjugate observables.
You can measure that one observable to an arbitrarily (not infinitely!) high precision -- if you have an correspondingly arbitrary duration of time and arbitrarily powerful computational resources. That measurement of yours, if exceedingly precise, might require a block of computronium which utilizes the entire energy resources of the universe. As a practical matter, that's not permitted. I'm certainly unaware of any measurement in physics to more than 100 significant digits, let alone "arbitrary precision".
In fact, as it turns out, no experiment has ever resolved structure down to the Planck length. A fundamental spatial resolution is likely to be quite a lot smaller than the Planck length; even the diameter of the electron has been estimated at anywhere from 10^-22m to 10^-81m.
The question I was responding to asked whether reals are "necessary" -- plainly, insofar as reality is concerned, they are not.
My concern with the reals goes the other direction. The reals are not closed under common operations. A lot of the work is done in complex numbers, which are. The rationals are not closed under radicals, and radicals seem pretty fundamental.
You can define a finitist model despite this. But it's ugly, and while ugliness is not physically meaningful, it tends to make progress difficult. A usable solution may yet arise; we shall (perhaps) see.
Now, are the reals necessary?
During the last decades, there have been published many research papers exploring the use of discreteness instead of the traditional continuity, but they cannot be considered as anything else but failures. The resulting mathematical models are much more complicated than the classic models, without offering any extra predictions that could be verified.
The reason for the complications is that in physics it would be pointless to try to model a single physical quantity as discrete instead of continuous. You have a system of many interrelated quantities and trying to model all of them as discrete reaches quickly contradictions for the simpler models, due to the irrational or transcendent functions that relate some quantities, functions that appear even when modeling something as simple as a rotation or oscillation. If, in order to avoid incommensurability, you replace a classic continuous uniform rotation with a sequence of unequal jumps in angular orientation, to match the possible directions of nodes in a discrete lattice, then the resulting model becomes extremely more complicated than the classic continuous model.
Everything that is known about numerical analysis is based on discreteness, instead of continuity. Every useful predictive model that we have about the world, for example for forecasting weather, depends on numerical analysis.
I consider this a success!
Forecasting weather, designing semiconductor devices, or any other such activities are all based on continuous mathematical models, which use e.g. systems of equations with partial derivatives or systems of integral equations.
Only in the last stage of solving such a problem, in order to use a digital computer the continuous mathematical model is approximated by a discrete mathematical model, which is constructed using a standard method, e.g. finite elements, boundary elements, finite differences, most of which are based on approximating an unknown function with an infinity of degrees of freedom with a function determined by a finite number of parameters, then by approximating the operations required to compute those parameters by operations with floating-point numbers.
Such an approximating method is something extremely different from formulating a discrete mathematical model of physics that is considered the exact model.
Even the graphics for a game are based on continuous models of space, not on discrete models, where it would be very difficult to implement something like the rotation of an object or perspective views.
The failures to which I have referred are the attempts to create such discrete models of physics, e.g. where the space and time are discrete not continuous.
These attempts have nothing in common with the approximating techniques, which are indeed the base for most successes in using digital computers.
Time-scale calculus is a pretty niche theoretical field that looks at blending the analysis of difference and differential equations, but I'm not aware of any algorithmic advances based on it.
In a sense this is wrong. Some say the indispensability of modern math, which includes the incomputable reals, shows that such abstract objects are required for science.
Of course not, but that would invalidate the entire project of some/many here to turn reality into something clockwork they can believe they understand. Reality is much more interesting than that.
It all gets mind-bendingly mind-bending really fast, especially with people like Harvey Friedman ( https://u.osu.edu/friedman.8/foundational-adventures/fom-ema... ) or the author of this post trying to break the math by constructing an untractably large values with the simplest means possible (thus showing that you can encounter problems that do not fit in the universe even when working in a "simple" theory)
(i saw the username and went to check audiomulch website, but it did not resolve :( )
The idea that uncountable means more comes from a bad metaphor. See https://news.ycombinator.com/item?id=44271589 for my explanation of that.
Accepting that uncountable means more forces us to debatable notions of existence. See https://news.ycombinator.com/item?id=44270383 for a debate over it.
But, finally, there is this. Every chain of reasoning that we can ever come up with, can be represented on a computer. So even if you wish to believe in some extension of ZFC with extremely large sets, PA is capable of proving every possible conclusion from your chosen set of axioms. So yes, PA is enough.
If you're not convinced, I recommend reading https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden....