@user21820 Is the function of all countable Boolean sequence $f: \Bbb{N}\to \text{Bool}$ an example of an indicator function of the universe hence impredicative?
@Secret Do you mean type or function of all ...? As a type, it depends on how you set up types in the system. In my preferred approach, it is merely a partial function on the universe, and in general "x ∈ (N→bool)" could be true or false or null (neither), where these values are the same as in Kleene's 3-valued logic. This approach is consistent with having a universal type obj that contains obj→bool.
In the higher-order logic approach, N→bool decidably splits (is an indicator function on) the universe, but if you want S→T to decidably split the universe then you cannot have a universal type obj otherwise obj→bool can be used to diagonalize. You should try to figure out how to do this; it's not hard!
This reason is why I do not quite favour the higher-order logic approach, since if we can conceive and describe the hierarchy of orders, then surely it is sensible to conceive of the entire universe. It appears to me that the only way out of this problem is to allow the system to create an order for each computable ordinal that can be proven (using objects in previously created orders), and then to allow an object to quantify over only objects that can be proven to be of lower order.
But it seems rather messy, so I don't quite like it, though it actually seems reasonable if one can justify the meaningfulness of having every function type decidably split the universe. Even for just (N→bool) I don't see how one can justify it, since it is essentially the same as the classical power-set.
The first indescribable number technically cannot exist besides the obvious reason that this sentence uniquely defines it (albeit impredicatively). Since the reals don't have a well order in the absence of any (nonconstructive) choice function, there isn't any 1st indescribable number
I am guessing that without the reals being well ordered, we cannot even find a 1st element because there are infinitely decreasing chains to prevent us form sepcifying which one is 1st even in an impredicative scenario
so let alone finding the 1st indescribable number
So I guess my comment is more like Berry's paradox in the context of the reals I think...
I don't know if that can ever be solved in any non paraconsistent logic (classical and intuitionist logic), since that paradox basically has its prove and contradiction at the same time, hence is self contradictory
It's self referential nature so means it will be impredicative but I guess I need to look more closely to see if I miss anything...
@Secret No there is no contradiction. There is only a basic logic error. Did you read the post I showed you previously about paradoxes?
I didn't explicitly deal with Berry's paradox in that post, but the error in the naive formulation of Berry's paradox is of pretty much the same kind as in the liar paradox.
It turns out (coincidentally?) that when we use provability instead of truth, then all the paradoxes can be transformed into important theorems about provability logic.
Liar paradox → Godel's incompleteness theorems.
Curry's paradox → Lob's theorem.
Berry's paradox → Another proof of incompleteness theorems. (Also related to Chaitin's proof via Kolmogorov complexity, and to the uncomputability of the Busy Beaver function.)
Quine's paradox → Modal fixed-point theorem (which can be used together with the Hilbert-Bernays derivability conditions to prove all the other theorems).
*head is spinning* just when I thought manipulating the syntax of logic is going to be like abstract algebra, it turns out like analysis, too many arrows are happening at the same time and now I lost track, grrr I guess I need to reread these in more detail...
The only point I understood in that post of yours is that classical (2 valued) logic can only deal with predicates that exists (i.e. assuming that they are always provable, I think...?)
(Once again, I am bad at comprehending negative abstractions (things of the form "X is such that X does not satisfy P")). What extra truth value we need to handle the LEM fail case. So far I am only aware of intuitionist logic (which has continuumly many truth values) and Kleene's 3 value logic (true, false, null)?
That's where we can't exactly say "truth value" without first deciding what exactly we want to capture by an extended notion of "truth" beyond real-world truth.
In my approach, I take Kleene's 3-valued logic because it fits nicely within a predicative viewpoint.
(NB MY poor ability at comprehending negative abstractions is one reason I tend to end up doing direct proofs instead of proof by contradictions in most of my learning)
Namely, there are real-world entities and for sentences about those we can have LEM, and there are also concepts (that may not have fixed real-world entities corresponding to them).
Predicativity itself is one of these concepts, for example. If you think of conceptual collections as an open categorization, then it makes sense. Namely, over time each conceptual collection accepts more things and rejects more, but never changes its mind on anything that has been accepted or rejected.
(N→bool) is an example of a conceptual collection. Over time, everything that you can convince me is a member will be accepted by it, and everything that you can convince me is not a member will be rejected by it. But not everything will fall into one of these two cases.
So that's what the third truth-value (null) means to me.
Yes they are indeed related in my opinion. That's why I said that Skolem's paradox may potentially be resolved in a satisfying way via 3-valued logic.
Recall that Cantor's theorem shows that there is no surjection from S onto (S→bool) for any type S, but there should not be a way to prove that there is no injection from (S→bool) into S. So one can't affirm that N is strictly smaller than (N→bool), even though it certainly is simpler.
Right, so (N→bool) may still be countable since the uncomputable (even if finite turing jumps are allowed) indicators functions will be registered as null (since the program that tries to decide them will run forever) and thus not included as terms of the (N→bool) type
In general, you can see that if the universal type obj is only required to contain N and function types, then similarly one should be unable to prove that obj injects into N.
Though we can prove that N does not surject onto obj.
(I am starting to wonder had this universe have at least countable memory and that supertasks are realisable, then uncoutable cardinalities may be predicative (because then a countable string output will be acceptable as computable)... but I digress)
I wonder if the hierarchy of mathematics is like this:
1. Mathematics (contains all human conceived mathematics, future mathematics, as well alien mathematics we don't know yet)
2. Nonconstructive (classical) mathematics: Those that allow nonconstructive objects
3. Constructive mathematics: Those that requires the objects to not only be definable, but described in terms of simpler objects in the formal system
4. Predicative mathematics: Those that make clear distinction on what is provable (at least true or false) and what is not, and reject those that are not provable to be included as part of an object (Otherwise I don't fully understood it, especially there are many conflicting definitions afaik)
Haha (1) is nearly the same as saying "any symbol-pushing game". But if you believe that computable stuff isn't the limit of what humans can do, then you might think (1) may include more than just computable formal systems. So far though, even quantum computability is subsumed by Turing computability. So nothing suggests that there is anything more.
@Secret Typically predicative mathematics assumes as given a fixed collection that satisfies the axioms for naturals. And then everything else is built predicatively on top, meaning that you don't assume anything for granted until you have justified its existence.
More precisely, you can come up with concepts but they may not have instantiations.
Predicative concepts are precisely those which you can justify having instantiations.
How does that differ from constructive mathematics, because they also require you can explicitly build the object in some way using already constructed objects?
This is not the usual way people have described predicativity, but in my view it's more generous. The usual view is that predicative mathematics allows constructing anything whose definition does not involve quantifying over a collection that includes itself.
But the usual view will necessarily exclude quantifying over the universe from being predicative, when it's not necessarily so.
@Secret There is no clear cut distinction. Some people use "constructive" when they actually mean "intuitionistic", which is orthogonal to predicativism.
Others use "constructive" when they feel the constructed objects are somewhat solid.
The mathematics that I felt most comfortable (and thus governs my way of thinking) is described in words as "Using what is given, build new things". For an example:
1. The following are the raw materials provided for you : ABCDEFG... 2. L is a new thing made from using AB 3. K s a new thing made from using LCD 4. In general, proofs are done by using what is given, and then work your way towards the required conclusion, or counterexample, or show it is undecidable
I am not sure where in constructive and predicative mathematics I fell for my way of thinking through
If you take the formalist viewpoint, you can literally do all mathematics, no matter using strong systems like ZFC, because your proof is a solid object that encodes the symbol-pushing strategy to get from raw materials (axioms) to desired entities (your theorem).
The problem comes when ascribing more to the foundations than symbol-pushing, which of course we want to, otherwise we wouldn't have invented those and desired to call them "foundations".
I tend to prefer direct proofs since I can visualise all the manipulations that I use to assemble objects into the proof I need. I don't prefer proof by contradiction as much since I can only trust the object exists by negating contradiction, but I don't have a solid graps on how it consists of the given raw materials
For example, when asked about some subset of natural numbers, I prefer to be able to write a formula that enumerate all its members
Every use of LEM corresponds to asking an oracle for the truth value of that sentence (which presupposes the meaningfulness of that sentence with respect to some external reality).
So if one believes that natural numbers have a well-defined sense in reality, then one can justify LEM for arithmetical sentences. Simply put, given any program in a Turing-complete language (like Python 3) on some given input, run on a computer with unlimited memory and time, will it eventually halt? If you agree that the answer is always yes or no, then you have essentially agreed to LEM for Σ1-sentences.
And then it's not hard to climb up the finite Turing jumps using a similar inquiry.
But if you reject that first claim, then you are pretty much stuck.
Hmm, so rejecting LEM will be equivalent to saying that the halting problem is undecidable even in principle (that is, suppose we can pick individual halting algorithms, there is no predetermined but unknowable time that it will halt)?
I think that does not sound quite far fetched, since there's an analogy in non realist interpretations, the value of an observable of a quanutm state does not even exist before measurement
That I am not sure. sure we can count objects one by one and notate them with a numeral and they are well ordered and thus we call them the naturals, can the naturals exists as some independent physical entity, I have no idea
I mean, what even does the concept of 1 look like intrinsically (but that's more philosophical)
All mathematical objects are human concepts and don't exactly exist physically, but it makes sense to ask whether there is an interpretation mapping them to physical entities. PA seems to have one at human scales.
I am thinking more about: Mathematics as a whole is a language and hence a cultural construct (that is, I don't quite buy the idea that nature is intrinsically mathematical, its just the way we humans comprehend it and see patterns everywhere), but there are concepts of mathematical objects which can be encoded or represented in a physical medium, thus due to laziness or something else, we tend to refer the representation as the object itself
e.g. two oranges placed together can be used to communicate the concept 2, which is a mathematical object
It's not as clear whether you would accept definedness of the halting problem for programs that can use the first jump. Arguably, you should, because you can 'use facts of reality' to simulate such programs. At every oracle call, you just continue down the path dictated by the answer to the oracle question in reality. Either it halts (after finitely many steps which include oracle calls) or it does not halt. So you should accept LEM for Σ2-sentences too. And repeat this argument.
@Secret No real disagreement with your not buying the notion that nature is intrinsically mathematical; after all until we specify which mathematics (you had 4 levels above), the notion itself is ill-defined.
But if you just ask about which logic is valid for reality, I say without doubt classical logic. Pure logic doesn't have any axioms about particular objects though, so this is not saying much.
I use the quantum example as analogy because just like the indefinedness of halting algorithms, they both don't have a preexisting but unknowable value. That does not mean that the halting algorithm is like a quantum state cause for a quantum state, when you measure it, its value will be defined, but not for a halting algorithm, because there exists no analogous notion to make it to have a truth value
As you saw from my post on Phil SE, I do believe that natural numbers don't have an exact interpretation in reality, simply due to finiteness of the observable universe, even if we ignore quantum effects. But the question then is how good approximation is it?
If your answer is that the mere inexactness is sufficient to render the halting problem unanswerable, then okay I can't argue against that.
After all, executing a program that keeps appending a zero to the end of a string is bound to hit the limit of the size of the observable universe sooner or later...
But as I said we still have a lot of explaining to do as to why PA (with closure under arithmetic operations plus LEM plus induction) doesn't seem to prove empirically false arithmetical sentences.
That is one of the things that people who consider all mathematics as meaningless to the real world always fail to explain.
Well, I think the answer to the question of the exact interpretation of naturals will involve an even harder question: Does there exist physical interpretations in reality of the concept "countably infinite", or more eaiser to comprehend version: Can a physical infinity exist.
If supertasks are impossible due to finite memory (as suggested by the finiteness of the observable universe) then it is possible that infinity cannot be physical and thus for the naturals, there will exist a smallest (extremely large) natural number which beyond that no entitiy in our universe can represent it
I do believe your last sentence. In the precise sense that errors will get larger and larger with the length of the string and we will be unable to guarantee accuracy in arithmetic operations.
But I still can't answer my question of why we don't see false theorems of PA.
So not literally your last sentence, since there is not really a smallest. Accuracy just gets worse and worse.
But is it possible to quantify that uncertainty of verification. For all topics I have read so far about validity of a proof, they either said we can do it or we cannot (cf P vs NP problems), but not something like "There's 50% chance we can do it"?
But then I don't know how useful is to introduce fuzzy and modal logic in the context of proof verification, nor am I familar with it enough
I never thought much about that. My first thought is to devise a first-order theory that is close enough to PA that it can prove the theorems of PA that have real-world applications and yet have some inbuilt cutoff that does not affect those theorems when we apply them.
Simple tricks like replacing every quantifier with a bounded one work somewhat but are very unsatisfying.
Some long time ago I was rambling about an idea on what happens if a proof is allowed to be partially successful for each step in its evaluation, so during the course of writing out the proof, there will be probabilities assign to how successful can one rewrite a step from 1 to 2 and thus a proof becomes something like a probability tree
e.g. imagine the usual irrationality of $\sqrt{2}$ being in such framework, then you can conclude something like "There is 50% chance that $\sqrt{2}$ is rational"
but again, that's still far from rejecting LEM so I think my mind is not flexible enough
@Secret But that makes no sense. It is an empirical fact that you can't find any finite binary strings that encode positive naturals p,q such that p^2 = 7·q^2.
How can you explain this empirical fact without using some rather concrete and certain proofs?
I changed the 2 to a 7, because you might argue that binary is too helpful for the case of sqrt(2).
Hmm... I have not thought that deep in a computational perspective before, I guess before all the conversations today, I might be a formalist (because one reason I like abstract algebra a lot is because I can prove things by formal manipulations) and rarely thought about the more practical, computational implementation of the proofs themselves, which will be where the non LEM cases readily arises
Perhaps for my framework I might be able to think of it this way: Consider the proof: There are no finite binary strings that can represent $p^2=7q^2$. Now, a series of program is written in order to implement the proof. However each computer is not perfect and there are nonzero chance it makes some errors in the string.
Suppose I used 1000 computers for this proof and 1 of these, due to errors in the string causing some 0 to become 1, managed to came up a finite string thus it provided a contradiction. Then suppose these computers are the only things we have to prove it (because we reject…
That is not very useful though, so my ramble will be indeed just rambles
though, this is worth to think about as more complicated proofs (such as the abc conjecture) are machine proved and we might need to trust the machines are giving us the correct answer since manual checking will took too long
The proof is wrong and you have given a correct counter-example.
The theorem, however, is correct. One way to prove it (besides the countless existing ones you see on this same question in Math SE) is as follows:
$p^2 = \gcd(p^2,nq^2) \mid \gcd(p^2,n) \gcd(p^2,q^2) \mid \gcd(p^2,n) \gcd(p,q)^2 ...
p^2 | n so n = k·p^2 for some integer k. But p^2 = n·q^2, so put those together to conclude that q^2 = 1.
Very few people know of this simple proof. I found it something like a decade ago when trying to prove the general irrationality of sqrt(n) without prime factorization.
This is a very constructive proof, I did not knew that before as you said
Btw, with this proof, I can illustrate what my ramble is like: The ramble is basically saying that the = sign holds e.g. $50$% of the time. Thus you can imagine for this proof, since there are 2 equal signs, the conclusion holds 25% of the time.
It's indeed a very nonsensical idea but that's a random thing I came up when my mind decided to mix probability theory with proof theory
but suppose there really is a part of mathematics where it will make sense, then we end up with proofs becoming probabiltiy trees, and truth values and verifibility of proofs will become probabilistic
The proof is wrong and you have given a correct counter-example.
The theorem, however, is correct. One way to prove it (besides the countless existing ones you see on this same question in Math SE) is as follows:
$p^2 = \gcd(p^2,nq^2) \mid \gcd(p^2,n) \gcd(p^2,q^2) \mid \gcd(p^2,n) \gcd(p,q)^2 ...
Mathworks (Not the main chat!)
Mathworks (Not the main chat!)