Are results of relative consistency metatheorems?












3














Suppose that $S, T$ are two theories in the language of set theory, and suppose I prove - using relativization of concepts, for example - that $operatorname{Con}(S) rightarrow operatorname{Con}(T)$. This results seems to me, unless both theories are finite, to be a result in the metatheory, in the sense that it is impossible to prove that $mathsf{ZF} vdash operatorname{Con}(S) rightarrow operatorname{Con}(T)$. It seems this way because, given a class model $mathcal{M}$, $mathcal{M} vDash S$ is generally a statement that can't be formalized in $mathsf{ZF}$. Does this sound right?










share|cite|improve this question




















  • 2




    But the metatheory typically is weaker than ZF, not stronger...
    – Eric Wofsey
    5 hours ago










  • What does being weaker and stronger means, in this case? I guess I didn't understand your comment.
    – Nuntractatuses Amável
    5 hours ago






  • 1




    I think you are confused by my use of the term "metatheorem" in my answer to your previous question. All that term means is that you are proving a theorem about what theorems ZF can prove, rather than proving those theorems in ZF. But this "metatheorem" about what theorems ZF can prove is itself a theorem of ZF (or typically even a much less powerful theory like PA), just like any other mathematical reasoning.
    – Eric Wofsey
    5 hours ago










  • Suppose, for example, I code ZFC's formulas into PA - then a relative consistency result would be a theorem in PA. But it wouldn't be a theorem of ZFC, at first (unless, of course, I coded ZFC into ZFC) - and the result would be dependent on the coding method I chose. It is a metatheorem in this sense.
    – Nuntractatuses Amável
    5 hours ago






  • 3




    OK, but you can code ZFC into ZFC if you prefer. This is easier than coding ZFC into PA, since ZFC is so much more powerful and expressive than PA.
    – Eric Wofsey
    5 hours ago
















3














Suppose that $S, T$ are two theories in the language of set theory, and suppose I prove - using relativization of concepts, for example - that $operatorname{Con}(S) rightarrow operatorname{Con}(T)$. This results seems to me, unless both theories are finite, to be a result in the metatheory, in the sense that it is impossible to prove that $mathsf{ZF} vdash operatorname{Con}(S) rightarrow operatorname{Con}(T)$. It seems this way because, given a class model $mathcal{M}$, $mathcal{M} vDash S$ is generally a statement that can't be formalized in $mathsf{ZF}$. Does this sound right?










share|cite|improve this question




















  • 2




    But the metatheory typically is weaker than ZF, not stronger...
    – Eric Wofsey
    5 hours ago










  • What does being weaker and stronger means, in this case? I guess I didn't understand your comment.
    – Nuntractatuses Amável
    5 hours ago






  • 1




    I think you are confused by my use of the term "metatheorem" in my answer to your previous question. All that term means is that you are proving a theorem about what theorems ZF can prove, rather than proving those theorems in ZF. But this "metatheorem" about what theorems ZF can prove is itself a theorem of ZF (or typically even a much less powerful theory like PA), just like any other mathematical reasoning.
    – Eric Wofsey
    5 hours ago










  • Suppose, for example, I code ZFC's formulas into PA - then a relative consistency result would be a theorem in PA. But it wouldn't be a theorem of ZFC, at first (unless, of course, I coded ZFC into ZFC) - and the result would be dependent on the coding method I chose. It is a metatheorem in this sense.
    – Nuntractatuses Amável
    5 hours ago






  • 3




    OK, but you can code ZFC into ZFC if you prefer. This is easier than coding ZFC into PA, since ZFC is so much more powerful and expressive than PA.
    – Eric Wofsey
    5 hours ago














3












3








3







Suppose that $S, T$ are two theories in the language of set theory, and suppose I prove - using relativization of concepts, for example - that $operatorname{Con}(S) rightarrow operatorname{Con}(T)$. This results seems to me, unless both theories are finite, to be a result in the metatheory, in the sense that it is impossible to prove that $mathsf{ZF} vdash operatorname{Con}(S) rightarrow operatorname{Con}(T)$. It seems this way because, given a class model $mathcal{M}$, $mathcal{M} vDash S$ is generally a statement that can't be formalized in $mathsf{ZF}$. Does this sound right?










share|cite|improve this question















