OK. (01)
Sincerely,
Rich Cooper
EnglishLogicKernel.com
Rich AT EnglishLogicKernel DOT com (02)
-----Original Message-----
From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx
[mailto:ontolog-forum-bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher
Menzel
Sent: Tuesday, February 09, 2010 11:21 AM
To: [ontolog-forum]
Subject: Re: [ontolog-forum] Inconsistent Theories (03)
On Feb 9, 2010, at 11:37 AM, Rich Cooper wrote:
> ...
>>> On Feb 9, 2010, at 12:56 AM, Rich Cooper wrote:
>>> Define( F(x), (x^3+27*x^2) )
>>
>> I think you are referring to the LISP operator "defun", in which case you
want:
>>
>> (defun F (x)
>> (* (+ (expt x 3) 27) (expt x 2))))
>
> Yes, thanks for completing the lisp expr in proper format.
>
>> > Which states that the identify of the symbol F(x) is defined to be
equal to
>> > the evaluable structure (x^3+27*x^2) which can be used to calculate the
>> > value of F(x) bound to any x.
>> >
>> > Those are two different views of '=' - by value and by defined
structure
>> > (expression or object, perhaps).
>
>> No, they aren't. Equality and defun are two entirely different things in
LISP.
>
> Isn't that what I just said above? (04)
I wasn't clear. My point was that defun isn't any sort of notion of
equality. It is a procedural operation. It *establishes* a certain class
of equalities when it is called. There simply *is* nothing like defun in
ordinary first-order logic (though I supposed one could come up with
something like it if one formalized first-order metatheory). (05)
> Defun puts the structure on an association list with the decomposition
above as its 'value' propery. That means, its value is defined by
evaluating the 'value' property. But there is still a significant
difference between the definition and the value of (F x). (06)
Obviously, but my whole point is that NONE of this is apposite to the
original discussion. You have injected all sorts of issues from the
semantics of programming languages into a simple discussion about the
semantics of identity in first-order logic that was spawned by a related
point about incompatible theories. If you want to discuss the semantics of
programming languages, fine and dandy, but start another thread or
something. You might as well have started injecting all sort of facts about
quantum electrodynamics or agribusiness. It's just not relevant. Start
another thread. (07)
> If you're going to appeal to LISP, you might be able to make your point
more profitably by appealing to its several related but distinct notions: --
"eq", "eql", "equal", and "equalp". But the general problem, again, is that
you are conflating the semantics of first-order logic with the semantics of
programming languages.
>
> Its not Lisp per se which I am trying to use in explaining the property
concept, but the fact that any lisp atom or expr can have as many properties
as you want to associate with it. The various versions of '=' in Lisp are
there for various programming reasons. But the particular reason I am
bringing up in this discussion is not Lisp, it's the multiplicity of
different kinds of properties that an object in a database can exhibit.
Don't get hung up on Lisp - I wanted to use something we all know to make
the point about how there are many properties, one of which is definition,
another value, ... etc.
>
> > The interpretation can be calculated to get the value, but the
interpretation is distinct from the value it gets at any given time.
>
> You illustrate my point nicely. LISP is a programming language; it is not
a first-order language.
>
> Actually, no. (08)
Actually, yes. You are confusing the fact that you can write S-expressions
that look like sentences of a first-order language, and the fact that you
can do some first-order theorem proving in LISP, with the idea that it's a
first-order language or (as you say below) a "superset" of first-order
logic. It isn't. Really. Programming language models are vastly more
complex and *also* far more constrained than models of first-order
languages. You can of course *transform* a first-order language into a
programming language by giving it a programming language semantics -- that's
basically what PROLOG does (though this claim needs to be qualified in
numerous ways). But, after doing so, it is no longer a first-order
language. In the context of this thread, a language is first-order in
virtue of having a standard first-order model theory. (09)
> Lisp has often been used to record FOL functionality. Any programming
language can perform any FOL calculation short of infinite. (010)
You are confusing first-order logic with automated theorem proving. (011)
> For example, the conjunct:
>
> (And (Box 'A)
> (Rectangle 'B)
> (OnTopOf 'A 'B))
>
> Is a perfectly feasible FOL situation description. (012)
Vide the point above. The fact that you can write S-expressions that look
like FOL sentences does not mean LISP is a first-order language. (013)
> And in fact, not only lisp, but any programming language incorporates full
FOL functionality (short of infinities). (014)
I think you have something like expressiveness in mind but there is no
straightforward comparison to be made between logical languages and
programming languages in those terms. (015)
> The semantics of programming languages is far more specialized and,
generally, far more complex than the semantics of first-order languages;
consider, e.g., the mathematics of domain theory that underlies the
denotational semantics of Scott and Strachey. The semantics of LISP, in
particular, is a very rich and difficult subject that involves not only
general issues in the semantics of programming languages such as support for
recursion but also issues related to list processing and the semantics of
LISP's distinctive operators like "defun", "cons", "car", "cdr", "setq",
etc. These issues are light years removed from vanilla first-order model
theory.
>
> Wrong, as described above. FOL is a SUBSET of modern programming
languages without infinity. (016)
*sigh* This statement is confused along so many dimensions that one scarcely
knows where to begin. I don't plan to start. (017)
-cm (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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (019)
_________________________________________________________________
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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (020)
|