Skip to main content
MathOverflow

Return to Answer

sp
Source Link
Charles Stewart
Charles Stewart
  • 2.3k
  • 19
  • 27

Certainly, classical logic is used in metalogic. I can't think, offhand, of any cases where I think its use is necessary. The methodology of Reverse Mathematicsreverse mathematics seems to offer a suitable, constructivist framework for discussing the kind of result that Tran Chieu Minh speaks of: our weak metalogic tells us that, e.g., we need something at least as strong as König's lemma to prove completeness, and as it happens, the converse implication is also true.

I agree with the questioner that "whatever is assumed at the metalevel should not be more than whatever is being formulated at the symbolic level." The danger is that one's metalogical assumptions might be leakier than one thinks.

If you accept this, then it follows some thinksthings that some people take to be the task of the metalogic are not: in particular, it is not the purpose of the metalogic to justify the system being studied; indeed, if one can, that tells one that the metalogic may not be well fitted to the task. And, furthermore, the strength of, say, constructivist logics as metalogics provides no kind of case that mathematics should be constructivist.

Certainly, classical logic is used in metalogic. I can't think, offhand, of any cases where I think its use is necessary. The methodology of Reverse Mathematics seems to offer a suitable, constructivist framework for discussing the kind of result that Tran Chieu Minh speaks of: our weak metalogic tells us that, e.g., we need König's lemma to prove completeness, and as it happens, the converse implication is also true.

I agree with the questioner that "whatever is assumed at the metalevel should not be more than whatever is being formulated at the symbolic level." The danger is that one's metalogical assumptions might be leakier than one thinks.

If you accept this, then it follows some thinks that some people take to be the task of the metalogic are not: in particular, it is not the purpose of the metalogic to justify the system being studied; indeed, if one can, that tells one that the metalogic may not be well fitted to the task. And, furthermore, the strength of, say, constructivist logics as metalogics provides no kind of case that mathematics should be constructivist.

Certainly, classical logic is used in metalogic. I can't think, offhand, of any cases where I think its use is necessary. The methodology of reverse mathematics seems to offer a suitable, constructivist framework for discussing the kind of result that Tran Chieu Minh speaks of: our weak metalogic tells us that, e.g., we need something at least as strong as König's lemma to prove completeness, and as it happens, the converse implication is also true.

I agree with the questioner that "whatever is assumed at the metalevel should not be more than whatever is being formulated at the symbolic level." The danger is that one's metalogical assumptions might be leakier than one thinks.

If you accept this, then it follows some things that some people take to be the task of the metalogic are not: in particular, it is not the purpose of the metalogic to justify the system being studied; indeed, if one can, that tells one that the metalogic may not be well fitted to the task. And, furthermore, the strength of, say, constructivist logics as metalogics provides no kind of case that mathematics should be constructivist.

Source Link
Charles Stewart
Charles Stewart
  • 2.3k
  • 19
  • 27

Certainly, classical logic is used in metalogic. I can't think, offhand, of any cases where I think its use is necessary. The methodology of Reverse Mathematics seems to offer a suitable, constructivist framework for discussing the kind of result that Tran Chieu Minh speaks of: our weak metalogic tells us that, e.g., we need König's lemma to prove completeness, and as it happens, the converse implication is also true.

I agree with the questioner that "whatever is assumed at the metalevel should not be more than whatever is being formulated at the symbolic level." The danger is that one's metalogical assumptions might be leakier than one thinks.

If you accept this, then it follows some thinks that some people take to be the task of the metalogic are not: in particular, it is not the purpose of the metalogic to justify the system being studied; indeed, if one can, that tells one that the metalogic may not be well fitted to the task. And, furthermore, the strength of, say, constructivist logics as metalogics provides no kind of case that mathematics should be constructivist.