Suppose that $S, T$ are two theories in the language of set theory, and suppose I prove - using relativization of concepts, for example - that $operatorname{Con}(S) rightarrow operatorname{Con}(T)$. This results seems to me, unless both theories are finite, to be a result in the metatheory, in the sense that it is impossible to prove that $mathsf{ZF} vdash operatorname{Con}(S) rightarrow operatorname{Con}(T)$. It seems this way because, given a class model $mathcal{M}$, $mathcal{M} vDash S$ is generally a statement that can't be formalized in $mathsf{ZF}$. Does this sound right?







logic set-theory meta-math






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited 1 hour ago









Asaf Karagila

301k32423755




301k32423755










asked 6 hours ago









Nuntractatuses Amável

60412




60412








  • 2




    But the metatheory typically is weaker than ZF, not stronger...
    – Eric Wofsey
    5 hours ago










  • What does being weaker and stronger means, in this case? I guess I didn't understand your comment.
    – Nuntractatuses Amável
    5 hours ago






  • 1




    I think you are confused by my use of the term "metatheorem" in my answer to your previous question. All that term means is that you are proving a theorem about what theorems ZF can prove, rather than proving those theorems in ZF. But this "metatheorem" about what theorems ZF can prove is itself a theorem of ZF (or typically even a much less powerful theory like PA), just like any other mathematical reasoning.
    – Eric Wofsey
    5 hours ago










  • Suppose, for example, I code ZFC's formulas into PA - then a relative consistency result would be a theorem in PA. But it wouldn't be a theorem of ZFC, at first (unless, of course, I coded ZFC into ZFC) - and the result would be dependent on the coding method I chose. It is a metatheorem in this sense.
    – Nuntractatuses Amável
    5 hours ago






  • 3




    OK, but you can code ZFC into ZFC if you prefer. This is easier than coding ZFC into PA, since ZFC is so much more powerful and expressive than PA.
    – Eric Wofsey
    5 hours ago














  • 2




    But the metatheory typically is weaker than ZF, not stronger...
    – Eric Wofsey
    5 hours ago










  • What does being weaker and stronger means, in this case? I guess I didn't understand your comment.
    – Nuntractatuses Amável
    5 hours ago






  • 1




    I think you are confused by my use of the term "metatheorem" in my answer to your previous question. All that term means is that you are proving a theorem about what theorems ZF can prove, rather than proving those theorems in ZF. But this "metatheorem" about what theorems ZF can prove is itself a theorem of ZF (or typically even a much less powerful theory like PA), just like any other mathematical reasoning.
    – Eric Wofsey
    5 hours ago










  • Suppose, for example, I code ZFC's formulas into PA - then a relative consistency result would be a theorem in PA. But it wouldn't be a theorem of ZFC, at first (unless, of course, I coded ZFC into ZFC) - and the result would be dependent on the coding method I chose. It is a metatheorem in this sense.
    – Nuntractatuses Amável
    5 hours ago






  • 3




    OK, but you can code ZFC into ZFC if you prefer. This is easier than coding ZFC into PA, since ZFC is so much more powerful and expressive than PA.
    – Eric Wofsey
    5 hours ago








2




2




But the metatheory typically is weaker than ZF, not stronger...
– Eric Wofsey
5 hours ago




But the metatheory typically is weaker than ZF, not stronger...
– Eric Wofsey
5 hours ago












What does being weaker and stronger means, in this case? I guess I didn't understand your comment.
– Nuntractatuses Amável
5 hours ago




What does being weaker and stronger means, in this case? I guess I didn't understand your comment.
– Nuntractatuses Amável
5 hours ago




1




1




I think you are confused by my use of the term "metatheorem" in my answer to your previous question. All that term means is that you are proving a theorem about what theorems ZF can prove, rather than proving those theorems in ZF. But this "metatheorem" about what theorems ZF can prove is itself a theorem of ZF (or typically even a much less powerful theory like PA), just like any other mathematical reasoning.
– Eric Wofsey
5 hours ago




I think you are confused by my use of the term "metatheorem" in my answer to your previous question. All that term means is that you are proving a theorem about what theorems ZF can prove, rather than proving those theorems in ZF. But this "metatheorem" about what theorems ZF can prove is itself a theorem of ZF (or typically even a much less powerful theory like PA), just like any other mathematical reasoning.
– Eric Wofsey
5 hours ago












