How to write a function defined by segments in a formula?












0












$begingroup$


I would like to define a function like $f(x) = 5$ if x is even, and $f(x) = 8$ if x is odd by using a first order logic formula. Is it possible? if yes, how?










share|cite|improve this question











$endgroup$

















    0












    $begingroup$


    I would like to define a function like $f(x) = 5$ if x is even, and $f(x) = 8$ if x is odd by using a first order logic formula. Is it possible? if yes, how?










    share|cite|improve this question











    $endgroup$















      0












      0








      0





      $begingroup$


      I would like to define a function like $f(x) = 5$ if x is even, and $f(x) = 8$ if x is odd by using a first order logic formula. Is it possible? if yes, how?










      share|cite|improve this question











      $endgroup$




      I would like to define a function like $f(x) = 5$ if x is even, and $f(x) = 8$ if x is odd by using a first order logic formula. Is it possible? if yes, how?







      logic arithmetic






      share|cite|improve this question















      share|cite|improve this question













      share|cite|improve this question




      share|cite|improve this question








      edited Jan 13 at 15:18









      Key Flex

      7,85261233




      7,85261233










      asked Jan 13 at 15:16









      user49413user49413

      294




      294






















          1 Answer
          1






          active

          oldest

          votes


















          2












          $begingroup$

          Is not that clear what you mean "_by defining a function....by using a first-order logic formula".



          I suppose that you meant if there is a formula in the the first-order language of arithmetic (also known as Peano Arithmetic or PA for short).



          If that is the case then you can simply rephrase you can define your function through the following functional formula



          $$varphi_f(x,y) equiv((exists z. 2z=x) rightarrow y=5) land ((forall z. 2z ne x) rightarrow y=8)$$



          Using the axioms of PA it is possible to prove that indeed
          $$forall x exists ! y varphi_f(x,y)$$
          that is $varphi_f$ is really a functional formula. Then you can say that $f(x)=y$ is a short-hand for $varphi_f(x,y)$.



          Alternatively if you are using also $mu$-recursion in your arithmetic language you can define $f$ as
          $$f(x)=mu_y varphi_f(x,y)$$
          (if you are not familiar with the formalism that means $f(x)$ is the minimal $y$ such that $varphi_f(x,y)$ holds).



          I hope this address your question.






          share|cite|improve this answer











          $endgroup$













          • $begingroup$
            Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
            $endgroup$
            – user49413
            Jan 13 at 18:08












          • $begingroup$
            @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
            $endgroup$
            – Noah Schweber
            Jan 13 at 18:45












          • $begingroup$
            Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
            $endgroup$
            – DanielV
            Jan 13 at 20:48












          • $begingroup$
            @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
            $endgroup$
            – Giorgio Mossa
            Jan 14 at 11:27










          • $begingroup$
            Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
            $endgroup$
            – Rob Arthan
            Jan 14 at 16:09













          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%2f3072096%2fhow-to-write-a-function-defined-by-segments-in-a-formula%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









          2












          $begingroup$

          Is not that clear what you mean "_by defining a function....by using a first-order logic formula".



          I suppose that you meant if there is a formula in the the first-order language of arithmetic (also known as Peano Arithmetic or PA for short).



          If that is the case then you can simply rephrase you can define your function through the following functional formula



          $$varphi_f(x,y) equiv((exists z. 2z=x) rightarrow y=5) land ((forall z. 2z ne x) rightarrow y=8)$$



          Using the axioms of PA it is possible to prove that indeed
          $$forall x exists ! y varphi_f(x,y)$$
          that is $varphi_f$ is really a functional formula. Then you can say that $f(x)=y$ is a short-hand for $varphi_f(x,y)$.



          Alternatively if you are using also $mu$-recursion in your arithmetic language you can define $f$ as
          $$f(x)=mu_y varphi_f(x,y)$$
          (if you are not familiar with the formalism that means $f(x)$ is the minimal $y$ such that $varphi_f(x,y)$ holds).



          I hope this address your question.






          share|cite|improve this answer











          $endgroup$













          • $begingroup$
            Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
            $endgroup$
            – user49413
            Jan 13 at 18:08












          • $begingroup$
            @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
            $endgroup$
            – Noah Schweber
            Jan 13 at 18:45












          • $begingroup$
            Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
            $endgroup$
            – DanielV
            Jan 13 at 20:48












          • $begingroup$
            @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
            $endgroup$
            – Giorgio Mossa
            Jan 14 at 11:27










          • $begingroup$
            Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
            $endgroup$
            – Rob Arthan
            Jan 14 at 16:09


















          2












          $begingroup$

          Is not that clear what you mean "_by defining a function....by using a first-order logic formula".



          I suppose that you meant if there is a formula in the the first-order language of arithmetic (also known as Peano Arithmetic or PA for short).



          If that is the case then you can simply rephrase you can define your function through the following functional formula



          $$varphi_f(x,y) equiv((exists z. 2z=x) rightarrow y=5) land ((forall z. 2z ne x) rightarrow y=8)$$



          Using the axioms of PA it is possible to prove that indeed
          $$forall x exists ! y varphi_f(x,y)$$
          that is $varphi_f$ is really a functional formula. Then you can say that $f(x)=y$ is a short-hand for $varphi_f(x,y)$.



          Alternatively if you are using also $mu$-recursion in your arithmetic language you can define $f$ as
          $$f(x)=mu_y varphi_f(x,y)$$
          (if you are not familiar with the formalism that means $f(x)$ is the minimal $y$ such that $varphi_f(x,y)$ holds).



          I hope this address your question.






          share|cite|improve this answer











          $endgroup$













          • $begingroup$
            Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
            $endgroup$
            – user49413
            Jan 13 at 18:08












          • $begingroup$
            @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
            $endgroup$
            – Noah Schweber
            Jan 13 at 18:45












          • $begingroup$
            Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
            $endgroup$
            – DanielV
            Jan 13 at 20:48












          • $begingroup$
            @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
            $endgroup$
            – Giorgio Mossa
            Jan 14 at 11:27










          • $begingroup$
            Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
            $endgroup$
            – Rob Arthan
            Jan 14 at 16:09
















          2












          2








          2





          $begingroup$

          Is not that clear what you mean "_by defining a function....by using a first-order logic formula".



          I suppose that you meant if there is a formula in the the first-order language of arithmetic (also known as Peano Arithmetic or PA for short).



          If that is the case then you can simply rephrase you can define your function through the following functional formula



          $$varphi_f(x,y) equiv((exists z. 2z=x) rightarrow y=5) land ((forall z. 2z ne x) rightarrow y=8)$$



          Using the axioms of PA it is possible to prove that indeed
          $$forall x exists ! y varphi_f(x,y)$$
          that is $varphi_f$ is really a functional formula. Then you can say that $f(x)=y$ is a short-hand for $varphi_f(x,y)$.



          Alternatively if you are using also $mu$-recursion in your arithmetic language you can define $f$ as
          $$f(x)=mu_y varphi_f(x,y)$$
          (if you are not familiar with the formalism that means $f(x)$ is the minimal $y$ such that $varphi_f(x,y)$ holds).



          I hope this address your question.






          share|cite|improve this answer











          $endgroup$



          Is not that clear what you mean "_by defining a function....by using a first-order logic formula".



          I suppose that you meant if there is a formula in the the first-order language of arithmetic (also known as Peano Arithmetic or PA for short).



          If that is the case then you can simply rephrase you can define your function through the following functional formula



          $$varphi_f(x,y) equiv((exists z. 2z=x) rightarrow y=5) land ((forall z. 2z ne x) rightarrow y=8)$$



          Using the axioms of PA it is possible to prove that indeed
          $$forall x exists ! y varphi_f(x,y)$$
          that is $varphi_f$ is really a functional formula. Then you can say that $f(x)=y$ is a short-hand for $varphi_f(x,y)$.



          Alternatively if you are using also $mu$-recursion in your arithmetic language you can define $f$ as
          $$f(x)=mu_y varphi_f(x,y)$$
          (if you are not familiar with the formalism that means $f(x)$ is the minimal $y$ such that $varphi_f(x,y)$ holds).



          I hope this address your question.







          share|cite|improve this answer














          share|cite|improve this answer



          share|cite|improve this answer








          edited Jan 14 at 20:40

























          answered Jan 13 at 16:53









          Giorgio MossaGiorgio Mossa

          14.1k11749




          14.1k11749












          • $begingroup$
            Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
            $endgroup$
            – user49413
            Jan 13 at 18:08












          • $begingroup$
            @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
            $endgroup$
            – Noah Schweber
            Jan 13 at 18:45












          • $begingroup$
            Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
            $endgroup$
            – DanielV
            Jan 13 at 20:48












          • $begingroup$
            @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
            $endgroup$
            – Giorgio Mossa
            Jan 14 at 11:27










          • $begingroup$
            Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
            $endgroup$
            – Rob Arthan
            Jan 14 at 16:09




















          • $begingroup$
            Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
            $endgroup$
            – user49413
            Jan 13 at 18:08












          • $begingroup$
            @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
            $endgroup$
            – Noah Schweber
            Jan 13 at 18:45












          • $begingroup$
            Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
            $endgroup$
            – DanielV
            Jan 13 at 20:48












          • $begingroup$
            @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
            $endgroup$
            – Giorgio Mossa
            Jan 14 at 11:27










          • $begingroup$
            Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
            $endgroup$
            – Rob Arthan
            Jan 14 at 16:09


















          $begingroup$
          Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
          $endgroup$
          – user49413
          Jan 13 at 18:08






          $begingroup$
          Your guess is right. Thanks for the answer. I understand your answer. But I think that μ-recursion (or restricted μ-operator) is not part of the original first-order logic. I see it in Gödel's article in 1931 in form of εx, but not in an ordinary book explaining first-order logic. My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition. If proposition can be added to the definition of a function only by μ-recursion, then a function in formula is always computable.
          $endgroup$
          – user49413
          Jan 13 at 18:08














          $begingroup$
          @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
          $endgroup$
          – Noah Schweber
          Jan 13 at 18:45






          $begingroup$
          @user49413 "My concern is in fact whether a function in first-order logic formula remains computable even when containing proposition in its definition." I'm not sure what that means, but it's certainly worth observing that not all first-order definable functions are computable. E.g. the characteristic function of the halting problem is first-order definable (in, again, $(mathbb{N};+,times$)). There is however a connection between computability-theoretic and syntactic complexity; specifically, the quantifier structure of the definition.
          $endgroup$
          – Noah Schweber
          Jan 13 at 18:45














          $begingroup$
          Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
          $endgroup$
          – DanielV
          Jan 13 at 20:48






          $begingroup$
          Since O.P. is asking specifically about computability and especially godel's techniques, it might be worth modifying the formula to be $dots (exists z < x) dots (forall z < x) dots$ , this is called "bounded quantifiers" and is what keeps the formulas directly computable.
          $endgroup$
          – DanielV
          Jan 13 at 20:48














          $begingroup$
          @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
          $endgroup$
          – Giorgio Mossa
          Jan 14 at 11:27




          $begingroup$
          @user49413 Then I guess that the only possibile definition is the one via abbreviation (i.e. you define the formula $f(x)=y$ as an abbreviation of the above mentioned formula. About your concerns on $mu$-recursion: actually you cannot replace any formula in the $mu$-recursive definition of the function but only computable ones. In this case the definition works because the formula is of the form $Sigma^0_1$, hence it is computable.
          $endgroup$
          – Giorgio Mossa
          Jan 14 at 11:27












          $begingroup$
          Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
          $endgroup$
          – Rob Arthan
          Jan 14 at 16:09






          $begingroup$
          Minor point: the bracketing in your formula for $phi_f(x,y)$ isn't right.
          $endgroup$
          – Rob Arthan
          Jan 14 at 16:09




















          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%2f3072096%2fhow-to-write-a-function-defined-by-segments-in-a-formula%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

          Mario Kart Wii

          The Binding of Isaac: Rebirth/Afterbirth

          What does “Dominus providebit” mean?