The Lucas argument vs the theorem-provers--who wins and why?Godel's 1st incompleteness theorem -...
The Lucas argument vs the theorem-provers--who wins and why?
Godel's 1st incompleteness theorem - clarification.Presburger ArithmeticGödel's Incompleteness Theorem and the complexity of arithmeticWhat are some proofs of Godel's Theorem which are *essentially different* from the original proof?A meta-mathematical question related to Hilbert tenth problemundecidable sentences of first-order arithmetic whose truth values are unknownGodel's Second Incompleteness theorem and ModelsCan a stochastic Turing machine output a consistent extension of PA with positive probability?Can Turing machines clarify mathematical, philosophical, and physical existence?Turing degree of finding independent formulas
$begingroup$
In his paper, "Minds, Machines and Godel", J.R. Lucas writes the following:
Godel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true—i.e., the formula is unprovable-in-the-system—but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.
Contrariwise, the following papers,
Wilfrid Sieg and Clinton Field, "Automated search for Godel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)
Lawrence C. Paulson, "A Mechanized Proof of Godel's Incompleteness Theorems using Nominal Isabelle" (published
suggest that computers can not only show that the Godel sentence is not provable from ZF − Infinity, but can also show that it is true, provided ZF − Infinity is consistent.
Why this is important is because Lucas, in the paragraph I quoted, makes the mistake that we as humans 'see' that the Godel sentence is true. In point of fact, we actually infer the truth of the Godel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover can infer the truth of the Godel sentence, assuming ZF − Infinity is consistent).
So that is the question before us: Can computers that run theorem-proving software infer that that the Godel sentence is true (note that Sieg and Field, as well as Paulson, use ZF − Infinity rather than PA for their theorem-proving software).
lo.logic computability-theory mathematical-philosophy proof-assistants
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
$endgroup$
add a comment |
$begingroup$
In his paper, "Minds, Machines and Godel", J.R. Lucas writes the following:
Godel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true—i.e., the formula is unprovable-in-the-system—but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.
Contrariwise, the following papers,
Wilfrid Sieg and Clinton Field, "Automated search for Godel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)
Lawrence C. Paulson, "A Mechanized Proof of Godel's Incompleteness Theorems using Nominal Isabelle" (published
suggest that computers can not only show that the Godel sentence is not provable from ZF − Infinity, but can also show that it is true, provided ZF − Infinity is consistent.
Why this is important is because Lucas, in the paragraph I quoted, makes the mistake that we as humans 'see' that the Godel sentence is true. In point of fact, we actually infer the truth of the Godel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover can infer the truth of the Godel sentence, assuming ZF − Infinity is consistent).
So that is the question before us: Can computers that run theorem-proving software infer that that the Godel sentence is true (note that Sieg and Field, as well as Paulson, use ZF − Infinity rather than PA for their theorem-proving software).
lo.logic computability-theory mathematical-philosophy proof-assistants
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
$endgroup$
$begingroup$
The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
$endgroup$
– Sylvain JULIEN
9 hours ago
add a comment |
$begingroup$
In his paper, "Minds, Machines and Godel", J.R. Lucas writes the following:
Godel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true—i.e., the formula is unprovable-in-the-system—but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.
Contrariwise, the following papers,
Wilfrid Sieg and Clinton Field, "Automated search for Godel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)
Lawrence C. Paulson, "A Mechanized Proof of Godel's Incompleteness Theorems using Nominal Isabelle" (published
suggest that computers can not only show that the Godel sentence is not provable from ZF − Infinity, but can also show that it is true, provided ZF − Infinity is consistent.
Why this is important is because Lucas, in the paragraph I quoted, makes the mistake that we as humans 'see' that the Godel sentence is true. In point of fact, we actually infer the truth of the Godel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover can infer the truth of the Godel sentence, assuming ZF − Infinity is consistent).
So that is the question before us: Can computers that run theorem-proving software infer that that the Godel sentence is true (note that Sieg and Field, as well as Paulson, use ZF − Infinity rather than PA for their theorem-proving software).
lo.logic computability-theory mathematical-philosophy proof-assistants
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
$endgroup$
In his paper, "Minds, Machines and Godel", J.R. Lucas writes the following:
Godel's theorem [First Incompleteness Theorem, that is—my comment] must apply to cybernetic machines, because it is of the essence of being a machine, that it should be a concrete instantiation of a formal system. It follows that given any machine which is consistent and capable of doing simple arithmetic, there is a formula which it is incapable of producing as being true—i.e., the formula is unprovable-in-the-system—but which we can see to be true. It follows that no machine can be a complete or adequate model of the mind, that minds are essentially different from machines.
Contrariwise, the following papers,
Wilfrid Sieg and Clinton Field, "Automated search for Godel's Proofs", Annals of Pure and Applied Logic 133 (2005) 319-338 (MSN)
Lawrence C. Paulson, "A Mechanized Proof of Godel's Incompleteness Theorems using Nominal Isabelle" (published
suggest that computers can not only show that the Godel sentence is not provable from ZF − Infinity, but can also show that it is true, provided ZF − Infinity is consistent.
Why this is important is because Lucas, in the paragraph I quoted, makes the mistake that we as humans 'see' that the Godel sentence is true. In point of fact, we actually infer the truth of the Godel sentence much as a theorem-prover might infer its truth (if in fact the theorem-prover can infer the truth of the Godel sentence, assuming ZF − Infinity is consistent).
So that is the question before us: Can computers that run theorem-proving software infer that that the Godel sentence is true (note that Sieg and Field, as well as Paulson, use ZF − Infinity rather than PA for their theorem-proving software).
lo.logic computability-theory mathematical-philosophy proof-assistants
lo.logic computability-theory mathematical-philosophy proof-assistants
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
edited 1 hour ago
Martin Sleziak
3,3803 gold badges22 silver badges33 bronze badges
3,3803 gold badges22 silver badges33 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
asked 9 hours ago
Thomas BenjaminThomas Benjamin
3,1951 gold badge16 silver badges26 bronze badges
3,1951 gold badge16 silver badges26 bronze badges
$begingroup$
The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
$endgroup$
– Sylvain JULIEN
9 hours ago
add a comment |
$begingroup$
The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
$endgroup$
– Sylvain JULIEN
9 hours ago
$begingroup$
The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
$endgroup$
– Sylvain JULIEN
9 hours ago
$begingroup$
The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
$endgroup$
– Sylvain JULIEN
9 hours ago
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.
For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $PA$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.
Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $ZF$ without infinity.
Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
$endgroup$
5
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
5
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
add a comment |
Your Answer
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "504"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f334944%2fthe-lucas-argument-vs-the-theorem-provers-who-wins-and-why%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.
For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $PA$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.
Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $ZF$ without infinity.
Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
$endgroup$
5
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
5
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
add a comment |
$begingroup$
Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.
For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $PA$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.
Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $ZF$ without infinity.
Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
$endgroup$
5
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
5
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
add a comment |
$begingroup$
Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.
For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $PA$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.
Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $ZF$ without infinity.
Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
$endgroup$
Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be.
For example, Russell O'Connor formalized Gödel's incompleteness theorems in Coq. As he points out in Section 7.1, Coq can prove that the natural numbers form a model of Peano arithmetic $PA$. I cannot find in his formalization an explicit statement that Gödel's sentence is true (which is not to say it isn't there), but I am quite confident that it would take little effort to formalize such a statement.
Also, let me point out that you might be confusing meta-theory with object-theory. Paulson uses the meta theory called "Nominal Isabelle" to prove Gödel's incompleteness theorem, but the way you phrased your question sounds as if you think Paulson's mechanised proof is carried out in $ZF$ without infinity.
Lastly, I would just like to say that I never understood how one could hold the position that ugly bags of mostly water are superior to machines in their ability to understand and create mathematics. A machine is not subject to uncontrollable chemical processes, fatigue, emotions, and temptations to sacrifice just a little bit of truth for a great deal of fame.
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
answered 7 hours ago
Andrej BauerAndrej Bauer
32.4k4 gold badges82 silver badges174 bronze badges
32.4k4 gold badges82 silver badges174 bronze badges
5
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
5
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
add a comment |
5
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
5
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
5
5
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
7 hours ago
5
5
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
"ugly bags of mostly water are superior to machines in their ability to understand and create mathematics" Well, aren't we machines too? As to uncontrollable chemical processes, take a glass of water and spill it first on yourself and then on your computer. Who will emerge in a better shape? Everything has its advantages and disadvantages compared to everything else. The question is not which technology is superior but how to combine the two in the most efficient way ;-)
$endgroup$
– fedja
4 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
$begingroup$
Are we not machines programmed by billions of years of natural selection? Ah, fedja beat me to it -- I'd add that human-programmed machines are great at understanding whatever we tell them to think about, but telling them to think about "genuinely new and spontaneous mathematics" is tantamount to giving them uncontrollable chemical processes and emotions.
$endgroup$
– Alec Rhea
2 hours ago
add a comment |
Thanks for contributing an answer to MathOverflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmathoverflow.net%2fquestions%2f334944%2fthe-lucas-argument-vs-the-theorem-provers-who-wins-and-why%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
$endgroup$
– Sylvain JULIEN
9 hours ago