Rick, (01)
As Pat emphasized, there is a huge semantic difference between
quantifying over relations (which can be done in Common Logic
with a first-order style of semantics) and the kind of higher-order
logic that logicians have been kicking around. (02)
In fact, many logicians have now come to believe that the infinite
hierarchy of relations, relations of relations, etc., which are
assumed for higher-order logic, should *not* be considered part
of logic. They should be considered a version of set theory. (03)
The computational system called HOL does not assume the hierarchies
that logicians talk about. In fact, HOL uses a semantics that is
very similar to CL. (It's probably a subset of CL semantics, but
it would be necessary to check that claim.) (04)
PH
>> Ask yourself whether [axioms (R a) and (Q b)] entail the following:
>>
>> (exists (p)(and (p a)(p b) )
>>
>> i.e. that there is a property that applies both to a and to b.
>>
>> If you intuitively answer "no", then you are thinking first-order,
>> and would likely find CL congenial. If it seems obviously "yes",
>> then you are thinking in a genuinely higher-order way.
>>
>> It really does matter which way you choose, as you will be
>> interested in very different logics. (05)
RM
> Understood. I've been heads down on functional programming lately, so
> I'm getting more comfy with higher order thinking. (06)
But the usual versions of functional programming are not higher-order
in the way logicians use the term. (07)
For Pat's example, the axioms (R a) and (Q b) can be satisfied in
a CL domain that has only four entities: {R, Q, a, b}. (08)
In that model, there is no p such that (p a) and (p b) are both true.
Therefore the statement (exists (p) (and (p a)(p b)) is false. (09)
But in the logicians' version of higher order logic, for any domain
of individuals such as {a,b}, there is an infinite hierarchy of
domains of all possible relations over the domain {a,b}, relations
of relations over that domain, ... (010)
Since all possible relations are included, there would have to be
some relation p such that (p a) and (p b). (011)
If you're using functional programming, I doubt that you would naturally
think of that infinite hierarchy while you're writing a program. I
suspect that you're more likely to think about CL kinds of models. (012)
RM
> to establish a hierarchy of types to avoid paradox. (013)
You don't need a hierarchy of types to avoid paradox.
In CL, the statement equivalent to Russell's paradox has
a stable truth value: false. No paradox. (014)
As far as types are concerned, I'd like to emphasize that you can,
if you wish, partition the domain of a CL model in disjoint sets
that you can call types. (015)
CL does not prevent you from using types. In fact, it encourages
you to do so by using quantifier restrictions. For example, (016)
(forall ((x Employee)) (exists ((y SSN)) ... )) (017)
This says that for all x of type Employee, there exists a y of
type SSN, where Employee and SSN are monadic relations that
restrict the domain of quantification of the variables x and y. (018)
This gives you weak typing. A logic with strong typing, such as Z,
can be mapped to a system with weak typing such as CL. Furthermore,
if you use quantifier restrictions, you can map the CL statements
that came from Z back to Z statements. (019)
What you get with Z is the option of using syntactic checks that
prevent any possible type mismatch. If you really, really want
strong type checking, you could also parse any set of CL statements
that were derived from Z to ensure that they obey the Z constraints. (020)
On the other hand, there are many legitimate sentences that you
can express in CL, which cannot be expressed in Z: (021)
"The number 23 is not an elephant." (022)
That is a true statement, which could be written (not (Elephant 23)). (023)
But you can't say that in Z because 'Elephant(23)' is a syntax error. (024)
In summary, you can map strongly typed logics to CL, if you want them.
If you really want to enforce the rules for strong typing, you can
even write a CL parser that would enforce those typing rules. (025)
But CL also permits you to use weak typing or no typing at all. (026)
John (027)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (028)
|