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
    4 hours ago






  • 2




    $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    4 hours 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
    4 hours ago






  • 2




    $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    4 hours 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 4 hours ago









Keefer RowanKeefer Rowan

1839




1839












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






  • 2




    $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    4 hours ago




















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






  • 2




    $begingroup$
    The short answer is "formalize the metatheory"
    $endgroup$
    – Carl Mummert
    4 hours ago


















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




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




2




2




$begingroup$
The short answer is "formalize the metatheory"
$endgroup$
– Carl Mummert
4 hours ago






$begingroup$
The short answer is "formalize the metatheory"
$endgroup$
– Carl Mummert
4 hours ago












1 Answer
1






active

oldest

votes


















6












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









  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago








  • 1




    $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
    3 hours ago






  • 1




    $begingroup$
    Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
    $endgroup$
    – spaceisdarkgreen
    2 hours 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









6












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









  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago








  • 1




    $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
    3 hours ago






  • 1




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
















6












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









  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago








  • 1




    $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
    3 hours ago






  • 1




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














6












6








6





$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 4 hours ago

























answered 4 hours ago









Carl MummertCarl Mummert

66.7k7132248




66.7k7132248








  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago








  • 1




    $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
    3 hours ago






  • 1




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














  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago






  • 1




    $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
    4 hours ago








  • 1




    $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
    3 hours ago






  • 1




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








1




1




$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
4 hours 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
4 hours ago




1




1




$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
4 hours 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
4 hours ago




1




1




$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
4 hours 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
4 hours ago






1




1




$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
3 hours 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
3 hours ago




1




1




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




$begingroup$
Also, out of curiosity, why is $Pi_2$ considered the boundary for finitism? I would have thought $Pi_1$.
$endgroup$
– spaceisdarkgreen
2 hours 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

How to label and detect the document text images

Image
1 $begingroup$ This is what I mean as document text image: I want to label the texts in image as separate blocks and my model should detect these labels as classes. NOTE: This is how the end result should be like: The labels like Block 1, Block 2, Block 3,.. should be Logo, Title, Date,.. Others, etc. Work done: First approach : I tried to implement this method via Object Detection, it didn't work. It didn't even detect any text. Second approach : Then I tried it using PixelLink. As this model is build for scene text detection, it detected each and every text in the image. But this method can detect multiple lines of text if the threshold values are increased. But I have no idea how do I add labels to the text blocks. PIXEL_CLS_WEIGHT_all_ones = 'PIXEL_CLS_WEIGHT_all_ones' PIXEL_C...
Read more

Vallis Paradisi

Image
Coordinata: .mw-parser-output .geo-default,.mw-parser-output .geo-dms,.mw-parser-output .geo-dec{display:inline}.mw-parser-output .geo-nondefault,.mw-parser-output .geo-multi-punct{display:none}.mw-parser-output .longitude,.mw-parser-output .latitude{white-space:nowrap} 33°03′S 71°37′W  /  33.05°S 71.617°W  / -33.05; -71.617 Vallis Paradisi Res apud Vicidata repertae: Civitas : Chilia Numerus incolarum : 296 655 Zona horaria : UTC-4 Situs interretialis Nomen officiale : Valparaíso Gubernium Consilium : municipal council of Valparaíso Geographia Superficies : 401 600 000 Metrum quadratum Coniunctiones urbium Urbes gemellae : Ovetum , Badalona , Santa Fe , Ora longa , Sciamhaevum , Quantunia , Callao , Bat Yam , Melaka , Novorossiysk , Busan , Corduba , Odessa , Rosario , Malacca , Barcino , Soteropolis , Franciscopolis (California) , Guanajuato, Silao Tabula aut despectus Despectus in portum sinumque et urbem Vallis Paradisi Vallis Para...
Read more

Tabula Rosettana

Image
Tabula multilinguis Rosettana in Museo Britannico ostenditur. Tabula Rosettana, [1] etiam titulo OGIS 90 agnita, est stela decreto de rebus sacris in Aegypto anno 196 a.C.n. lato inscripta. Tabula iuxta Rosettam Aegypti, urbem in delta Nili et ad oram maris Mediterranei iacentem, anno 1799 a milite Francico reperta est. Inventio stelae, linguis duabus scripturisque tribus inscriptae, eruditis Instituti Aegypti statim nuntiata est; ibi enim iussu imperatoris Napoleonis eruditi omnium scientiarum (sub aegide Commissionis Scientiarum et Artium) properaverant cum expeditione Francica. Qua a Britannis mox debellata, tabula Rosettana Londinium missa hodie apud Museum Britannicum iacet. Textus Graecus cito lectus interpretationi textuum Aegyptiorum (in formis hieroglyphica et demotica expressorum) gradatim adiuvit. Denique textum plene interpretatus est Ioannes Franciscus Champollion. Ab opere eruditorum cumulativo coepit hodiernus scripturae hieroglyphicae linguaeque Aegyptiae a...
Read more