David, (01)
> As I understand it, a function in a logical language
> is the same as a proposition with another argument. (02)
I would rephrase that sentence by saying that any function of
N arguments can be replaced by a relation with N+1 arguments. (03)
For example, you could represent the arithmetic operator '+'
by a function: (04)
x+y=z would become plus(x,y)=z (05)
But you could also replace it by a relation: (06)
plus(x,y)=z is equivalent to plus(x,y,z) (07)
> A logical language "function" is radically different than
> imperative language 'function". (08)
No. You can define a function by either method and convert one
definition into the other. (09)
An imperative language (AKA procedural) specifies a step-by-step
algorithm for computing the result of a function. (010)
A logical language (AKA declarative) can specify the preconditions
and postconditions of any computation. There are various methods for
deriving an algorithm from those preconditions and postconditions.
(Those preconditions and postconditions are also called axioms.) (011)
Procedural languages may have "side effects". But those side effects
can also be specified in the pre- and post- conditions (or axioms). (012)
> I don't think IKL (or Common Logic) supports what has traditionally
> been called "definitions" in first order predicate logic. (013)
Pure FOL does not have definitions. If you want to specify a function
(or relation) in FOL, you state axioms that must be true of any use
of that function. But if those axioms happen to be inconsistent or
incomplete, it's possible that no suitable function exists. (014)
For example, I could state the following axiom for a function 'sqrt': (015)
For every x, if x ≥ 0, then sqrt(x)² = x. (016)
But this axiom does not uniquely define sqrt, because every function
must be single-valued. If x=4, sqrt(4) could be 2 or -2. (017)
To specify sqrt uniquely, I would have to add another condition
to the then-clause: (018)
For every x, if x ≥ 0, then sqrt(x)² = x, and sqrt(x) ≥ 0. (019)
The if-clause states the precondition: x≥0.
The then-clause states the postconditions: sqrt(x)²=x & sqrt(x)≥0. (020)
These conditions are just as true for a logical or procedural language. (021)
In any case, IKL was not designed to support definitions, but to support
metalanguage. That is a different, but related issue. (022)
John (023)
_________________________________________________________________
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 (024)
|