Formalist understanding of metalogical proofs












3












$begingroup$


How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts of metalogical theorems attest to the validity of the logic a formalist must hold dear, thus it seems problematic they are unjustifiable within this perspective.






logic foundations philosophy







share|cite|improve this question









$endgroup$












  • $begingroup$
    This may be a question more suitable for philosophy.stackexchange.com.
    $endgroup$
    – user458276
    2 hours ago










  • $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    1 hour ago


















3












$begingroup$


How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts of metalogical theorems attest to the validity of the logic a formalist must hold dear, thus it seems problematic they are unjustifiable within this perspective.






logic foundations philosophy







share|cite|improve this question









$endgroup$












  • $begingroup$
    This may be a question more suitable for philosophy.stackexchange.com.
    $endgroup$
    – user458276
    2 hours ago










  • $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    1 hour ago
















3












3








3





$begingroup$


How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts of metalogical theorems attest to the validity of the logic a formalist must hold dear, thus it seems problematic they are unjustifiable within this perspective.






logic foundations philosophy







share|cite|improve this question









$endgroup$




How can a formalist understand a metalogical proof such as the completeness theorem? These proofs exist exclusively outside of a logical system where the "rules of the game" are undefined. These sorts of metalogical theorems attest to the validity of the logic a formalist must hold dear, thus it seems problematic they are unjustifiable within this perspective.






logic foundations philosophy




logic foundations philosophy






share|cite|improve this question













share|cite|improve this question











share|cite|improve this question




share|cite|improve this question










asked 2 hours ago









Keefer RowanKeefer Rowan

1819




1819












  • $begingroup$
    This may be a question more suitable for philosophy.stackexchange.com.
    $endgroup$
    – user458276
    2 hours ago










  • $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    1 hour ago




















  • $begingroup$
    This may be a question more suitable for philosophy.stackexchange.com.
    $endgroup$
    – user458276
    2 hours ago










  • $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    1 hour ago


















$begingroup$
This may be a question more suitable for philosophy.stackexchange.com.
$endgroup$
– user458276
2 hours ago




$begingroup$
This may be a question more suitable for philosophy.stackexchange.com.
$endgroup$
– user458276
2 hours ago












$begingroup$
The short answer is "formalize the metatheory"
$endgroup$
– Carl Mummert
1 hour ago






$begingroup$
The short answer is "formalize the metatheory"
$endgroup$
– Carl Mummert
1 hour ago












1 Answer
1






active

oldest

votes


















5












$begingroup$

Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $text{ZFC} vdash Phi$.



This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.



Method B. Through conservation results. There is a system $text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $text{WKL}_0$ of second-order arithmetic with the following properties:




  1. $text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).


  2. There is a finitistic proof that any $Pi^0_2$ sentence of arithmetic that is provable in $text{WKL}_0$ is provable in the finitistic system $text{PRA}$. This kind of metatheorem is known as a `conservation result'.



So a formalist can work in $text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $Pi^0_2$ sentence that she proves is already finitistically provable. Because only $Pi^0_2$ statements are viewed as meaningful in finitism, this means that any meaningful statement she proves from $text{WKL}_0$ can be proved finitistically, and hence can be "accepted".



This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.






share|cite|improve this answer











$endgroup$













  • $begingroup$
    I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
    $endgroup$
    – Carl Mummert
    1 hour ago










  • $begingroup$
    So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
    $endgroup$
    – Carl Mummert
    1 hour ago












  • $begingroup$
    Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
    $endgroup$
    – spaceisdarkgreen
    38 mins ago











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


}
});














draft saved

draft discarded


















StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3109471%2fformalist-understanding-of-metalogical-proofs%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









5












$begingroup$

Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $text{ZFC} vdash Phi$.



This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.



Method B. Through conservation results. There is a system $text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $text{WKL}_0$ of second-order arithmetic with the following properties:




  1. $text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).


  2. There is a finitistic proof that any $Pi^0_2$ sentence of arithmetic that is provable in $text{WKL}_0$ is provable in the finitistic system $text{PRA}$. This kind of metatheorem is known as a `conservation result'.



So a formalist can work in $text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $Pi^0_2$ sentence that she proves is already finitistically provable. Because only $Pi^0_2$ statements are viewed as meaningful in finitism, this means that any meaningful statement she proves from $text{WKL}_0$ can be proved finitistically, and hence can be "accepted".



This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.






share|cite|improve this answer











$endgroup$













  • $begingroup$
    I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
    $endgroup$
    – Carl Mummert
    1 hour ago










  • $begingroup$
    So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
    $endgroup$
    – Carl Mummert
    1 hour ago












  • $begingroup$
    Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
    $endgroup$
    – spaceisdarkgreen
    38 mins ago
















5












$begingroup$

Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $text{ZFC} vdash Phi$.



This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.



