Substitutability in First-Order Logic











up vote
0
down vote

favorite












Here is a definition for substitutability found in a PDF of logic notes by Eric Pacuit:



enter image description here



I am more concerned with the part of the definition squared in red. My question is: Given $(forall y) psi$, does this mean that, since $y$ does not occur free in $(forall y) psi$, is $tau$ substitutable for $y$ in $(forall y) psi$?










share|cite|improve this question


















  • 1




    Yes, because the term substitutable means that performing the operation we "cause no troubles". In that case, the operation is allowed simply because it does not change the original formula.
    – Mauro ALLEGRANZA
    Nov 18 at 12:49










  • @MauroALLEGRANZA I found another definition for substitutability from the textbook by Arindama Singh: $y$ is free for $x$ in $phi$ iff $x$ does not occur free within the scope of any $forall y$ or $exists y$. Is the negation: $y$ is not free for $x$ in $phi$ iff $x$ occurs free within the scope of any $forall y$ or $exists y$?
    – numericalorange
    Nov 19 at 4:53















up vote
0
down vote

favorite












Here is a definition for substitutability found in a PDF of logic notes by Eric Pacuit:



enter image description here



I am more concerned with the part of the definition squared in red. My question is: Given $(forall y) psi$, does this mean that, since $y$ does not occur free in $(forall y) psi$, is $tau$ substitutable for $y$ in $(forall y) psi$?










share|cite|improve this question


















  • 1




    Yes, because the term substitutable means that performing the operation we "cause no troubles". In that case, the operation is allowed simply because it does not change the original formula.
    – Mauro ALLEGRANZA
    Nov 18 at 12:49










  • @MauroALLEGRANZA I found another definition for substitutability from the textbook by Arindama Singh: $y$ is free for $x$ in $phi$ iff $x$ does not occur free within the scope of any $forall y$ or $exists y$. Is the negation: $y$ is not free for $x$ in $phi$ iff $x$ occurs free within the scope of any $forall y$ or $exists y$?
    – numericalorange
    Nov 19 at 4:53













up vote
0
down vote

favorite









up vote
0
down vote

favorite











Here is a definition for substitutability found in a PDF of logic notes by Eric Pacuit:



enter image description here



I am more concerned with the part of the definition squared in red. My question is: Given $(forall y) psi$, does this mean that, since $y$ does not occur free in $(forall y) psi$, is $tau$ substitutable for $y$ in $(forall y) psi$?










share|cite|improve this question













Here is a definition for substitutability found in a PDF of logic notes by Eric Pacuit:



enter image description here



I am more concerned with the part of the definition squared in red. My question is: Given $(forall y) psi$, does this mean that, since $y$ does not occur free in $(forall y) psi$, is $tau$ substitutable for $y$ in $(forall y) psi$?







logic first-order-logic substitution






share|cite|improve this question













share|cite|improve this question











share|cite|improve this question




share|cite|improve this question










asked Nov 18 at 4:42









numericalorange

1,619311




1,619311








  • 1




    Yes, because the term substitutable means that performing the operation we "cause no troubles". In that case, the operation is allowed simply because it does not change the original formula.
    – Mauro ALLEGRANZA
    Nov 18 at 12:49










  • @MauroALLEGRANZA I found another definition for substitutability from the textbook by Arindama Singh: $y$ is free for $x$ in $phi$ iff $x$ does not occur free within the scope of any $forall y$ or $exists y$. Is the negation: $y$ is not free for $x$ in $phi$ iff $x$ occurs free within the scope of any $forall y$ or $exists y$?
    – numericalorange
    Nov 19 at 4:53














  • 1




    Yes, because the term substitutable means that performing the operation we "cause no troubles". In that case, the operation is allowed simply because it does not change the original formula.
    – Mauro ALLEGRANZA
    Nov 18 at 12:49










  • @MauroALLEGRANZA I found another definition for substitutability from the textbook by Arindama Singh: $y$ is free for $x$ in $phi$ iff $x$ does not occur free within the scope of any $forall y$ or $exists y$. Is the negation: $y$ is not free for $x$ in $phi$ iff $x$ occurs free within the scope of any $forall y$ or $exists y$?
    – numericalorange
    Nov 19 at 4:53








1




1




Yes, because the term substitutable means that performing the operation we "cause no troubles". In that case, the operation is allowed simply because it does not change the original formula.
– Mauro ALLEGRANZA
Nov 18 at 12:49




Yes, because the term substitutable means that performing the operation we "cause no troubles". In that case, the operation is allowed simply because it does not change the original formula.
– Mauro ALLEGRANZA
Nov 18 at 12:49












@MauroALLEGRANZA I found another definition for substitutability from the textbook by Arindama Singh: $y$ is free for $x$ in $phi$ iff $x$ does not occur free within the scope of any $forall y$ or $exists y$. Is the negation: $y$ is not free for $x$ in $phi$ iff $x$ occurs free within the scope of any $forall y$ or $exists y$?
– numericalorange
Nov 19 at 4:53




@MauroALLEGRANZA I found another definition for substitutability from the textbook by Arindama Singh: $y$ is free for $x$ in $phi$ iff $x$ does not occur free within the scope of any $forall y$ or $exists y$. Is the negation: $y$ is not free for $x$ in $phi$ iff $x$ occurs free within the scope of any $forall y$ or $exists y$?
– numericalorange
Nov 19 at 4:53










1 Answer
1






active

oldest

votes

















up vote
1
down vote



accepted










By definition, the answer is yes, $tau$ is substitutable for $y$ in $(forall y)phi$. This happens because there is nothing that to substitute and, therefore, you not change the original formula.






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',
    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%2f3003141%2fsubstitutability-in-first-order-logic%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








    up vote
    1
    down vote



    accepted










    By definition, the answer is yes, $tau$ is substitutable for $y$ in $(forall y)phi$. This happens because there is nothing that to substitute and, therefore, you not change the original formula.






    share|cite|improve this answer

























      up vote
      1
      down vote



      accepted










      By definition, the answer is yes, $tau$ is substitutable for $y$ in $(forall y)phi$. This happens because there is nothing that to substitute and, therefore, you not change the original formula.






      share|cite|improve this answer























        up vote
        1
        down vote



        accepted







        up vote
        1
        down vote



        accepted






        By definition, the answer is yes, $tau$ is substitutable for $y$ in $(forall y)phi$. This happens because there is nothing that to substitute and, therefore, you not change the original formula.






        share|cite|improve this answer












        By definition, the answer is yes, $tau$ is substitutable for $y$ in $(forall y)phi$. This happens because there is nothing that to substitute and, therefore, you not change the original formula.







        share|cite|improve this answer












        share|cite|improve this answer



        share|cite|improve this answer










        answered Nov 18 at 5:38









        Gödel

        1,351319




        1,351319






























             

            draft saved


            draft discarded



















































             


            draft saved


            draft discarded














            StackExchange.ready(
            function () {
            StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3003141%2fsubstitutability-in-first-order-logic%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

            Quarter-circle Tiles

            build a pushdown automaton that recognizes the reverse language of a given pushdown automaton?

            Mont Emei