Loading ...
Sorry, an error occurred while loading the content.

Re: Quantifying over functions in first-order logic

Expand Messages
  • cedricstjl
    Why does it matter? I m quantifying over objects that behave exactly like FOL functions instead of quantifying directly over FOL functions. I could write a
    Message 1 of 9 , Jun 13, 2006
    • 0 Attachment
      Why does it matter? I'm quantifying over "objects that behave exactly
      like FOL functions" instead of quantifying directly over FOL functions.

      I could write a program, which takes as input a second-order logic
      sentence, does inference in FOL with the conversion from my first
      post, and translates back into second-order logic. Or are there SOL
      sentences that wouldn't be translatable?

      Thank you for your time,

      Cedric

      --- In aima-talk@yahoogroups.com, "Peter Norvig" <peter@...> wrote:
      >
      > You could do that, and that could be a way of expressing reflexivity,
      > but it wouldn't be quantifying over FOL functions -- it would be
      > quantifying over objects that you happen to call "functions" but are
      > regular objects as far as the logic is concerned.
      >
      > -Peter
      >
      > On 6/8/06, cedricstjl <cedricstjl@...> wrote:
      > > I have some difficulty seeing the difference in expressiveness between
      > > first-order logic and higher-order logics. Wikipedia (as well as AIMA,
      > > AFAICT) says that F-O logic cannot quantify over functions. But
      > > couldn't it be achieved equivalently by reifying functions and
      > > predicates? I.e.:
      > >
      > > x = fun(var)
      > >
      > > becomes
      > >
      > > x = call_function(fun, var)
      > >
      > > and then one can express reflexivity:
      > >
      > > for all fun, a, b: reflexive(fun) <=> call_function(fun, a, b) =
      > > call_function(fun, b, a)
      > >
      > > Cedric
    • Peter Norvig
      I agree that for most of what you would reasonably want to do, it wouldn t matter. But the point is that when you quantify over all functions/relations
      Message 2 of 9 , Jun 13, 2006
      • 0 Attachment
        I agree that for most of what you would reasonably want to do, it
        wouldn't matter. But the point is that when you quantify over all
        functions/relations (represented as objects), you wouldn't be
        quantifying over "call_function" nor "reflexive".

        -Peter

        On 6/13/06, cedricstjl <cedricstjl@...> wrote:
        > Why does it matter? I'm quantifying over "objects that behave exactly
        > like FOL functions" instead of quantifying directly over FOL functions.
        >
        > I could write a program, which takes as input a second-order logic
        > sentence, does inference in FOL with the conversion from my first
        > post, and translates back into second-order logic. Or are there SOL
        > sentences that wouldn't be translatable?
        >
        > Thank you for your time,
        >
        > Cedric
        >
        > --- In aima-talk@yahoogroups.com, "Peter Norvig" <peter@...> wrote:
        > >
        > > You could do that, and that could be a way of expressing reflexivity,
        > > but it wouldn't be quantifying over FOL functions -- it would be
        > > quantifying over objects that you happen to call "functions" but are
        > > regular objects as far as the logic is concerned.
        > >
        > > -Peter
        > >
        > > On 6/8/06, cedricstjl <cedricstjl@...> wrote:
        > > > I have some difficulty seeing the difference in expressiveness between
        > > > first-order logic and higher-order logics. Wikipedia (as well as AIMA,
        > > > AFAICT) says that F-O logic cannot quantify over functions. But
        > > > couldn't it be achieved equivalently by reifying functions and
        > > > predicates? I.e.:
        > > >
        > > > x = fun(var)
        > > >
        > > > becomes
        > > >
        > > > x = call_function(fun, var)
        > > >
        > > > and then one can express reflexivity:
        > > >
        > > > for all fun, a, b: reflexive(fun) <=> call_function(fun, a, b) =
        > > > call_function(fun, b, a)
        > > >
        > > > Cedric
        >
        >
        >
        >
        >
        >
        >
        >
        >
        >
        >
        > Yahoo! Groups Links
        >
        >
        >
        >
        >
        >
        >
        >
      • cedricstjl
        I don t see why one would ever want to quantify over call_function. I don t think that there is an equivalent to that in regular logic. I can quantify over
        Message 3 of 9 , Jun 14, 2006
        • 0 Attachment
          I don't see why one would ever want to quantify over call_function. I
          don't think that there is an equivalent to that in "regular" logic.

          I can quantify over reflexive by adding another level of indirection.
          reflexive(f) becomes call_function_2(reflexive, f). As long as all
          functions have a clearly defined level, it should work. Furthermore,
          using levels is, from what I've read, a common way of avoiding
          Russell's paradox in SOL. Does the "SOL is strictly more expressive
          than FOL" claim apply only to SOL without levels?

          Cedric

          --- In aima-talk@yahoogroups.com, "Peter Norvig" <peter@...> wrote:
          >
          > I agree that for most of what you would reasonably want to do, it
          > wouldn't matter. But the point is that when you quantify over all
          > functions/relations (represented as objects), you wouldn't be
          > quantifying over "call_function" nor "reflexive".
          >
          > -Peter
          >
          > On 6/13/06, cedricstjl <cedricstjl@...> wrote:
          > > Why does it matter? I'm quantifying over "objects that behave exactly
          > > like FOL functions" instead of quantifying directly over FOL
          functions.
          > >
          > > I could write a program, which takes as input a second-order logic
          > > sentence, does inference in FOL with the conversion from my first
          > > post, and translates back into second-order logic. Or are there SOL
          > > sentences that wouldn't be translatable?
          > >
          > > Thank you for your time,
          > >
          > > Cedric
          > >
          > > --- In aima-talk@yahoogroups.com, "Peter Norvig" <peter@> wrote:
          > > >
          > > > You could do that, and that could be a way of expressing
          reflexivity,
          > > > but it wouldn't be quantifying over FOL functions -- it would be
          > > > quantifying over objects that you happen to call "functions" but are
          > > > regular objects as far as the logic is concerned.
          > > >
          > > > -Peter
          > > >
          > > > On 6/8/06, cedricstjl <cedricstjl@> wrote:
          > > > > I have some difficulty seeing the difference in expressiveness
          between
          > > > > first-order logic and higher-order logics. Wikipedia (as well
          as AIMA,
          > > > > AFAICT) says that F-O logic cannot quantify over functions. But
          > > > > couldn't it be achieved equivalently by reifying functions and
          > > > > predicates? I.e.:
          > > > >
          > > > > x = fun(var)
          > > > >
          > > > > becomes
          > > > >
          > > > > x = call_function(fun, var)
          > > > >
          > > > > and then one can express reflexivity:
          > > > >
          > > > > for all fun, a, b: reflexive(fun) <=> call_function(fun, a, b) =
          > > > > call_function(fun, b, a)
          > > > >
          > > > > Cedric
        • cedricstjl
          Actually, I think that I don t even need levels. for all fun, a, b: call_function(reflexive, fun) call_function(fun, a, b) = call_function(fun, b, a) seems
          Message 4 of 9 , Jun 14, 2006
          • 0 Attachment
            Actually, I think that I don't even need levels.

            for all fun, a, b: call_function(reflexive, fun) <=>
            call_function(fun, a, b) = call_function(fun, b, a)

            seems to work fine to me.

            Cedric

            --- In aima-talk@yahoogroups.com, "cedricstjl" <cedricstjl@...> wrote:
            >
            > I don't see why one would ever want to quantify over call_function. I
            > don't think that there is an equivalent to that in "regular" logic.
            >
            > I can quantify over reflexive by adding another level of indirection.
            > reflexive(f) becomes call_function_2(reflexive, f). As long as all
            > functions have a clearly defined level, it should work. Furthermore,
            > using levels is, from what I've read, a common way of avoiding
            > Russell's paradox in SOL. Does the "SOL is strictly more expressive
            > than FOL" claim apply only to SOL without levels?
            >
            > Cedric
            >
            > --- In aima-talk@yahoogroups.com, "Peter Norvig" <peter@> wrote:
            > >
            > > I agree that for most of what you would reasonably want to do, it
            > > wouldn't matter. But the point is that when you quantify over all
            > > functions/relations (represented as objects), you wouldn't be
            > > quantifying over "call_function" nor "reflexive".
            > >
            > > -Peter
            > >
            > > On 6/13/06, cedricstjl <cedricstjl@> wrote:
            > > > Why does it matter? I'm quantifying over "objects that behave
            exactly
            > > > like FOL functions" instead of quantifying directly over FOL
            > functions.
            > > >
            > > > I could write a program, which takes as input a second-order logic
            > > > sentence, does inference in FOL with the conversion from my first
            > > > post, and translates back into second-order logic. Or are there SOL
            > > > sentences that wouldn't be translatable?
            > > >
            > > > Thank you for your time,
            > > >
            > > > Cedric
            > > >
            > > > --- In aima-talk@yahoogroups.com, "Peter Norvig" <peter@> wrote:
            > > > >
            > > > > You could do that, and that could be a way of expressing
            > reflexivity,
            > > > > but it wouldn't be quantifying over FOL functions -- it would be
            > > > > quantifying over objects that you happen to call "functions"
            but are
            > > > > regular objects as far as the logic is concerned.
            > > > >
            > > > > -Peter
            > > > >
            > > > > On 6/8/06, cedricstjl <cedricstjl@> wrote:
            > > > > > I have some difficulty seeing the difference in expressiveness
            > between
            > > > > > first-order logic and higher-order logics. Wikipedia (as well
            > as AIMA,
            > > > > > AFAICT) says that F-O logic cannot quantify over functions. But
            > > > > > couldn't it be achieved equivalently by reifying functions and
            > > > > > predicates? I.e.:
            > > > > >
            > > > > > x = fun(var)
            > > > > >
            > > > > > becomes
            > > > > >
            > > > > > x = call_function(fun, var)
            > > > > >
            > > > > > and then one can express reflexivity:
            > > > > >
            > > > > > for all fun, a, b: reflexive(fun) <=> call_function(fun, a, b) =
            > > > > > call_function(fun, b, a)
            > > > > >
            > > > > > Cedric
            >
          • Joe Hendrix
            ... This is a useful technique. I ve also seen it called currifying in other papers, however it doesn t let you achieve the full power of second-order logic,
            Message 5 of 9 , Jun 14, 2006
            • 0 Attachment
              > On 6/8/06, cedricstjl <cedricstjl@> wrote:
              > couldn't it be achieved equivalently by reifying functions and
              > predicates?

              This is a useful technique. I've also seen it called currifying in
              other papers, however it doesn't let you achieve the full power of
              second-order logic, much less higher-order logic.

              A basic first-order logic result is that finiteness is not
              expressible. That is there is no sentence P such that M is a model of
              P iff. M is finite. However, in second order logic one can express
              finiteness. Specifically, if P is the statement that all injective
              functions are surjective, then M is a model of P iff. M is finite.

              The wikipedia article on second-order logic discusses some of the
              differences between first-order and second-order logic at more length
              than this email.

              Joe
            • cedricstjl
              Hmmm, I ve got a hard time translating your example, or those from the Wikipedia article into logical sentences (I have no idea how to express that a model is
              Message 6 of 9 , Jun 15, 2006
              • 0 Attachment
                Hmmm, I've got a hard time translating your example, or those from the
                Wikipedia article into logical sentences (I have no idea how to
                express that a model is finite, for instance). I guess I should pick
                up a book on the subject; my only background in logic is from AIMA and
                Hofstadter's book.

                Thanks for the info!

                Cedric

                --- In aima-talk@yahoogroups.com, Joe Hendrix <jhendrix@...> wrote:
                >
                > > On 6/8/06, cedricstjl <cedricstjl@> wrote:
                > > couldn't it be achieved equivalently by reifying functions and
                > > predicates?
                >
                > This is a useful technique. I've also seen it called currifying in
                > other papers, however it doesn't let you achieve the full power of
                > second-order logic, much less higher-order logic.
                >
                > A basic first-order logic result is that finiteness is not
                > expressible. That is there is no sentence P such that M is a model of
                > P iff. M is finite. However, in second order logic one can express
                > finiteness. Specifically, if P is the statement that all injective
                > functions are surjective, then M is a model of P iff. M is finite.
                >
                > The wikipedia article on second-order logic discusses some of the
                > differences between first-order and second-order logic at more length
                > than this email.
                >
                > Joe
                >
              Your message has been successfully submitted and would be delivered to recipients shortly.