Thanks John. See below. (01)
On Fri, 2011-08-19 at 10:31 -0400, John F. Sowa wrote:
> 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. (02)
John, your point is completely superfluous. I have already clarified the
term in relation to section 3.4.4 in Chris's paper. (03)
As an aside, why do you say 'kicking around?' I am left with the
impression that you don't respect the work of these logicians on higher
order logic. (04)
> 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. (05)
Really, I hope they are still employed. (06)
> 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.) (07)
Are you referring to Mike Gordon's HOL, or Paulson's Isabelle/HOL? (08)
Will you be publishing your proof in the Journal of Symbolic Logic? This
is surely a publishable result. (09)
>
> 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. (010)
In what way, John? Are you challenging the validity of the
Girard-Reynolds Isomorphism? (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)
While I'm writing a program, I'm quite un-naturally thinking in a
syntactic sugar over the second order (polymorphic) lambda calculus. (013)
I am very unlikley to think about CL models. (014)
> RM
> > to establish a hierarchy of types to avoid paradox.
>
> You don't need a hierarchy of types to avoid paradox. (015)
John, you are superimposing an inappropriate context on the statement I
made to foist your polemic on me and others. My statement explained the
meaning of the term predicativity in the literature of intuitionistic
logic. (016)
> In CL, the statement equivalent to Russell's paradox has
> a stable truth value: false. No paradox.
>
> 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. (017)
Let me understand. (018)
1. Chris nicely outlines design goals and derives the rationale for CL
as a fully and completely type free logic for the web. (019)
2. You recommend partitioning a domain in this type free logic, naming
the partition set, then renaming the set to type. (020)
You won't find me doing that, John. That is very problematic. And surely
your have a high tolerance for ambiguity and a low standard for the
veridical in semantics. (021)
> CL does not prevent you from using types. (022)
But CL is fully and completely type free and provides no semantics for
types. (023)
> 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. (024)
> A logic with strong typing, such as Z,
> can be mapped to a system with weak typing such as CL. (025)
I won't be using Z, John. We've come a long way since then. (026)
Today, there are much more attractive alternatives in Martin-Lof type
theory, constructive logics and univalent foundations. (027)
> 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. (028)
This is absurd. Of course, unless you're paying. (029)
>
> But CL also permits you to use weak typing or no typing at all. (030)
Really. (031)
> 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
>
> (032)
_________________________________________________________________
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 (033)
|