ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] type free logic and higher order quantification

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Fri, 19 Aug 2011 18:15:12 -0400
Message-id: <4E4EE070.2000207@xxxxxxxxxxx>
Just two points about Pat's comments, which I completely agree with.    (01)

> I have been taken to task by some very competent logicians for calling
> CL first-order, as they are using a purely syntactic criterion of order.
> Nobody is right in debates like this, but clearly the terminology
> lacks precision.    (02)

I strongly agree.  I like to cite Quine's short article that shows
how to reduce quantification over relations (as in CL) to a notation
in which there is only one relation -- just an "apply relation" that
applies one individual to another individual.    (03)

That shows very clearly that there is no need to consider quantifiers
over relations to be higher order than quantification over individuals.
For the record, following is the citation:    (04)

Quine, Willard Van Orman (1953) Reduction to a dyadic predicate, 
reprinted in Quine (1966), pp. 224-226.    (05)

Quine, Willard Van Orman (1966) Selected Logic Papers, Enlarged Edition, 
Harvard University Press, Cambridge, MA, 1995.    (06)

> The usual formulation of defining conditions does not permit a
> definition to be false, which forces the paradox into existence.    (07)

Many people make a distinction between definitions and other statements:    (08)

  1. Some use the phrase "true by definition", by which they mean
     "necessarily true" or "non-negotiable".    (09)

  2. The DL tradition distinguishes the T-Box (Terminology definitions)
     as necessarily true in comparison to the A-Box (Assertions).    (010)

  3. The people who do belief revision or theory revision define
     degrees of "entrenchment" for various statements.  Definitions
     are usually considered the most deeply entrenched and the last
     ones to be modified by any method of revision.    (011)

These assumptions are metalevel statements outside the system of logic
itself.  When we were working on the Common Logic standard, there were
some requests for a "define" verb or its equivalent that would allow
somebody to say    (012)

    Define (square x) as (times x x).    (013)

This definition, by itself, would be harmless.  It could be considered
syntactic sugar for an equivalence:    (014)

    (forall (x) (iff (square x) (times x x))    (015)

But when you introduce a 'define' verb, somebody is likely to try
a recursive definition that uses the same name on the left and
the right.  When you do that, you create puzzles and paradoxes.    (016)

If you use the equivalence statement (with 'iff'), you just have
a statement that might happen to be false.  There is no puzzle
about something false that is supposed to be "true by definition".    (017)

John    (018)

_________________________________________________________________
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    (019)

<Prev in Thread] Current Thread [Next in Thread>