[ontoiop-forum] DOL finalisation

[John F Sowa]

On 1/3/2018 2:52 PM, Till Mossakowski wrote:
> in a higher-order setting, no-one prevents you from writing
> 
> (lambda (p) (not (p p)))
> 
> which is a term that cannot have a denotation.

Yes.  I admit that a lambda expression as an argument
of a function or relation could cause an inconsistency.

For anyone who is not familiar with CL semantics, the above
definition would be safe if it had been stated as an axiom:

    (forall (p) (= (f p) (not (p p))))

If you substitute f for p, this axiom would imply

    (= (f f) (not (f f)))

This statement is false.  Therefore, the axiom must be false.
That may cause a problem for a particular theory, but it does
not create an inconsistency in CL semantics.

Examples such as these, explain why CL does *not* have
a special notation for stating definitions, such as

    Define f as (= (f p) (not (p p))).

Since definitions must be true "by definition", this statement
must be true.  And that would create an inconsistency in the
CL methods for stating definitions.

As Till's example illustrates, lambda expressions used as
arguments of a function or relation could create the same
kind of inconsistency as an explicit notation for definitions.

John