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

Re: Quantifying over functions in first-order logic

Expand Messages
  • 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 1 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 2 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 3 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.