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

Quantifying over functions in first-order logic

Expand Messages
  • cedricstjl
    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
    Message 1 of 9 , Jun 8, 2006
    • 0 Attachment
      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
      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
      Message 2 of 9 , Jun 8, 2006
      • 0 Attachment
        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
        >
        >
        >
        >
        >
        >
        >
      • Maithreebhanu Wimalasekare
        Is acting human approch to AI it usefull orpractical except for simulation and games. ( robotics exculded ) Are there new avenues for reserch in this area and
        Message 3 of 9 , Jun 12, 2006
        • 0 Attachment
          Is acting human approch to AI it usefull orpractical except for simulation and games. ( robotics exculded )

          Are there new avenues for reserch in this area and what promise do they offers to reserchers?


          __________________________________________________
          Do You Yahoo!?
          Tired of spam? Yahoo! Mail has the best spam protection around
          http://mail.yahoo.com

        • 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 4 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 5 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 6 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 7 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 8 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 9 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.