Method B. Through conservation results. There is a system $text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $text{WKL}_0$ of second-order arithmetic with the following properties:




  1. $text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).


  2. There is a finitistic proof that any $Pi^0_2$ sentence of arithmetic that is provable in $text{WKL}_0$ is provable in the finitistic system $text{PRA}$. This kind of metatheorem is known as a `conservation result'.



So a formalist can work in $text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $Pi^0_2$ sentence that she proves is already finitistically provable. Because only $Pi^0_2$ statements are viewed as meaningful in finitism, this means that any meaningful statement she proves from $text{WKL}_0$ can be proved finitistically, and hence can be "accepted".



This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.






share|cite|improve this answer











$endgroup$













  • $begingroup$
    I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
    $endgroup$
    – Carl Mummert
    1 hour ago










  • $begingroup$
    So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
    $endgroup$
    – Carl Mummert
    1 hour ago












  • $begingroup$
    Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
    $endgroup$
    – spaceisdarkgreen
    38 mins ago














5












5








5





$begingroup$

Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $text{ZFC} vdash Phi$.



This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.



Method B. Through conservation results. There is a system $text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $text{WKL}_0$ of second-order arithmetic with the following properties:




  1. $text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).


  2. There is a finitistic proof that any $Pi^0_2$ sentence of arithmetic that is provable in $text{WKL}_0$ is provable in the finitistic system $text{PRA}$. This kind of metatheorem is known as a `conservation result'.



So a formalist can work in $text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $Pi^0_2$ sentence that she proves is already finitistically provable. Because only $Pi^0_2$ statements are viewed as meaningful in finitism, this means that any meaningful statement she proves from $text{WKL}_0$ can be proved finitistically, and hence can be "accepted".



This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.






share|cite|improve this answer











$endgroup$



Method A. By making the metatheory explicit. The completeness theorem is provable in ZFC, so if $Phi$ is a statement of the completeness theorem in the language of ZFC then a formalist/finitist still recognizes the formal derivation that shows $text{ZFC} vdash Phi$.



This method may not be very satisfying, because it doesn't help a finitist prove anything else. The next method does that.