Suppose, for example, I code ZFC's formulas into PA - then a relative consistency result would be a theorem in PA. But it wouldn't be a theorem of ZFC, at first (unless, of course, I coded ZFC into ZFC) - and the result would be dependent on the coding method I chose. It is a metatheorem in this sense.
– Nuntractatuses Amável
5 hours ago




Suppose, for example, I code ZFC's formulas into PA - then a relative consistency result would be a theorem in PA. But it wouldn't be a theorem of ZFC, at first (unless, of course, I coded ZFC into ZFC) - and the result would be dependent on the coding method I chose. It is a metatheorem in this sense.
– Nuntractatuses Amável
5 hours ago




3




3




OK, but you can code ZFC into ZFC if you prefer. This is easier than coding ZFC into PA, since ZFC is so much more powerful and expressive than PA.
– Eric Wofsey
5 hours ago




OK, but you can code ZFC into ZFC if you prefer. This is easier than coding ZFC into PA, since ZFC is so much more powerful and expressive than PA.
– Eric Wofsey
5 hours ago










2 Answers
2






active

oldest

votes


















2














Yes. Consistency results are meta-theorems. They are not about implications of statements in the language, but rather about the properties of theories, which are objects of the meta-theory.



Now, in the comments you express some confusion about the meta-theory being $sf PA$ or $sf ZF$ or something else. In practice this does not matter. If you can interpret a theory $T$ in a theory $S$, then all proofs from $T$ can be translated as well. In particular, $sf PA$ can be interpreted in $sf ZF$, so whatever you can do in $sf PA$ as a meta-theory, you can in fact do in $sf ZF$. Actually, $sf PA$ is far too strong for most of the things you want a meta-theory to do, and $sf PRA$ (Primitive-Recursive Arithmetic) is actually enough.



But $sf ZF$ offers us more. It offers us models and semantics, and Gödel's completeness theorem which tells us that $operatorname{Con}(S)$ holds if and only if $S$ has a model. So it lets us play with objects, rather than with formulas and proofs. Because usually playing with objects is easier than playing with syntax. The important part is that $sf ZF$ lets us take all the results we obtained semantically, and convert them back into something that was actually proved from $sf PA$ or some subtheory thereof.



Of course, when you use $sf ZF$ as your meta-theory for itself, you are not talking about class models, you are talking about set models. We go one step further down the rabbit hole. And that's fine.






