higher-order logic

higher-order logic

Post by alex goldm » Fri, 28 Jan 2005 22:16:13


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)
 
 
 

higher-order logic

Post by Jose Juan » Sat, 29 Jan 2005 20:10:40


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

 
 
 

higher-order logic

Post by alex goldm » Tue, 01 Feb 2005 03:22:21


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?
 
 
 

higher-order logic

Post by hbe » Tue, 01 Feb 2005 07:42:13


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
 
 
 

higher-order logic

Post by Owen » Tue, 01 Feb 2005 21:13:31


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

higher-order logic

Post by Jose Juan » Wed, 02 Feb 2005 01:09:34


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
 
 
 

higher-order logic

Post by alex goldm » Wed, 02 Feb 2005 01:23:53


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.
 
 
 

higher-order logic

Post by Chris Menz » Wed, 02 Feb 2005 05:58:06

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
 
 
 

higher-order logic

Post by Jeffrey Ke » Wed, 02 Feb 2005 07:23:20

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
 
 
 

higher-order logic

Post by Owen » Wed, 02 Feb 2005 19:44:19

"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
 
 
 

higher-order logic

Post by Chris Menz » Thu, 03 Feb 2005 02:16:16

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
 
 
 

higher-order logic

Post by me » Thu, 03 Feb 2005 06:11:03


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