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

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













4












$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).










share|cite|improve this question











$endgroup$











  • $begingroup$
    The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
    $endgroup$
    – Sylvain JULIEN
    9 hours ago















4












$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).










share|cite|improve this question











$endgroup$











  • $begingroup$
    The argument by Lucas you quote reminds me of Penrose's book "shadows of the mind".
    $endgroup$
    – Sylvain JULIEN
    9 hours ago













4












4








4


2



$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).










share|cite|improve this question











$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






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








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




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
















  • $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










1 Answer
1






active

oldest

votes


















7












$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.






share|cite|improve this answer









$endgroup$








  • 5




    $begingroup$
    What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
    $endgroup$
    – Gerry Myerson
    6 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














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
);



);













draft saved

draft discarded


















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









7












$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.






share|cite|improve this answer









$endgroup$








  • 5




    $begingroup$
    What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
    $endgroup$
    – Gerry Myerson
    6 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
















7












$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.






share|cite|improve this answer









$endgroup$








  • 5




    $begingroup$
    What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
    $endgroup$
    – Gerry Myerson
    6 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














7












7








7





$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.






share|cite|improve this answer









$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.







share|cite|improve this answer












share|cite|improve this answer



share|cite|improve this answer










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
    6 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




    $begingroup$
    What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
    $endgroup$
    – Gerry Myerson
    6 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
6 hours ago




$begingroup$
What if "uncontrollable chemical processes, fatigue, emotions" are necessary for the creation of mathematics?
$endgroup$
– Gerry Myerson
6 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


















draft saved

draft discarded
















































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.




draft saved


draft discarded














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





















































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







Popular posts from this blog

Invision Community Contents History See also References External links Navigation menuProprietaryinvisioncommunity.comIPS Community ForumsIPS Community Forumsthis blog entry"License Changes, IP.Board 3.4, and the Future""Interview -- Matt Mecham of Ibforums""CEO Invision Power Board, Matt Mecham Is a Liar, Thief!"IPB License Explanation 1.3, 1.3.1, 2.0, and 2.1ArchivedSecurity Fixes, Updates And Enhancements For IPB 1.3.1Archived"New Demo Accounts - Invision Power Services"the original"New Default Skin"the original"Invision Power Board 3.0.0 and Applications Released"the original"Archived copy"the original"Perpetual licenses being done away with""Release Notes - Invision Power Services""Introducing: IPS Community Suite 4!"Invision Community Release Notes

Canceling a color specificationRandomly assigning color to Graphics3D objects?Default color for Filling in Mathematica 9Coloring specific elements of sets with a prime modified order in an array plotHow to pick a color differing significantly from the colors already in a given color list?Detection of the text colorColor numbers based on their valueCan color schemes for use with ColorData include opacity specification?My dynamic color schemes

Tom Holland Mục lục Đầu đời và giáo dục | Sự nghiệp | Cuộc sống cá nhân | Phim tham gia | Giải thưởng và đề cử | Chú thích | Liên kết ngoài | Trình đơn chuyển hướngProfile“Person Details for Thomas Stanley Holland, "England and Wales Birth Registration Index, 1837-2008" — FamilySearch.org”"Meet Tom Holland... the 16-year-old star of The Impossible""Schoolboy actor Tom Holland finds himself in Oscar contention for role in tsunami drama"“Naomi Watts on the Prince William and Harry's reaction to her film about the late Princess Diana”lưu trữ"Holland and Pflueger Are West End's Two New 'Billy Elliots'""I'm so envious of my son, the movie star! British writer Dominic Holland's spent 20 years trying to crack Hollywood - but he's been beaten to it by a very unlikely rival"“Richard and Margaret Povey of Jersey, Channel Islands, UK: Information about Thomas Stanley Holland”"Tom Holland to play Billy Elliot""New Billy Elliot leaving the garage"Billy Elliot the Musical - Tom Holland - Billy"A Tale of four Billys: Tom Holland""The Feel Good Factor""Thames Christian College schoolboys join Myleene Klass for The Feelgood Factor""Government launches £600,000 arts bursaries pilot""BILLY's Chapman, Holland, Gardner & Jackson-Keen Visit Prime Minister""Elton John 'blown away' by Billy Elliot fifth birthday" (video with John's interview and fragments of Holland's performance)"First News interviews Arrietty's Tom Holland"“33rd Critics' Circle Film Awards winners”“National Board of Review Current Awards”Bản gốc"Ron Howard Whaling Tale 'In The Heart Of The Sea' Casts Tom Holland"“'Spider-Man' Finds Tom Holland to Star as New Web-Slinger”lưu trữ“Captain America: Civil War (2016)”“Film Review: ‘Captain America: Civil War’”lưu trữ“‘Captain America: Civil War’ review: Choose your own avenger”lưu trữ“The Lost City of Z reviews”“Sony Pictures and Marvel Studios Find Their 'Spider-Man' Star and Director”“‘Mary Magdalene’, ‘Current War’ & ‘Wind River’ Get 2017 Release Dates From Weinstein”“Lionsgate Unleashing Daisy Ridley & Tom Holland Starrer ‘Chaos Walking’ In Cannes”“PTA's 'Master' Leads Chicago Film Critics Nominations, UPDATED: Houston and Indiana Critics Nominations”“Nominaciones Goya 2013 Telecinco Cinema – ENG”“Jameson Empire Film Awards: Martin Freeman wins best actor for performance in The Hobbit”“34th Annual Young Artist Awards”Bản gốc“Teen Choice Awards 2016—Captain America: Civil War Leads Second Wave of Nominations”“BAFTA Film Award Nominations: ‘La La Land’ Leads Race”“Saturn Awards Nominations 2017: 'Rogue One,' 'Walking Dead' Lead”Tom HollandTom HollandTom HollandTom Hollandmedia.gettyimages.comWorldCat Identities300279794no20130442900000 0004 0355 42791085670554170004732cb16706349t(data)XX5557367