Yes. The term you are looking for is uncomputability.
Halting problem is most well known but that's just the beginning.
There are also numbers you can't compute. In practice, you can't compute nearly all of the numbers. Computer algorithms are just a finite sequences of symbols, you can sort them and arrange them in total order = there is countably many algorithms. However there is uncountably many real numbers between 0-1, which means there is infinitely many more numbers in that range than there are possible algorithms. You can never write a finite algorithm that will calculate any of these uncomputable numbers. We can even define some of them(chaitin's constant) and we can estimate it, but we can never compute them to any arbitrary precision(also we can only define countably many numbers as well, it's same limitation).
And there are physical limits as well. There are problems that couldn't be computed even if you made an ideal computer using all the space and energy in observable universe. Namely Bekenstein bound and Bremermann's limit.
Don't worry, all these limitations also apply to humans.
Continuum. Whenever that's aleph-1 or not it's undecidable under ZFC.
There is nothing stopping machine from doing the same reasoning process given appropriate algorithm. In principle, it could just simulate human mind and call it a day.
Sure is zoom zoom tonight. Kurt Godel proved that for any mathematical system there are proofs outside the scope of whatever axioms it uses. You need new axioms to prove more. I wish these zoom zooms would get off their fricking phones.
resources = impossible to calculate
Not true for the busy beaver case. If you could calculate BB(8000) you could use that to prove the consistency of ZFC: https://scottaaronson.blog/?p=2725
It's equivalent to the halting problem.
Technically you could still write a program that outputs BB(8000), but you wouldn't know that it's BB(8000), so I don't think that counts.
>Automated theorem proves
If you can write down a formal (and therefore computer-checkable) proof then a computer program can bruteforce it.
I don't think a non-computable version can actually be called a prover, because it doesn't (can't) output proofs. An oracle, perhaps.
*prover
I mean something where you input a statement and the computer tells you if it is true or false.
>If you can write down a formal (and therefore computer-checkable) proof then a computer program can bruteforce it.
Obviously wrong.
I can prove that there infinitely many numbers between 0 and 1 (sorry
>I mean something where you input a statement and the computer tells you if it is true or false.
That's not a prover because it doesn't create any proofs. >a computer couldn't brute force that even if it runs to infinity
Formal proofs are enumerable. You can represent a proof as a string of bits, and thereby as a natural number.
Formal proofs can be verified by a computer program. (That's more or less what "formal" means.)
That means a program can go through every possible formal proof one by one until it finds one that proves the statement.
If a formal proof exists that there are infinitely many numbers between 0 and 1 then a program can find it.
Gödel only comes into play for statements for which no formal proof exists at all.
>That's not a prover because it doesn't create any proofs.
It would need to create a proof in order to tell you if something is right or not.
>Formal proofs are enumerable. You can represent a proof as a string of bits, and thereby as a natural number.
You can represent real numbers as natural numbers but they are not enumerable.
The very fact that a proof could have a real number in it means they are not countable.
>Gödel only comes into play for statements for which no formal proof exists at all.
So when you submit one of those to the system you will not get an output.
>If a formal proof exists that there are infinitely many numbers between 0 and 1 then a program can find it.
Even when there exists a proof for something, you can not guarantee that the system will reach it. That is what uncountable means.
2 years ago
Anonymous
>You can represent real numbers as natural numbers
You can't do this for all real numbers, that's what not being enumerable means. If you try to do this there will always be real numbers you leave out (per Cantor's diagonalization argument).
>a proof could have a real number in it
It can only have a real number with a finite description in it. The real numbers with finite descriptions are enumerable, they only become un-enumerable when you start involving uncomputable numbers (the value of which can't be used in proofs).
2 is a real number, and yet it can be used in finite machine-generated proofs. Same with sqrt(2), or pi.
>Even when there exists a proof for something, you can not guarantee that the system will reach it.
Can you write it down on paper? If so then the system can reach it. If not then it doesn't fit in a mathematician's head either.
2 years ago
Anonymous
>Can you write it down on paper? If so then the system can reach it. If not then it doesn't fit in a mathematician's head either.
If you arbitrarily limit the size of the proofs, of course they are enumerable.
But I want a theorem prover, not a program that determines if the proof is longer than a certain length.
Can you even prove that all proofs are of finite length?
Even then the system is still not decidable as there are still those statements without proofs or disproofs.
No matter how many justifications you try to come up with, you won't escape the face that what you're saying is just: >if a computer could prove something, then it could prove it
And the way you justify this is by trying to change the definition of a theorem prover from something which tells you if a statement is true or false to something which proves theorems it can prove.
2 years ago
Anonymous
A theorem prover proves theorems. You prove something by producing a proof . This has always been the definition.
You can't write a computer program that tells you for arbitrary theorems whether they're true or not, I completely agree with that and I'm sorry if that wasn't clear. That's not a theorem prover though.
(I'm not very interested in semantics, so if you can propose two terms for these two things them I'm willing to switch to those.) >If you arbitrarily limit the size of the proofs, of course they are enumerable.
If the proof is finite then the program will eventually reach it, no matter how large that finite length is.
AFAIK infinitely long proofs exist as mathematical objects but aren't considered to establish mathematical truth in and of themselves. I don't know much about this though.
Anything that a human can prove, in the sense of writing down a formal proof to communicate to other humans, a computer program can also prove given sufficient resources. Do you agree? I got the sense that you didn't, but if you do then we're done.
2 years ago
Anonymous
>Anything that a human can prove, in the sense of writing down a formal proof to communicate to other humans, a computer program can also prove given sufficient resources. Do you agree?
Of course.
You could probably simulate the human mind with a computer so it seems logical that anything the mind can produce a computer can as well.
This is why AI will never be real, all we'll ever have is a long chain of if()else statements. https://orthosphere.wordpress.com/2018/05/19/godels-theorem/
“The fact that the mind cannot derive a formal proof of the consistency of a formal system from the system itself is actually the very proof that human reasoning, if it is to exist at all, must resort in the last analysis to informal, self-reflecting, intuitive steps as well. This is precisely what a machine, being necessarily a purely formal system, cannot do, and this is why Gödel’s Theorem distinguishes in effect between self-conscious beings and inanimate objects.”
Are you saying that we know ZFC is consistent? How do we know? There are loads of mathematicians who don't claim to know this.
Jaki and Penrose are wrong.
>how many years until you lose your virginity
that can be computed, it's literally <= op's lifetime >how long you will remain never being a woman
that's literally == op's lifetime
Due to limited space, time, energy etc, there's very little computers can compute in practice. It's all coarse approximations, toy scenarios, lucky guesses...
There are incalculable incalculable things
This. There isn't enough memory in the universe to count how many black dudes have been in your mom's butthole, for example.
Give me a specific example (except for the meme halting probability)
How many numbers exist between 0 and 1?
Infinite is not a number
Thrembo
have a nice day
Give me thrembo reasons why I should
thrembo is a real constant in the interval [6-7]
it is nowhere close to the infinity of real numbers
thats called an uncountable infinity
ive seen a numberphile video on it
based numberphile enjoyer
mathematics fire witches are the qtest
Yes. The term you are looking for is uncomputability.
Halting problem is most well known but that's just the beginning.
There are also numbers you can't compute. In practice, you can't compute nearly all of the numbers. Computer algorithms are just a finite sequences of symbols, you can sort them and arrange them in total order = there is countably many algorithms. However there is uncountably many real numbers between 0-1, which means there is infinitely many more numbers in that range than there are possible algorithms. You can never write a finite algorithm that will calculate any of these uncomputable numbers. We can even define some of them(chaitin's constant) and we can estimate it, but we can never compute them to any arbitrary precision(also we can only define countably many numbers as well, it's same limitation).
And there are physical limits as well. There are problems that couldn't be computed even if you made an ideal computer using all the space and energy in observable universe. Namely Bekenstein bound and Bremermann's limit.
Don't worry, all these limitations also apply to humans.
Continuum. Whenever that's aleph-1 or not it's undecidable under ZFC.
There is nothing stopping machine from doing the same reasoning process given appropriate algorithm. In principle, it could just simulate human mind and call it a day.
Traveling sales man problem, graph coloring problem (for large enough number) and list goes on and on basically any O to an exponential problems
hmm
halting problem?
128 bit encryption
1/0
literally anything that can't be reduced to hard math
a thread died for this
Give an example
how to find me a gf
.1+.2
π
yes. look up undecidability.
your mom's BMI
Your mom's body count lmao
Nontrivial Busy Beaver numbers. The function grows faster than any calculable function.
>Are there things that computers cannot calculate?
True AI, because the computationalist hypothesis is wrong.
The feeling when no girlfriend
Sure is zoom zoom tonight. Kurt Godel proved that for any mathematical system there are proofs outside the scope of whatever axioms it uses. You need new axioms to prove more. I wish these zoom zooms would get off their fricking phones.
resources = impossible to calculate
Not true for the busy beaver case. If you could calculate BB(8000) you could use that to prove the consistency of ZFC: https://scottaaronson.blog/?p=2725
It's equivalent to the halting problem.
Technically you could still write a program that outputs BB(8000), but you wouldn't know that it's BB(8000), so I don't think that counts.
What can humans calculate that computers can't?
>Automated theorem proves
If you can write down a formal (and therefore computer-checkable) proof then a computer program can bruteforce it.
I don't think a non-computable version can actually be called a prover, because it doesn't (can't) output proofs. An oracle, perhaps.
*prover
I mean something where you input a statement and the computer tells you if it is true or false.
>If you can write down a formal (and therefore computer-checkable) proof then a computer program can bruteforce it.
Obviously wrong.
I can prove that there infinitely many numbers between 0 and 1 (sorry
, you were actually right), but a computer couldn't brute force that even if it runs to infinity.
I forgot what busy beavers were and just assumed it was one of those functions that get hard to compute because you said grows faster.
>I mean something where you input a statement and the computer tells you if it is true or false.
That's not a prover because it doesn't create any proofs.
>a computer couldn't brute force that even if it runs to infinity
Formal proofs are enumerable. You can represent a proof as a string of bits, and thereby as a natural number.
Formal proofs can be verified by a computer program. (That's more or less what "formal" means.)
That means a program can go through every possible formal proof one by one until it finds one that proves the statement.
If a formal proof exists that there are infinitely many numbers between 0 and 1 then a program can find it.
Gödel only comes into play for statements for which no formal proof exists at all.
>That's not a prover because it doesn't create any proofs.
It would need to create a proof in order to tell you if something is right or not.
>Formal proofs are enumerable. You can represent a proof as a string of bits, and thereby as a natural number.
You can represent real numbers as natural numbers but they are not enumerable.
The very fact that a proof could have a real number in it means they are not countable.
>Gödel only comes into play for statements for which no formal proof exists at all.
So when you submit one of those to the system you will not get an output.
>If a formal proof exists that there are infinitely many numbers between 0 and 1 then a program can find it.
Even when there exists a proof for something, you can not guarantee that the system will reach it. That is what uncountable means.
>You can represent real numbers as natural numbers
You can't do this for all real numbers, that's what not being enumerable means. If you try to do this there will always be real numbers you leave out (per Cantor's diagonalization argument).
>a proof could have a real number in it
It can only have a real number with a finite description in it. The real numbers with finite descriptions are enumerable, they only become un-enumerable when you start involving uncomputable numbers (the value of which can't be used in proofs).
2 is a real number, and yet it can be used in finite machine-generated proofs. Same with sqrt(2), or pi.
>Even when there exists a proof for something, you can not guarantee that the system will reach it.
Can you write it down on paper? If so then the system can reach it. If not then it doesn't fit in a mathematician's head either.
>Can you write it down on paper? If so then the system can reach it. If not then it doesn't fit in a mathematician's head either.
If you arbitrarily limit the size of the proofs, of course they are enumerable.
But I want a theorem prover, not a program that determines if the proof is longer than a certain length.
Can you even prove that all proofs are of finite length?
Even then the system is still not decidable as there are still those statements without proofs or disproofs.
No matter how many justifications you try to come up with, you won't escape the face that what you're saying is just:
>if a computer could prove something, then it could prove it
And the way you justify this is by trying to change the definition of a theorem prover from something which tells you if a statement is true or false to something which proves theorems it can prove.
A theorem prover proves theorems. You prove something by producing a proof . This has always been the definition.
You can't write a computer program that tells you for arbitrary theorems whether they're true or not, I completely agree with that and I'm sorry if that wasn't clear. That's not a theorem prover though.
(I'm not very interested in semantics, so if you can propose two terms for these two things them I'm willing to switch to those.)
>If you arbitrarily limit the size of the proofs, of course they are enumerable.
If the proof is finite then the program will eventually reach it, no matter how large that finite length is.
AFAIK infinitely long proofs exist as mathematical objects but aren't considered to establish mathematical truth in and of themselves. I don't know much about this though.
Anything that a human can prove, in the sense of writing down a formal proof to communicate to other humans, a computer program can also prove given sufficient resources. Do you agree? I got the sense that you didn't, but if you do then we're done.
>Anything that a human can prove, in the sense of writing down a formal proof to communicate to other humans, a computer program can also prove given sufficient resources. Do you agree?
Of course.
You could probably simulate the human mind with a computer so it seems logical that anything the mind can produce a computer can as well.
the meaning of life
one time pad
guess which number I'm thinking of
Goedel's Theorem
This is why AI will never be real, all we'll ever have is a long chain of if()else statements. https://orthosphere.wordpress.com/2018/05/19/godels-theorem/
Humans can't do this either
“The fact that the mind cannot derive a formal proof of the consistency of a formal system from the system itself is actually the very proof that human reasoning, if it is to exist at all, must resort in the last analysis to informal, self-reflecting, intuitive steps as well. This is precisely what a machine, being necessarily a purely formal system, cannot do, and this is why Gödel’s Theorem distinguishes in effect between self-conscious beings and inanimate objects.”
Are you saying that we know ZFC is consistent? How do we know? There are loads of mathematicians who don't claim to know this.
Jaki and Penrose are wrong.
no computer can process the magnitude of how much of a homosexual OP is
how many years until you lose your virginity/how long you will remain never being a woman
>how many years until you lose your virginity
that can be computed, it's literally <= op's lifetime
>how long you will remain never being a woman
that's literally == op's lifetime
Due to limited space, time, energy etc, there's very little computers can compute in practice. It's all coarse approximations, toy scenarios, lucky guesses...