share|cite|improve this answer





























    2














    Yes, they are metatheorems in the sense that they are theorems about formal systems. But notice there is a fuzzy line as to what to call a metatheorem. If $phi$ is a sentence in the language of set theory and $phi$ is a theorem of ZFC, then the (true) statement "$mathsf{ZFC}vdash phi$" is a metatheorem that we prove in the metatheory, typically by producing and verifying a formal ZFC proof (well, what we actually do is give a natural language mathematical argument that is supposed to more-or-less clearly map to a formal ZFC proof). Typically when theorems are called out specifically as metatheorems, they are more complicated statements than $"mathsf{ZFC}vdash phi$," so that it's important to take notice that we are doing something less trivial in the metatheory than simply verifying a proof.



    $mathrm{Con}(S)to mathrm{Con}(T)$ is one of these more complicated statements, where we actually have two distinct theories, and we're saying that if we can prove a contradiction from $T$ then we can from $S$ as well.



    So yes, it's in the metatheory, but what's the metatheory? It's just the language we're using to study and prove things about the formal systems in question. We do this in natural language typically, but it can often be of interest to formalize the metatheory and ask questions like which axioms are needed to prove a given result about ZFC. To do this we need to code the ideas of formulas and proofs into some formal system, i.e. Godel encoding. (I won't say anything more on this since I see it was discussed in the comments.) Nothing precludes us from using ZFC to formalize the metatheory, although it is typically overkill for studying proofs in formal systems and weak theories of arithmetic suffice.



    In particular, as Eric says in the comments, we can typically prove something like $mathrm{Con}(S)to mathrm{Con}(T)$ in a system much weaker than ZF, so we can certainly prove it in ZF. Note that this is framable as an arithmetic statements about certain proof numbers existing, and ZF can talk about arithmetic through its natural numbers, so you can very readily express the statement in both systems (and thanks to ZF's greater expressiveness you have other more natural encoding options there too rather than just using numbers).



    You are correct that $mathcal Mmodels S$ and more generally the satisfaction relation
    $mathcal Mmodels phi$ cannot be expressed in ZFC for $M$ a proper class. I assume you have in mind demonstrating the premise of a theorem like "If for all $phiin S,$ ZFC can prove $mathcal Mmodels phi$ for some $mathcal M$ (which is a proper class in this instance) then $mathrm{Con}(mathsf{ZFC}) to mathrm{Con}(S)$". But note the subtlety here... we aren't asked to show $mathcal Mmodels phi,$ we're asked to show that ZFC proves this. In other words that it holds in all (set!) models of ZFC. And the relativization of proper class to a set model is of course a set.






    share|cite|improve this answer





















      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%2f3052631%2fare-results-of-relative-consistency-metatheorems%23new-answer', 'question_page');
      }
      );

      Post as a guest















      Required, but never shown

























      2 Answers
      2






      active

      oldest

      votes








      2 Answers
      2






      active

      oldest

      votes









      active

      oldest

      votes






      active

      oldest

      votes









      2














      Yes. Consistency results are meta-theorems. They are not about implications of statements in the language, but rather about the properties of theories, which are objects of the meta-theory.



      Now, in the comments you express some confusion about the meta-theory being $sf PA$ or $sf ZF$ or something else. In practice this does not matter. If you can interpret a theory $T$ in a theory $S$, then all proofs from $T$ can be translated as well. In particular, $sf PA$ can be interpreted in $sf ZF$, so whatever you can do in $sf PA$ as a meta-theory, you can in fact do in $sf ZF$. Actually, $sf PA$ is far too strong for most of the things you want a meta-theory to do, and $sf PRA$ (Primitive-Recursive Arithmetic) is actually enough.



      But $sf ZF$ offers us more. It offers us models and semantics, and Gödel's completeness theorem which tells us that $operatorname{Con}(S)$ holds if and only if $S$ has a model. So it lets us play with objects, rather than with formulas and proofs. Because usually playing with objects is easier than playing with syntax. The important part is that $sf ZF$ lets us take all the results we obtained semantically, and convert them back into something that was actually proved from $sf PA$ or some subtheory thereof.



      Of course, when you use $sf ZF$ as your meta-theory for itself, you are not talking about class models, you are talking about set models. We go one step further down the rabbit hole. And that's fine.






      share|cite|improve this answer


























        2














        Yes. Consistency results are meta-theorems. They are not about implications of statements in the language, but rather about the properties of theories, which are objects of the meta-theory.



        Now, in the comments you express some confusion about the meta-theory being $sf PA$ or $sf ZF$ or something else. In practice this does not matter. If you can interpret a theory $T$ in a theory $S$, then all proofs from $T$ can be translated as well. In particular, $sf PA$ can be interpreted in $sf ZF$, so whatever you can do in $sf PA$ as a meta-theory, you can in fact do in $sf ZF$. Actually, $sf PA$ is far too strong for most of the things you want a meta-theory to do, and $sf PRA$ (Primitive-Recursive Arithmetic) is actually enough.



        But $sf ZF$ offers us more. It offers us models and semantics, and Gödel's completeness theorem which tells us that $operatorname{Con}(S)$ holds if and only if $S$ has a model. So it lets us play with objects, rather than with formulas and proofs. Because usually playing with objects is easier than playing with syntax. The important part is that $sf ZF$ lets us take all the results we obtained semantically, and convert them back into something that was actually proved from $sf PA$ or some subtheory thereof.



        Of course, when you use $sf ZF$ as your meta-theory for itself, you are not talking about class models, you are talking about set models. We go one step further down the rabbit hole. And that's fine.






        share|cite|improve this answer
























          2












          2








          2






          Yes. Consistency results are meta-theorems. They are not about implications of statements in the language, but rather about the properties of theories, which are objects of the meta-theory.



          Now, in the comments you express some confusion about the meta-theory being $sf PA$ or $sf ZF$ or something else. In practice this does not matter. If you can interpret a theory $T$ in a theory $S$, then all proofs from $T$ can be translated as well. In particular, $sf PA$ can be interpreted in $sf ZF$, so whatever you can do in $sf PA$ as a meta-theory, you can in fact do in $sf ZF$. Actually, $sf PA$ is far too strong for most of the things you want a meta-theory to do, and $sf PRA$ (Primitive-Recursive Arithmetic) is actually enough.



          But $sf ZF$ offers us more. It offers us models and semantics, and Gödel's completeness theorem which tells us that $operatorname{Con}(S)$ holds if and only if $S$ has a model. So it lets us play with objects, rather than with formulas and proofs. Because usually playing with objects is easier than playing with syntax. The important part is that $sf ZF$ lets us take all the results we obtained semantically, and convert them back into something that was actually proved from $sf PA$ or some subtheory thereof.



          Of course, when you use $sf ZF$ as your meta-theory for itself, you are not talking about class models, you are talking about set models. We go one step further down the rabbit hole. And that's fine.






          share|cite|improve this answer












          Yes. Consistency results are meta-theorems. They are not about implications of statements in the language, but rather about the properties of theories, which are objects of the meta-theory.



          Now, in the comments you express some confusion about the meta-theory being $sf PA$ or $sf ZF$ or something else. In practice this does not matter. If you can interpret a theory $T$ in a theory $S$, then all proofs from $T$ can be translated as well. In particular, $sf PA$ can be interpreted in $sf ZF$, so whatever you can do in $sf PA$ as a meta-theory, you can in fact do in $sf ZF$. Actually, $sf PA$ is far too strong for most of the things you want a meta-theory to do, and $sf PRA$ (Primitive-Recursive Arithmetic) is actually enough.



          But $sf ZF$ offers us more. It offers us models and semantics, and Gödel's completeness theorem which tells us that $operatorname{Con}(S)$ holds if and only if $S$ has a model. So it lets us play with objects, rather than with formulas and proofs. Because usually playing with objects is easier than playing with syntax. The important part is that $sf ZF$ lets us take all the results we obtained semantically, and convert them back into something that was actually proved from $sf PA$ or some subtheory thereof.



          Of course, when you use $sf ZF$ as your meta-theory for itself, you are not talking about class models, you are talking about set models. We go one step further down the rabbit hole. And that's fine.







          share|cite|improve this answer












          share|cite|improve this answer



          share|cite|improve this answer










          answered 1 hour ago









          Asaf Karagila

          301k32423755




          301k32423755























              2














              Yes, they are metatheorems in the sense that they are theorems about formal systems. But notice there is a fuzzy line as to what to call a metatheorem. If $phi$ is a sentence in the language of set theory and $phi$ is a theorem of ZFC, then the (true) statement "$mathsf{ZFC}vdash phi$" is a metatheorem that we prove in the metatheory, typically by producing and verifying a formal ZFC proof (well, what we actually do is give a natural language mathematical argument that is supposed to more-or-less clearly map to a formal ZFC proof). Typically when theorems are called out specifically as metatheorems, they are more complicated statements than $"mathsf{ZFC}vdash phi$," so that it's important to take notice that we are doing something less trivial in the metatheory than simply verifying a proof.



              $mathrm{Con}(S)to mathrm{Con}(T)$ is one of these more complicated statements, where we actually have two distinct theories, and we're saying that if we can prove a contradiction from $T$ then we can from $S$ as well.



              So yes, it's in the metatheory, but what's the metatheory? It's just the language we're using to study and prove things about the formal systems in question. We do this in natural language typically, but it can often be of interest to formalize the metatheory and ask questions like which axioms are needed to prove a given result about ZFC. To do this we need to code the ideas of formulas and proofs into some formal system, i.e. Godel encoding. (I won't say anything more on this since I see it was discussed in the comments.) Nothing precludes us from using ZFC to formalize the metatheory, although it is typically overkill for studying proofs in formal systems and weak theories of arithmetic suffice.



              In particular, as Eric says in the comments, we can typically prove something like $mathrm{Con}(S)to mathrm{Con}(T)$ in a system much weaker than ZF, so we can certainly prove it in ZF. Note that this is framable as an arithmetic statements about certain proof numbers existing, and ZF can talk about arithmetic through its natural numbers, so you can very readily express the statement in both systems (and thanks to ZF's greater expressiveness you have other more natural encoding options there too rather than just using numbers).



              You are correct that $mathcal Mmodels S$ and more generally the satisfaction relation
              $mathcal Mmodels phi$ cannot be expressed in ZFC for $M$ a proper class. I assume you have in mind demonstrating the premise of a theorem like "If for all $phiin S,$ ZFC can prove $mathcal Mmodels phi$ for some $mathcal M$ (which is a proper class in this instance) then $mathrm{Con}(mathsf{ZFC}) to mathrm{Con}(S)$". But note the subtlety here... we aren't asked to show $mathcal Mmodels phi,$ we're asked to show that ZFC proves this. In other words that it holds in all (set!) models of ZFC. And the relativization of proper class to a set model is of course a set.






              share|cite|improve this answer


























                2














                Yes, they are metatheorems in the sense that they are theorems about formal systems. But notice there is a fuzzy line as to what to call a metatheorem. If $phi$ is a sentence in the language of set theory and $phi$ is a theorem of ZFC, then the (true) statement "$mathsf{ZFC}vdash phi$" is a metatheorem that we prove in the metatheory, typically by producing and verifying a formal ZFC proof (well, what we actually do is give a natural language mathematical argument that is supposed to more-or-less clearly map to a formal ZFC proof). Typically when theorems are called out specifically as metatheorems, they are more complicated statements than $"mathsf{ZFC}vdash phi$," so that it's important to take notice that we are doing something less trivial in the metatheory than simply verifying a proof.



                $mathrm{Con}(S)to mathrm{Con}(T)$ is one of these more complicated statements, where we actually have two distinct theories, and we're saying that if we can prove a contradiction from $T$ then we can from $S$ as well.



                So yes, it's in the metatheory, but what's the metatheory? It's just the language we're using to study and prove things about the formal systems in question. We do this in natural language typically, but it can often be of interest to formalize the metatheory and ask questions like which axioms are needed to prove a given result about ZFC. To do this we need to code the ideas of formulas and proofs into some formal system, i.e. Godel encoding. (I won't say anything more on this since I see it was discussed in the comments.) Nothing precludes us from using ZFC to formalize the metatheory, although it is typically overkill for studying proofs in formal systems and weak theories of arithmetic suffice.



                In particular, as Eric says in the comments, we can typically prove something like $mathrm{Con}(S)to mathrm{Con}(T)$ in a system much weaker than ZF, so we can certainly prove it in ZF. Note that this is framable as an arithmetic statements about certain proof numbers existing, and ZF can talk about arithmetic through its natural numbers, so you can very readily express the statement in both systems (and thanks to ZF's greater expressiveness you have other more natural encoding options there too rather than just using numbers).



                You are correct that $mathcal Mmodels S$ and more generally the satisfaction relation
                $mathcal Mmodels phi$ cannot be expressed in ZFC for $M$ a proper class. I assume you have in mind demonstrating the premise of a theorem like "If for all $phiin S,$ ZFC can prove $mathcal Mmodels phi$ for some $mathcal M$ (which is a proper class in this instance) then $mathrm{Con}(mathsf{ZFC}) to mathrm{Con}(S)$". But note the subtlety here... we aren't asked to show $mathcal Mmodels phi,$ we're asked to show that ZFC proves this. In other words that it holds in all (set!) models of ZFC. And the relativization of proper class to a set model is of course a set.






                share|cite|improve this answer
























                  2












                  2








                  2






                  Yes, they are metatheorems in the sense that they are theorems about formal systems. But notice there is a fuzzy line as to what to call a metatheorem. If $phi$ is a sentence in the language of set theory and $phi$ is a theorem of ZFC, then the (true) statement "$mathsf{ZFC}vdash phi$" is a metatheorem that we prove in the metatheory, typically by producing and verifying a formal ZFC proof (well, what we actually do is give a natural language mathematical argument that is supposed to more-or-less clearly map to a formal ZFC proof). Typically when theorems are called out specifically as metatheorems, they are more complicated statements than $"mathsf{ZFC}vdash phi$," so that it's important to take notice that we are doing something less trivial in the metatheory than simply verifying a proof.



                  $mathrm{Con}(S)to mathrm{Con}(T)$ is one of these more complicated statements, where we actually have two distinct theories, and we're saying that if we can prove a contradiction from $T$ then we can from $S$ as well.



                  So yes, it's in the metatheory, but what's the metatheory? It's just the language we're using to study and prove things about the formal systems in question. We do this in natural language typically, but it can often be of interest to formalize the metatheory and ask questions like which axioms are needed to prove a given result about ZFC. To do this we need to code the ideas of formulas and proofs into some formal system, i.e. Godel encoding. (I won't say anything more on this since I see it was discussed in the comments.) Nothing precludes us from using ZFC to formalize the metatheory, although it is typically overkill for studying proofs in formal systems and weak theories of arithmetic suffice.



                  In particular, as Eric says in the comments, we can typically prove something like $mathrm{Con}(S)to mathrm{Con}(T)$ in a system much weaker than ZF, so we can certainly prove it in ZF. Note that this is framable as an arithmetic statements about certain proof numbers existing, and ZF can talk about arithmetic through its natural numbers, so you can very readily express the statement in both systems (and thanks to ZF's greater expressiveness you have other more natural encoding options there too rather than just using numbers).



                  You are correct that $mathcal Mmodels S$ and more generally the satisfaction relation
                  $mathcal Mmodels phi$ cannot be expressed in ZFC for $M$ a proper class. I assume you have in mind demonstrating the premise of a theorem like "If for all $phiin S,$ ZFC can prove $mathcal Mmodels phi$ for some $mathcal M$ (which is a proper class in this instance) then $mathrm{Con}(mathsf{ZFC}) to mathrm{Con}(S)$". But note the subtlety here... we aren't asked to show $mathcal Mmodels phi,$ we're asked to show that ZFC proves this. In other words that it holds in all (set!) models of ZFC. And the relativization of proper class to a set model is of course a set.






                  share|cite|improve this answer












                  Yes, they are metatheorems in the sense that they are theorems about formal systems. But notice there is a fuzzy line as to what to call a metatheorem. If $phi$ is a sentence in the language of set theory and $phi$ is a theorem of ZFC, then the (true) statement "$mathsf{ZFC}vdash phi$" is a metatheorem that we prove in the metatheory, typically by producing and verifying a formal ZFC proof (well, what we actually do is give a natural language mathematical argument that is supposed to more-or-less clearly map to a formal ZFC proof). Typically when theorems are called out specifically as metatheorems, they are more complicated statements than $"mathsf{ZFC}vdash phi$," so that it's important to take notice that we are doing something less trivial in the metatheory than simply verifying a proof.



                  $mathrm{Con}(S)to mathrm{Con}(T)$ is one of these more complicated statements, where we actually have two distinct theories, and we're saying that if we can prove a contradiction from $T$ then we can from $S$ as well.



                  So yes, it's in the metatheory, but what's the metatheory? It's just the language we're using to study and prove things about the formal systems in question. We do this in natural language typically, but it can often be of interest to formalize the metatheory and ask questions like which axioms are needed to prove a given result about ZFC. To do this we need to code the ideas of formulas and proofs into some formal system, i.e. Godel encoding. (I won't say anything more on this since I see it was discussed in the comments.) Nothing precludes us from using ZFC to formalize the metatheory, although it is typically overkill for studying proofs in formal systems and weak theories of arithmetic suffice.



                  In particular, as Eric says in the comments, we can typically prove something like $mathrm{Con}(S)to mathrm{Con}(T)$ in a system much weaker than ZF, so we can certainly prove it in ZF. Note that this is framable as an arithmetic statements about certain proof numbers existing, and ZF can talk about arithmetic through its natural numbers, so you can very readily express the statement in both systems (and thanks to ZF's greater expressiveness you have other more natural encoding options there too rather than just using numbers).



                  You are correct that $mathcal Mmodels S$ and more generally the satisfaction relation
                  $mathcal Mmodels phi$ cannot be expressed in ZFC for $M$ a proper class. I assume you have in mind demonstrating the premise of a theorem like "If for all $phiin S,$ ZFC can prove $mathcal Mmodels phi$ for some $mathcal M$ (which is a proper class in this instance) then $mathrm{Con}(mathsf{ZFC}) to mathrm{Con}(S)$". But note the subtlety here... we aren't asked to show $mathcal Mmodels phi,$ we're asked to show that ZFC proves this. In other words that it holds in all (set!) models of ZFC. And the relativization of proper class to a set model is of course a set.







                  share|cite|improve this answer












                  share|cite|improve this answer



                  share|cite|improve this answer










                  answered 1 hour ago









                  spaceisdarkgreen

                  32.2k21753




                  32.2k21753






























                      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.





                      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.




                      draft saved


                      draft discarded














                      StackExchange.ready(
                      function () {
                      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3052631%2fare-results-of-relative-consistency-metatheorems%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

                      404 Error Contact Form 7 ajax form submitting

                      How to know if a Active Directory user can login interactively

                      TypeError: fit_transform() missing 1 required positional argument: 'X'