On Aug 19, 2011, at 9:31 AM, John F. Sowa wrote: (01)
> Rick,
>
> 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.
>
> 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.
>
> 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.)
>
> 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.
>
> RM
>> Understood. I've been heads down on functional programming lately, so
>> I'm getting more comfy with higher order thinking.
>
> But the usual versions of functional programming are not higher-order
> in the way logicians use the term.
>
> 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}.
>
> 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.
>
> 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, ...
>
> Since all possible relations are included, there would have to be
> some relation p such that (p a) and (p b). (02)
In particular, it would be (03)
(lambda (x)(or (R x)(Q x))) (04)
which shows that even if one restricts oneself to lambda-definable relations
(of which there are only countably many, instead of the uncountably many
mathematically possible relations that would exist over any ground universe
that contained, for example, any model of arithmetic) you would still get a
divergence of intuition. As I am sure Chris will want to point out, the Henkin
construction provides a(n arguably) first-order semantics for this
lambda-definable fragment of true HO logic, so the higher/first-order wetlands
get even boggier around here. (05)
>
> 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. (06)
That is my suspicion also, but one never knows :-) (07)
>
> RM
>> to establish a hierarchy of types to avoid paradox.
>
> 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. (08)
It is (09)
(exists (Russel)(forall (x) (iff (Russel x)(not (x x))))) (010)
which yields a contradiction by instantiating x with Russell. What saves this
from being a paradox is that it does not claim to *define* Russell, only to
give exact conditions for its true application. In this case, those very
conditions are contradictory, so the 'definition' fails to define. The usual
formulation of defining conditions does not permit a definition to be false,
which forces the paradox into existence. (011)
> 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.
>
> CL does not prevent you from using types. In fact, it encourages
> you to do so by using quantifier restrictions. For example,
>
> (forall ((x Employee)) (exists ((y SSN)) ... ))
>
> 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.
>
> 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.
>
> 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.
>
> On the other hand, there are many legitimate sentences that you
> can express in CL, which cannot be expressed in Z:
>
> "The number 23 is not an elephant."
>
> That is a true statement, which could be written (not (Elephant 23)).
>
> But you can't say that in Z because 'Elephant(23)' is a syntax error.
>
> 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.
>
> But CL also permits you to use weak typing or no typing at all. (012)
Put another way, strong typing is weak typing where some type-checking
inferences are done by the parser rather than a post-parsing inference engine,
and are considered to be mandatory. (013)
Pat (014)
>
> John
>
> _________________________________________________________________
> 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
>
> (015)
------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 mobile
phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes (016)
_________________________________________________________________
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 (017)
|