Is finitary method for Hilbert and modern logic - Turing computability?
It is known that Hilbert proposed in the state of crisis of foundations of mathematics that we create formal theories which we analyze using "proof theory" or "metamathematics". He then also said that such analysis must be finitary in order to be convincing enough [Kleene "Introduction to Metamathematics" 1971].
I have some sort of intuition behind what finitary means just because I have seen a lot of metamathematical proofs. But the problem is that I have never found any source which said "Hilbert by finitary probably meant ... ". Also, I am confused about what logicians nowadays consider to be finitary in metamathematical reasoning.
When I worked through Godel's incompleteness theorem as presented in Kleene's "Introduction to Metamathematics" it used a lot of properties of natural numbers. Then I thought to myself - why would one formalize number theory if one uses it in metamathematics anyways? Then, my answer would be, because we would like to formalize even more abstract theories like real numbers (which are uncountably infinite) and set theory, and so forth. But then what makes natural numbers so reliable and other theories not? Recently I started learning about Turing machines and, even though Hilbert proposed finitary methods before the development of Turing machines, I feel like this is the closest that I have to being a finitary method. There, natural numbers play a special role because they are countable and each number can be represented as, say, finite amount of marks on the tape. For example, for the proof of Godel's incompleteness theorem we show that functions like predicate being a prime number are primitive recursive functions (which are therefore Turing computable functions). I feel like then the feeling of being secure with such operations (like, why + on natural numbers commutes) basically just means a statement that one might mechanically check for arbitrary two numbers certain property. So, we reduce proofs to being purely mechanical without intuition at all. Then it also makes sense why Turing machines are required to compute in finite steps because then it means that whenever someone doesn't believe me in metamathematical proof using natural numbers then one can check the statement by writing certain strings under certain well described rules (and if numbers are not too large) and just check it. This for me suffices to be finitary and convincing enough for metamathematics.
Why this is important to me? I just want to understand when one says "let us use finitary methods" what does that mean.
What do you think? I would appreciate your opinions and comments about this. I hope I made myself clear enough - if not please let me know.
logic math-history
asked Jan 4 at 0:20
Daniels Krimans
48529
add a comment |
It is known that Hilbert proposed in the state of crisis of foundations of mathematics that we create formal theories which we analyze using "proof theory" or "metamathematics". He then also said that such analysis must be finitary in order to be convincing enough [Kleene "Introduction to Metamathematics" 1971].
I have some sort of intuition behind what finitary means just because I have seen a lot of metamathematical proofs. But the problem is that I have never found any source which said "Hilbert by finitary probably meant ... ". Also, I am confused about what logicians nowadays consider to be finitary in metamathematical reasoning.
When I worked through Godel's incompleteness theorem as presented in Kleene's "Introduction to Metamathematics" it used a lot of properties of natural numbers. Then I thought to myself - why would one formalize number theory if one uses it in metamathematics anyways? Then, my answer would be, because we would like to formalize even more abstract theories like real numbers (which are uncountably infinite) and set theory, and so forth. But then what makes natural numbers so reliable and other theories not? Recently I started learning about Turing machines and, even though Hilbert proposed finitary methods before the development of Turing machines, I feel like this is the closest that I have to being a finitary method. There, natural numbers play a special role because they are countable and each number can be represented as, say, finite amount of marks on the tape. For example, for the proof of Godel's incompleteness theorem we show that functions like predicate being a prime number are primitive recursive functions (which are therefore Turing computable functions). I feel like then the feeling of being secure with such operations (like, why + on natural numbers commutes) basically just means a statement that one might mechanically check for arbitrary two numbers certain property. So, we reduce proofs to being purely mechanical without intuition at all. Then it also makes sense why Turing machines are required to compute in finite steps because then it means that whenever someone doesn't believe me in metamathematical proof using natural numbers then one can check the statement by writing certain strings under certain well described rules (and if numbers are not too large) and just check it. This for me suffices to be finitary and convincing enough for metamathematics.
Why this is important to me? I just want to understand when one says "let us use finitary methods" what does that mean.
What do you think? I would appreciate your opinions and comments about this. I hope I made myself clear enough - if not please let me know.
logic math-history
asked Jan 4 at 0:20
Daniels Krimans
48529
Probably Hilbert meant that finite many axioms should be sufficient to formally derive the complete mathematics.
– Peter
2 days ago
@Peter Thanks for your comment! From my experience I can tell that probably finitary is used when talking not about a formal system (such that it has some property like finite axioms) but about metamathematical reasoning about formal systems in general.
– Daniels Krimans
yesterday
add a comment |
It is known that Hilbert proposed in the state of crisis of foundations of mathematics that we create formal theories which we analyze using "proof theory" or "metamathematics". He then also said that such analysis must be finitary in order to be convincing enough [Kleene "Introduction to Metamathematics" 1971].
I have some sort of intuition behind what finitary means just because I have seen a lot of metamathematical proofs. But the problem is that I have never found any source which said "Hilbert by finitary probably meant ... ". Also, I am confused about what logicians nowadays consider to be finitary in metamathematical reasoning.
When I worked through Godel's incompleteness theorem as presented in Kleene's "Introduction to Metamathematics" it used a lot of properties of natural numbers. Then I thought to myself - why would one formalize number theory if one uses it in metamathematics anyways? Then, my answer would be, because we would like to formalize even more abstract theories like real numbers (which are uncountably infinite) and set theory, and so forth. But then what makes natural numbers so reliable and other theories not? Recently I started learning about Turing machines and, even though Hilbert proposed finitary methods before the development of Turing machines, I feel like this is the closest that I have to being a finitary method. There, natural numbers play a special role because they are countable and each number can be represented as, say, finite amount of marks on the tape. For example, for the proof of Godel's incompleteness theorem we show that functions like predicate being a prime number are primitive recursive functions (which are therefore Turing computable functions). I feel like then the feeling of being secure with such operations (like, why + on natural numbers commutes) basically just means a statement that one might mechanically check for arbitrary two numbers certain property. So, we reduce proofs to being purely mechanical without intuition at all. Then it also makes sense why Turing machines are required to compute in finite steps because then it means that whenever someone doesn't believe me in metamathematical proof using natural numbers then one can check the statement by writing certain strings under certain well described rules (and if numbers are not too large) and just check it. This for me suffices to be finitary and convincing enough for metamathematics.
Why this is important to me? I just want to understand when one says "let us use finitary methods" what does that mean.
What do you think? I would appreciate your opinions and comments about this. I hope I made myself clear enough - if not please let me know.
logic math-history
asked Jan 4 at 0:20
Daniels Krimans
48529
It is known that Hilbert proposed in the state of crisis of foundations of mathematics that we create formal theories which we analyze using "proof theory" or "metamathematics". He then also said that such analysis must be finitary in order to be convincing enough [Kleene "Introduction to Metamathematics" 1971].
I have some sort of intuition behind what finitary means just because I have seen a lot of metamathematical proofs. But the problem is that I have never found any source which said "Hilbert by finitary probably meant ... ". Also, I am confused about what logicians nowadays consider to be finitary in metamathematical reasoning.
When I worked through Godel's incompleteness theorem as presented in Kleene's "Introduction to Metamathematics" it used a lot of properties of natural numbers. Then I thought to myself - why would one formalize number theory if one uses it in metamathematics anyways? Then, my answer would be, because we would like to formalize even more abstract theories like real numbers (which are uncountably infinite) and set theory, and so forth. But then what makes natural numbers so reliable and other theories not? Recently I started learning about Turing machines and, even though Hilbert proposed finitary methods before the development of Turing machines, I feel like this is the closest that I have to being a finitary method. There, natural numbers play a special role because they are countable and each number can be represented as, say, finite amount of marks on the tape. For example, for the proof of Godel's incompleteness theorem we show that functions like predicate being a prime number are primitive recursive functions (which are therefore Turing computable functions). I feel like then the feeling of being secure with such operations (like, why + on natural numbers commutes) basically just means a statement that one might mechanically check for arbitrary two numbers certain property. So, we reduce proofs to being purely mechanical without intuition at all. Then it also makes sense why Turing machines are required to compute in finite steps because then it means that whenever someone doesn't believe me in metamathematical proof using natural numbers then one can check the statement by writing certain strings under certain well described rules (and if numbers are not too large) and just check it. This for me suffices to be finitary and convincing enough for metamathematics.
Why this is important to me? I just want to understand when one says "let us use finitary methods" what does that mean.
What do you think? I would appreciate your opinions and comments about this. I hope I made myself clear enough - if not please let me know.
logic math-history
logic math-history
asked Jan 4 at 0:20
Daniels Krimans
48529
asked Jan 4 at 0:20
Daniels Krimans
48529
asked Jan 4 at 0:20
Daniels Krimans
48529
asked Jan 4 at 0:20
Daniels Krimans
48529
asked Jan 4 at 0:20
Daniels Krimans
48529
48529
Probably Hilbert meant that finite many axioms should be sufficient to formally derive the complete mathematics.
– Peter
2 days ago
@Peter Thanks for your comment! From my experience I can tell that probably finitary is used when talking not about a formal system (such that it has some property like finite axioms) but about metamathematical reasoning about formal systems in general.
– Daniels Krimans
yesterday
add a comment |
Probably Hilbert meant that finite many axioms should be sufficient to formally derive the complete mathematics.
– Peter
2 days ago
@Peter Thanks for your comment! From my experience I can tell that probably finitary is used when talking not about a formal system (such that it has some property like finite axioms) but about metamathematical reasoning about formal systems in general.
– Daniels Krimans
yesterday
Probably Hilbert meant that finite many axioms should be sufficient to formally derive the complete mathematics.
– Peter
2 days ago
Probably Hilbert meant that finite many axioms should be sufficient to formally derive the complete mathematics.
– Peter
2 days ago
@Peter Thanks for your comment! From my experience I can tell that probably finitary is used when talking not about a formal system (such that it has some property like finite axioms) but about metamathematical reasoning about formal systems in general.
– Daniels Krimans
yesterday
@Peter Thanks for your comment! From my experience I can tell that probably finitary is used when talking not about a formal system (such that it has some property like finite axioms) but about metamathematical reasoning about formal systems in general.
– Daniels Krimans
yesterday
add a comment |
0
active
oldest
votes
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
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%2fmath.stackexchange.com%2fquestions%2f3061181%2fis-finitary-method-for-hilbert-and-modern-logic-turing-computability%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
Thanks for contributing an answer to Mathematics Stack Exchange!
- 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.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- 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.
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%2fmath.stackexchange.com%2fquestions%2f3061181%2fis-finitary-method-for-hilbert-and-modern-logic-turing-computability%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
Probably Hilbert meant that finite many axioms should be sufficient to formally derive the complete mathematics.
– Peter
2 days ago
@Peter Thanks for your comment! From my experience I can tell that probably finitary is used when talking not about a formal system (such that it has some property like finite axioms) but about metamathematical reasoning about formal systems in general.
– Daniels Krimans
yesterday