The theory of classical realizability is a framework for the Curry-Howard correspondence which enables to associate a program with each proof in Zermelo-Fraenkel set theory. But, almost all the applications of mathematics in physics, probability, statistics, etc. use Analysis i.e. the axiom of dependent choice (DC) or even the (full) axiom of choice (AC). It is therefore important to find explicit programs for these axioms. Various solutions have been found for DC, for instance the lambda-term called “bar recursion” or the instruction “quote” of LISP. We present here the first program for AC.
You know you’re arguing with a psychedelic-abusing schizophrenicwho sees things, right? (Haven’t you been online long enough to recognize the very distinctive wordsalad & exclusively verbal style of argumentation, or the free association & redefining in his comments while ignoring widely-accepted physics about spacetime?) Seems like a waste of time, IMO.
I did not know any specifics. I did think it was worth my time start skimming because I have another interesting problem vaguely related; then I thought it was worth my time to understand what the objection buried under the word salad (yes, Benjamin, it’s word salad) might be, because it seemed like there might actually be one. And there was! Standard lambda calculus at face value doesn’t work with nonconstructive proofs. That’s interesting and I didn’t know it. Then:
[Googles]
as expected, looks like there’s plenty of work on this, and there’s nothing actually surprising here. My standard practice after doing something like this is to leave a perfectly-reasonable-if-they-were-reasonable question getting to the heart of what’s up, as I did; I can afford this of course because I’m much less high profile than you, or, y’know, any physicist. :D
Interestingly and a complete aside: I grew up with a close relative who wrote in That Distinctive Style and only later encountered it on the wider internet, and wasn’t that a revelation.
Have you heard of ad hominem? If that is what is called rationality and upvoted on this platform, than there is truly no hope for fruitful conversation on it. Unfortunately this attitude if you continue to uphold is certain to lead to a lot of problems and dissatisfaction for you and others.
What do you think it does to schizo that is not like me and might be genuinely schizophrenic (I did say that I am but technically I got another diagnosis which I think was more accurate) and psychotic and gets verbally attacked with an ad hominem like this? They might start to lash out at others or harm themselves.
Well done, pat yourself on the back.
>distinctive wordsalad
This is about mathematical proof and mathematical definition.
What you are saying is toxic word salad. It is irrational words, which are also literally toxic if engaged in, which I do not, as I keep my distance from such insults.
1=1 is proven to be true.
1=8 is not true, be definition.
That is not word salad, you are being an extremely impolite and contra-rational (as ad-hominem is one of the most irrational fallacies one could think of) and contra-humanistic by creating an ad hominem of a severe diagnosed condition of all things.
I rarely say this, but you and everyone that upvoted this comment should rethink what they are doing, and frankly it would make sense to be ashamed of what you just said.
Feel free to delete your comment if you think it was not appropriate.
It says it enables to associate a program with each proof in Zermelo-Fraenkel set theory. You can also, in principle associate a program to each value of the busy beaver function, or even uncountably many of them (for example for each value of the BB function a complex-valued function that based of the square of the value of the BB function as a constant in each of the complex-valued functions of each value). Even though you cannot compute the values of the busy beaver function.
That means you can associate programs to uncomputable functions, like the function of definition.
I can also associate a program to X = ?; for example rand(60). That however assumes that the natural number in question is a constant, which as I said above does not logically follow from the instruction of choosing one natural number. You can logically instruct something, and do something different. That is not a contradiction in terms of logic.
But as I said above that program would not compute X, it would merely be associated to X, which is a different notion. For example I can associate the BB function to X, but that does not make X computable, and indeed the opposite follows, as X could have the values of the BB function, which is proven to not be computable. So X could be not computable, and as it could be not computable, it is uncomputable in this context, as the question is if you can compute X without first defining it, which you cannot. Once you defined X=3, you can of course program a computer to deduce X=3, but that happens after the definition, and is not the definition of X in this context (which was asked to be done by a person) but a computational replication of an earlier definition, which is still a definition but not a choice, or even the acknowledgement that there is a choice between choice and no choice (meaning just saying X=Y which is a bit of a non-choice in this context but still valid).
You can find programs for axioms, like if have the axiom S(0)=1 I can find a program that display s(0)=1 on my screen. That is just not a definition, it is a replication or association. I can even find a program that displays 0=1 and is correct about that if I define 0 to mean the natural number 0 the symbol 1 to mean the natural number 0. All of these things are possible and valid, although a bit wild syntactically.
[Googles] Why does something like https://arxiv.org/pdf/2006.05433.pdf not resolve things? Is it simply wrong? Is it not actually applicable?
You know you’re arguing with a psychedelic-abusing schizophrenic who sees things, right? (Haven’t you been online long enough to recognize the very distinctive wordsalad & exclusively verbal style of argumentation, or the free association & redefining in his comments while ignoring widely-accepted physics about spacetime?) Seems like a waste of time, IMO.
I did not know any specifics. I did think it was worth my time start skimming because I have another interesting problem vaguely related; then I thought it was worth my time to understand what the objection buried under the word salad (yes, Benjamin, it’s word salad) might be, because it seemed like there might actually be one. And there was! Standard lambda calculus at face value doesn’t work with nonconstructive proofs. That’s interesting and I didn’t know it. Then:
as expected, looks like there’s plenty of work on this, and there’s nothing actually surprising here. My standard practice after doing something like this is to leave a perfectly-reasonable-if-they-were-reasonable question getting to the heart of what’s up, as I did; I can afford this of course because I’m much less high profile than you, or, y’know, any physicist. :D
Interestingly and a complete aside: I grew up with a close relative who wrote in That Distinctive Style and only later encountered it on the wider internet, and wasn’t that a revelation.
Have you heard of ad hominem? If that is what is called rationality and upvoted on this platform, than there is truly no hope for fruitful conversation on it. Unfortunately this attitude if you continue to uphold is certain to lead to a lot of problems and dissatisfaction for you and others.
What do you think it does to schizo that is not like me and might be genuinely schizophrenic (I did say that I am but technically I got another diagnosis which I think was more accurate) and psychotic and gets verbally attacked with an ad hominem like this? They might start to lash out at others or harm themselves.
Well done, pat yourself on the back.
>distinctive wordsalad
This is about mathematical proof and mathematical definition.
What you are saying is toxic word salad. It is irrational words, which are also literally toxic if engaged in, which I do not, as I keep my distance from such insults.
1=1 is proven to be true.
1=8 is not true, be definition.
That is not word salad, you are being an extremely impolite and contra-rational (as ad-hominem is one of the most irrational fallacies one could think of) and contra-humanistic by creating an ad hominem of a severe diagnosed condition of all things.
I rarely say this, but you and everyone that upvoted this comment should rethink what they are doing, and frankly it would make sense to be ashamed of what you just said.
Feel free to delete your comment if you think it was not appropriate.
No, I do not think it is wrong.
It says it enables to associate a program with each proof in Zermelo-Fraenkel set theory. You can also, in principle associate a program to each value of the busy beaver function, or even uncountably many of them (for example for each value of the BB function a complex-valued function that based of the square of the value of the BB function as a constant in each of the complex-valued functions of each value). Even though you cannot compute the values of the busy beaver function.
That means you can associate programs to uncomputable functions, like the function of definition.
I can also associate a program to X = ?; for example rand(60). That however assumes that the natural number in question is a constant, which as I said above does not logically follow from the instruction of choosing one natural number. You can logically instruct something, and do something different. That is not a contradiction in terms of logic.
But as I said above that program would not compute X, it would merely be associated to X, which is a different notion. For example I can associate the BB function to X, but that does not make X computable, and indeed the opposite follows, as X could have the values of the BB function, which is proven to not be computable. So X could be not computable, and as it could be not computable, it is uncomputable in this context, as the question is if you can compute X without first defining it, which you cannot. Once you defined X=3, you can of course program a computer to deduce X=3, but that happens after the definition, and is not the definition of X in this context (which was asked to be done by a person) but a computational replication of an earlier definition, which is still a definition but not a choice, or even the acknowledgement that there is a choice between choice and no choice (meaning just saying X=Y which is a bit of a non-choice in this context but still valid).
You can find programs for axioms, like if have the axiom S(0)=1 I can find a program that display s(0)=1 on my screen. That is just not a definition, it is a replication or association. I can even find a program that displays 0=1 and is correct about that if I define 0 to mean the natural number 0 the symbol 1 to mean the natural number 0. All of these things are possible and valid, although a bit wild syntactically.