I'm interested in learning more about higher-order logic: its computational

aspects, inference and learning algorithms, and perhaps uncertainty

representation.

The books on higher-order logic that I found appear to actually be tutorials

on using specific proof assistance software products (HOL or Isabelle),

which is not what I want.

Does anyone have any suggestions or links to resources? (No research paper

plugs please, however)

This is a very readable introduction to higher-order

intuionistic logic:

Simon Thompson, 'Type Theory and Functional Programming'

http://www.yqcomputer.com/

Jose Juan Mendoza Rodriguez

let me=josejuanmr in

let privacy=iespana in

let net=es in

XXXX@XXXXX.COM

Thanks. I've read some of it, however, while I asked for pointers to

literature on higher-order logic, this paper discusses first-order logic.

And, while it's not a research paper plug, it does seem to be Constructive

Mathematics advocacy and mainly concerns itself with programming aides,

does it not?

I was hoping to find a non-advocacy review of main results in higher-order

logic (as opposed to first-order logic).

By the way, is the term "higher-order logic" ever used in a sense different

from "second-order logic"? Since second-order logic allows quantification

over relations, would third-, etc. order logics allow quantification over

quantifiers or something similarly outlandish?

It's simpler than that.

First order: quantify over individuals

Second order: quantify over sets of individuals and relations on individuals.

Third order: quantify over sets of sets of individuals (and relations on

relations on individuals).

Quibble: Church actually used a slightly more refined way of counting

third, fourth, ... order.

You said (in the original post) no plugs, so I won't say anything

about Chapter 4 of my logic book.

--Herb Enderton

>>By the way, is the term "higher-order logic" ever used in a sense

different

>>from "second-order logic"? Since second-order logic allows

quantification

>>over relations, would third-, etc. order logics allow quantification

over

>>quantifiers or something similarly outlandish?

>

> It's simpler than that.

> First order: quantify over individuals

> Second order: quantify over sets of individuals and relations on

individuals.

> Third order: quantify over sets of sets of individuals (and relations

on

> relations on individuals).

I don't agree.

Second order logic quantifies over properties/relations of individuals,

and so on.

There is no need to specify sets at all.

Only if sets correspond with properties, are you correct.

(there are exceptions: the Russell set does not correspond with any

property)