Method B. Through conservation results. There is a system $text{PRA}$ of arithmetic that is usually identified with finitistic reasoning. There is also a subsystem $text{WKL}_0$ of second-order arithmetic with the following properties:




  1. $text{WKL}_0$ proves the completeness theorem for countable, syntactically consistent first-order theories (every countable first-order syntactically consistent theory has a model).


  2. There is a finitistic proof that any $Pi^0_2$ sentence of arithmetic that is provable in $text{WKL}_0$ is provable in the finitistic system $text{PRA}$. This kind of metatheorem is known as a `conservation result'.



So a formalist can work in $text{WKL}_0$, and use the completeness theorem for countable theories, while knowing all the while that any $Pi^0_2$ sentence that she proves is already finitistically provable. Because only $Pi^0_2$ statements are viewed as meaningful in finitism, this means that any meaningful statement she proves from $text{WKL}_0$ can be proved finitistically, and hence can be "accepted".



This method is sometimes known as 'reductionism'. The idea is that someone can use an "ideal" theory (e.g. $text{WKL}_0$) to prove a wide variety of statements, knowing that some subclass of these statements (e.g. the $Pi^0_2$ ones) that are proved in this way are already provable in a weaker "concrete" system that the person prefers.







share|cite|improve this answer














share|cite|improve this answer



share|cite|improve this answer








edited 2 hours ago

























answered 2 hours ago









Carl MummertCarl Mummert

66.7k7132248




66.7k7132248












  • $begingroup$
    I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
    $endgroup$
    – Carl Mummert
    1 hour ago










  • $begingroup$
    So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
    $endgroup$
    – Carl Mummert
    1 hour ago












  • $begingroup$
    Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
    $endgroup$
    – spaceisdarkgreen
    38 mins ago


















  • $begingroup$
    I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
    $endgroup$
    – Carl Mummert
    1 hour ago










  • $begingroup$
    So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
    $endgroup$
    – Carl Mummert
    1 hour ago












  • $begingroup$
    Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
    $endgroup$
    – spaceisdarkgreen
    1 hour ago










  • $begingroup$
    Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
    $endgroup$
    – spaceisdarkgreen
    38 mins ago
















$begingroup$
I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
$endgroup$
– spaceisdarkgreen
1 hour ago




$begingroup$
I'm not sure I see how this helps a finitist be comfortable with the completeness theorem. Is the idea that they could do a rudimentary model theoretic proof of consistency in WKL$_0$ and be content that it means there is a 'legit' PRA consistency proof out there?
$endgroup$
– spaceisdarkgreen
1 hour ago












$begingroup$
It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
$endgroup$
– Carl Mummert
1 hour ago




$begingroup$
It means that they can prove whatever they want in WKLo, and even use the completeness theorem (which is provable in WKLo anyway), and know that even though they are using axioms that are not finitisitic, any "meaningful" (i.e. $Pi^0_2$) sentence that they happen to prove also has a finitistic proof (which can be mechanically extracted from the proof in WKLo). So they can be comfortable that, as long as they stick to WKLo, they don't have to worry about the completeness theorem proving any meaningful statements that they think are false.
$endgroup$
– Carl Mummert
1 hour ago












$begingroup$
So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
$endgroup$
– Carl Mummert
1 hour ago






$begingroup$
So, I guess it's right that, if I can prove in WKLo that a given theory is semantically consistent, then I can prove in WKLo that the theory is syntactically consistent, and that latter syntactic claim is $Pi^0_2$, so that means there is a finitistic proof that the theory is consistent. (Of course, WKLo doesn't prove too many theories are semantically or syntactically consistent). But the completeness theorem is usually read in the other direction - syntactic implies semantic consistency - and that direction is only useful for a finitist if it implies other, more meaningful statements.
$endgroup$
– Carl Mummert
1 hour ago














$begingroup$
Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
$endgroup$
– spaceisdarkgreen
1 hour ago




$begingroup$
Got it (and already +1'd before commenting). Yes, I guess that 's the soundness direction. (I also liked the analogy in the comment you deleted, that e.g. a person who doesn't believe in AC can and should use it freely in their attempts to prove the Riemann hypothesis.)
$endgroup$
– spaceisdarkgreen
1 hour ago












$begingroup$
Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
$endgroup$
– spaceisdarkgreen
38 mins ago




$begingroup$
Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
$endgroup$
– spaceisdarkgreen
38 mins ago


















draft saved

draft discarded




















































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.




draft saved


draft discarded














StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3109471%2fformalist-understanding-of-metalogical-proofs%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

flock() on closed filehandle LOCK_FILE at /usr/bin/apt-mirror

Image
0 I recently upgraded an Ubuntu 16.04 virtual machine to 18.04. I regularly use this VM to run apt-mirror at school on their high-speed internet, then rsync these files to my rack-mount server at home for updating multiple computers at home without wasting the tiny amount of bandwidth I have there. Since updating I can't get apt-mirror to run on my VM. It keeps giving the error: flock() on closed filehandle LOCK_FILE at /usr/bin/apt-mirror line 214 immediately followed by: apt-mirror is already running, exiting at /usr/bin/apt-mirror line 217 apt-mirror is NOT running, and does not have a cron job. I've tried rebooting, and even looked for the old-style lockfile to delete, but I guess that method is no longer used. Is there some way to force unlock this so I can run apt-mirror? UPDATE: So... I f...
Read more

Mangá

Image
  Nota:  Não confundir com Manga. Mangás e Animes Mangá Mangaká • Tankōbon Film comic La nouvelle manga Mangá original em inglês Anime História Animação influenciada por animes • Filler • OVA • Seiyū Públicos Kodomo • Shōjo • Shōnen Josei • Seinen Gêneros Mahō shōjo • Mecha • Harém Ecchi • Hentai ( Yaoi • Yuri Futanari • Shotacon • Lolicon Toddlercon ) Termos Bishōjo • Chibi • Fan service Gaiden • Kawaii • Kaitō • Light novel Mahō shōnen • Moe (antropomorfismo • Kemonomimi Nekomimi ) • Super deformed Omake • Tsundere • Yonkoma Listas Mangás • Animes • Ecchi • Mangaka • Estúdios • Revistas Fãs ( otaku ) Anime Music Video Convenções • Cosplay Dōjinshi • Fansub • Fandub • Fujoshi OS-tan • Scanlation Portal de Anime e mangá v d e O mangá (português brasileiro) ou manga (português europeu) [ 1 ] (em japonês: 漫画 , manga ? , lit. “história em quadrinhos”) , é a ...
Read more

Eduardo VII do Reino Unido

Image
Eduardo VII Rei do Reino Unido da Grã-Bretanha e Irlanda e dos Domínios Britânicos de Além-mar Imperador da Índia Rei do Reino Unido e Imperador da Índia Reinado 22 de janeiro de 1901 a 6 de maio de 1910 Coroação 9 de agosto de 1902 Delhi Durbar 1 de janeiro de 1903 Predecessora Vitória Sucessor Jorge V   Esposa Alexandra da Dinamarca Descendência Alberto Vitor, Duque de Clarence e Avondale Jorge V do Reino Unido Luísa, Princesa Real Vitória de Gales Maud de Gales Alexandre João de Gales Casa Saxe-Coburgo-Gota Nome completo Alberto Eduardo Nascimento 9 de novembro de 1841   Palácio de Buckingham, Londres, Reino Unido Morte 6 de maio de 1910 (68 anos)   Palácio de Buckingham, Londres, Reino Unido Enterro Capela de São Jorge, Windsor, Berkshire, Reino Unido 20 de maio de 1910 Pai Alberto de Saxe-Coburgo-Gota Mãe Vitória do Reino Unido Assinatura ...
Read more