- 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

> > On 6/8/06, cedricstjl <cedricstjl@> wrote:

This is a useful technique. I've also seen it called currifying in

> couldn't it be achieved equivalently by reifying functions and

> predicates?

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- 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

>