{x:~(x e x} does not exist!

Third order predications quantify over properties of properties, etc.

>

> Quibble: Church actually used a slightly more refined way of counting

> third, fourth, ... order.

>

>> I'm interested in learning more about higher-order logic

>> (...)

>>I was hoping to find a non-advocacy review of main results in

higher-order

>>logic (as opposed to first-order logic).

>

> You said (in the original post) no plugs, so I won't say anything

> about Chapter 4 of my logic book.

>

> --Herb Enderton

>

>

And also higher-order logics. See sections '5.9 Universes' on page 174,

and '6.3.5/6 Quantification and universes' on page 220.

Any book or paper teaching a difficult subject carries advocacy in

one way or another. If the author weren't interested in the subject,

it wouldn't have taken the task of writing the book/paper.

You mentioned "its computational aspects" in your original post.

The main principle underlying current intuitionistic logic/type theory

is that propositions behave as types in programming languages,

and proofs behave as programs (this is my oversimplified point of view,

of course).

I forgot to mention the following texts in my last message.

The first one is directly related to complexity theory, it discusses

second-order classical logic over finite structures. The second one

is more detailed, it deals with first and second-order intuitionistic

logic. You may want to compare the semantic differences between

classical SOL and System F (it's not a trivial task!).

http://www.yqcomputer.com/

Wolfgang Thomas, Languages, automata and logic. Technical Report 9607,

Institut f Informatik und Praktische Mathematik,

Christian-Albrechts-Universit zu Kiel, Germany, May 1996.

http://www.yqcomputer.com/ ~pt/stable/prot.ps.gz

J.-Y. Girard (translated and with appendices by Y. Lafont & P. Taylor),

Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7,

Cambridge University Press (1989)

You seem to be interested in applications of logic to artificial

intelligence. Perhaps asking this question in comp.ai or

comp.lang.functional may give more informative answers.

Good luck.

JosJuan Mendoza Rodruez

Thanks for the suggestions. "Computational aspects" was ambiguous. By those

I meant algorithms for and complexities of inference, learning, etc. [in

higher-order logic], and not so much the application of logic to functional

programming language design.

On Mon, 31 Jan 2005 07:13:31 -0500, Owen < XXXX@XXXXX.COM > said:

It seems that you do.

As well as over individuals.

And in the standard semantics for higher-order logic that Herb was

assuming, they are.

Chris Menzel

It seems that you do.

As well as over individuals.

And in the standard semantics for higher-order logic that Herb was

assuming, they are.

Chris Menzel

wen wrote in message ...

On the usual Henkin semantics for a (consider monadic, for simplicity)

second-order language L, an L-structure has the form (M, S), where

(i) M is the interpretation of the first-order sublanguage (with domain

dom(M)),

(ii) S is some subset of P(dom(M)).

If S is the full power set P(dom(M)), we say that the structure is full.

The structure (M, S) need not even satisfy the Comprehension Scheme:

(EX)(Ax)(X(x) <-> phi(x))

Usually we consider structures that satisfy comprehension or some restricted

version of comprehension (e.g., predicative comprehension, where phi(x)

cannot contain bound occurrences of second-order variables).

A valuation over (M, S) is a function v such that

(a) v maps each constant, first-order variable and term to an element of

dom(M);

(b) v maps each second-order (monadic) variable to an element of S (i.e., a

set).

So, if X is a second-order (monadic) variable, then v(X) is a set (not a

property).

The semantic clause for evaluating atomic (monadic) second-order formulas

is:

A formula X(t) is true in (M, S) relative to v iff v(t) is in v(X).

The semantic clause for evaluating universal second-order formulas is:

A formula (AX)phi(X) is true in (M, S) relative to v iff for any set A in S,

phi(X) is true in (M, S) relative to v*, (where v* is identical to v except

that v(X) is A).

Obviously, all of this (semantical meta-theory) is irreducibly

set-theoretic.

One could consider the notion of a "property-structure", of the form (M,

S*), where S* is a collection of properties of entities in dom(M). One

should be able to write out the corresponding semantcal metatheory without

too much difficulty. E.g.,

So, if X is a second-order variable, then v(X) is a property.

A formula X(t) is true in (M, S*) relative to v iff v(t) has property v(X).

But it's rather unclear what relations hold between the properties in S*.

E.g., if P and Q are properties, then is their disjunction a property? Their

conjunction? If R is a binary relation, then is its quantification (E)R a

property? In the case of second-order logic with the usual Henkin semantics,

then either we have that the structure satisfies comprehension (which

explicitly tells us which sets exist in S) and we can use standard

set-theoretic methods in the meta-theory, or we consider full models, in

which case we have all subsets of the first-order domain. Unfortunately, in

areas where people worry about properties, no one thinks that comprehension

is valid for properties and no one thinks that each subsets of a domain

corresponds to a genuine property.

I've heard people talk about placing a metric on the first-order domain and

identfying properties with convex sets.

The debate about what SOL really quantifies over is a bit misguided, in my

view. There are a number of different ways of providing a semantics for SOL.

Non-standard Henkin models are actually quite useful. This is because the

Completeness Theorem (Henkin 1950) holds with respect to Henkin semantics.

As such, they are used all the time in technical work on second-order

theories (see, e.g., Simpson's book _Subsystems of Second-Order Arithmetic_,

1998).

For example, any non-standard model M of PA expands to a non-standard Henkin

model (M, S) of the predicative second-order theory ACA_0 by taking S to be

the arithmetically definable (in M) sets. It follows that ACA_0

conservatively extends PA.

George B

On the usual Henkin semantics for a (consider monadic, for simplicity)

second-order language L, an L-structure has the form (M, S), where

(i) M is the interpretation of the first-order sublanguage (with domain

dom(M)),

(ii) S is some subset of P(dom(M)).

If S is the full power set P(dom(M)), we say that the structure is full.

The structure (M, S) need not even satisfy the Comprehension Scheme:

(EX)(Ax)(X(x) <-> phi(x))

Usually we consider structures that satisfy comprehension or some restricted

version of comprehension (e.g., predicative comprehension, where phi(x)

cannot contain bound occurrences of second-order variables).

A valuation over (M, S) is a function v such that

(a) v maps each constant, first-order variable and term to an element of

dom(M);

(b) v maps each second-order (monadic) variable to an element of S (i.e., a

set).

So, if X is a second-order (monadic) variable, then v(X) is a set (not a

property).

The semantic clause for evaluating atomic (monadic) second-order formulas

is:

A formula X(t) is true in (M, S) relative to v iff v(t) is in v(X).

The semantic clause for evaluating universal second-order formulas is:

A formula (AX)phi(X) is true in (M, S) relative to v iff for any set A in S,

phi(X) is true in (M, S) relative to v*, (where v* is identical to v except

that v(X) is A).

Obviously, all of this (semantical meta-theory) is irreducibly

set-theoretic.

One could consider the notion of a "property-structure", of the form (M,

S*), where S* is a collection of properties of entities in dom(M). One

should be able to write out the corresponding semantcal metatheory without

too much difficulty. E.g.,

So, if X is a second-order variable, then v(X) is a property.

A formula X(t) is true in (M, S*) relative to v iff v(t) has property v(X).

But it's rather unclear what relations hold between the properties in S*.

E.g., if P and Q are properties, then is their disjunction a property? Their

conjunction? If R is a binary relation, then is its quantification (E)R a

property? In the case of second-order logic with the usual Henkin semantics,

then either we have that the structure satisfies comprehension (which

explicitly tells us which sets exist in S) and we can use standard

set-theoretic methods in the meta-theory, or we consider full models, in

which case we have all subsets of the first-order domain. Unfortunately, in

areas where people worry about properties, no one thinks that comprehension

is valid for properties and no one thinks that each subsets of a domain

corresponds to a genuine property.

I've heard people talk about placing a metric on the first-order domain and

identfying properties with convex sets.

The debate about what SOL really quantifies over is a bit misguided, in my

view. There are a number of different ways of providing a semantics for SOL.

Non-standard Henkin models are actually quite useful. This is because the

Completeness Theorem (Henkin 1950) holds with respect to Henkin semantics.

As such, they are used all the time in technical work on second-order

theories (see, e.g., Simpson's book _Subsystems of Second-Order Arithmetic_,

1998).

For example, any non-standard model M of PA expands to a non-standard Henkin

model (M, S) of the predicative second-order theory ACA_0 by taking S to be

the arithmetically definable (in M) sets. It follows that ACA_0

conservatively extends PA.

George B

"Jeffrey Ketland" < XXXX@XXXXX.COM > wrote in message

news:ctmbed$af6$ XXXX@XXXXX.COM ...

> Owen wrote in message ...

>

>> I don't agree.

>> Second order logic quantifies over properties/relations of

individuals,

>>and so on.

>> There is no need to specify sets at all.

>

> On the usual Henkin semantics for a (consider monadic, for simplicity)

> second-order language L, an L-structure has the form (M, S), where

> (i) M is the interpretation of the first-order sublanguage (with domain

> dom(M)),

> (ii) S is some subset of P(dom(M)).

>

> If S is the full power set P(dom(M)), we say that the structure is full.

>

> The structure (M, S) need not even satisfy the Comprehension Scheme:

> (EX)(Ax)(X(x) <-> phi(x))

> Usually we consider structures that satisfy comprehension or some

restricted

> version of comprehension (e.g., predicative comprehension, where phi(x)

> cannot contain bound occurrences of second-order variables).

>

> A valuation over (M, S) is a function v such that

> (a) v maps each constant, first-order variable and term to an element of

> dom(M);

> (b) v maps each second-order (monadic) variable to an element of S

(i.e., a

> set).

>

> So, if X is a second-order (monadic) variable, then v(X) is a set (not a

> property).

>

> The semantic clause for evaluating atomic (monadic) second-order

formulas

> is:

>

> A formula X(t) is true in (M, S) relative to v iff v(t) is in v(X).

>

> The semantic clause for evaluating universal second-order formulas is:

>

> A formula (AX)phi(X) is true in (M, S) relative to v iff for any set A

in S,

> phi(X) is true in (M, S) relative to v*, (where v* is identical to v

except

> that v(X) is A).

>

> Obviously, all of this (semantical meta-theory) is irreducibly

> set-theoretic.

> One could consider the notion of a "property-structure", of the form (M,

> S*), where S* is a collection of properties of entities in dom(M). One

> should be able to write out the corresponding semantcal metatheory

without

> too much difficulty. E.g.,

>

> So, if X is a second-order variable, then v(X) is a property.

> A formula X(t) is true in (M, S*) relative to v iff v(t) has property

v(X).

>

> But it's rather unclear what relations hold between the properties in

S*.

> E.g., if P and Q are properties, then is their disjunction a property?

Their

> conjunction? If R is a binary relation, then is its quantification (E)R

a

> property? In the case of second-order logic with the usual Henkin

semantics,

> then either we have that the structure satisfies comprehension (which

> explicitly tells us which sets exist in S) and we can use standard

> set-theoretic methods in the meta-theory, or we consider full models, in

> which case we have all subsets of the first-order domain. Unfortunately,

in

> areas where people worry about properties, no one thinks that

comprehension

> is valid for properties and no one thinks that each subsets of a domain

> corresponds to a genuine property.

> I've heard people talk about placing a metric on the first-order domain

and

> identfying properties with convex s

news:ctmbed$af6$ XXXX@XXXXX.COM ...

> Owen wrote in message ...

>

>> I don't agree.

>> Second order logic quantifies over properties/relations of

individuals,

>>and so on.

>> There is no need to specify sets at all.

>

> On the usual Henkin semantics for a (consider monadic, for simplicity)

> second-order language L, an L-structure has the form (M, S), where

> (i) M is the interpretation of the first-order sublanguage (with domain

> dom(M)),

> (ii) S is some subset of P(dom(M)).

>

> If S is the full power set P(dom(M)), we say that the structure is full.

>

> The structure (M, S) need not even satisfy the Comprehension Scheme:

> (EX)(Ax)(X(x) <-> phi(x))

> Usually we consider structures that satisfy comprehension or some

restricted

> version of comprehension (e.g., predicative comprehension, where phi(x)

> cannot contain bound occurrences of second-order variables).

>

> A valuation over (M, S) is a function v such that

> (a) v maps each constant, first-order variable and term to an element of

> dom(M);

> (b) v maps each second-order (monadic) variable to an element of S

(i.e., a

> set).

>

> So, if X is a second-order (monadic) variable, then v(X) is a set (not a

> property).

>

> The semantic clause for evaluating atomic (monadic) second-order

formulas

> is:

>

> A formula X(t) is true in (M, S) relative to v iff v(t) is in v(X).

>

> The semantic clause for evaluating universal second-order formulas is:

>

> A formula (AX)phi(X) is true in (M, S) relative to v iff for any set A

in S,

> phi(X) is true in (M, S) relative to v*, (where v* is identical to v

except

> that v(X) is A).

>

> Obviously, all of this (semantical meta-theory) is irreducibly

> set-theoretic.

> One could consider the notion of a "property-structure", of the form (M,

> S*), where S* is a collection of properties of entities in dom(M). One

> should be able to write out the corresponding semantcal metatheory

without

> too much difficulty. E.g.,

>

> So, if X is a second-order variable, then v(X) is a property.

> A formula X(t) is true in (M, S*) relative to v iff v(t) has property

v(X).

>

> But it's rather unclear what relations hold between the properties in

S*.

> E.g., if P and Q are properties, then is their disjunction a property?

Their

> conjunction? If R is a binary relation, then is its quantification (E)R

a

> property? In the case of second-order logic with the usual Henkin

semantics,

> then either we have that the structure satisfies comprehension (which

> explicitly tells us which sets exist in S) and we can use standard

> set-theoretic methods in the meta-theory, or we consider full models, in

> which case we have all subsets of the first-order domain. Unfortunately,

in

> areas where people worry about properties, no one thinks that

comprehension

> is valid for properties and no one thinks that each subsets of a domain

> corresponds to a genuine property.

> I've heard people talk about placing a metric on the first-order domain

and

> identfying properties with convex s

On Tue, 1 Feb 2005 05:44:19 -0500, Owen < XXXX@XXXXX.COM > said:

The axiom of reducibility only makes sense within the baroque system of

types and orders of the ramified theory of types, which you've

jettisoned here.

What you call AR above is indeed trivial in second order logic. But it

isn't AR.

Chris Menzel

The axiom of reducibility only makes sense within the baroque system of

types and orders of the ramified theory of types, which you've

jettisoned here.

What you call AR above is indeed trivial in second order logic. But it

isn't AR.

Chris Menzel

The phrase "higher-order logic" usually refers to systems

that are descendents of Church's T system. In them, typically

every expression has a type and expressions of type o are

formulas. A predicate of type o->o takes a formula as an

argument. An predicate of type (o->o)->o takes an expression of

type (o->o) as an argument, and so on.

Because there is no limit to how much this can be extended,

it's sometimes called "higher-order logic" (some people insist

on the spelling "higher order logic", three words). However,

it should be noted that the type restrictions make it something

quite different from conventional second-order logic.

--Jamie. (a Dover edition designed for years of use!)

andrews .uwo } Merge these two lines to obtain my e-mail address.

@csd .ca } (Unsolicited "bulk" e-mail costs everyone.)

1. type theory and higher order logic?

2. OT: Higher Order Perl and Amazon (was: Book: Higher-Order Perl: Transforming Programs with Programs)

3. attn: James Edward Gray II, Higher-Order Ruby

4. Higher-order messaging in Ruby

5. Can I enter higher-order differentials in MATL

6. Can I enter higher-order differentials in MATLAB?

8. [kepler-dev] question on typing processes and higher-order fu

9. Functional Programming in C -- higher-order programming

10. higher-order programming language

11. Accessibility of the Higher-Order Perl E-book in Amazon (Was: Emulating Generators)

12. Does unpack() support higher-order Unicode strings for hex conversion?

13. higher-order macros [ Python syntax in Lisp and Scheme

14. Book: Higher-Order Perl: Transforming Programs with Programs

15. Higher-Order Perl: The Quest for an Accessible Version, Initial Impressions (Long)

12 post • Page:**1** of **1**