[SCL] Re: Folding unnecessary [was: Re: Update to SCL-related work]

[Tanel Tammet]

Pat Hayes wrote:

>> Now, if we forget the equality for a moment,
>> it still appears that once the two folding axioms
>> are present, the "simplified horrocks sentence"
>>
>> (forall (x y) (and (P x) (not (Q y)))
>>
>> does NOT have a one-element domain,
>> differently from the conventional FOL
>> formula, which does.
>>
>> The folding axioms
>>
>> (forall (x) (iff (holds2 P x) (P x)))
>> (forall (x) (iff (holds2 Q x) (Q x)))
>>
>> introduce two constants
>
>
> Yes, quite; which begs the question of their existence, since all 
> constant symbols must denote something in FOL. 

Yes, but this does not pose any problems by itself:
they can all happily denote one single individual
in the domain. Bringing in constant symbols is fine:
the sole problem is how we use these constants in
the axioms.

> So these axioms do not properly capture the folding construction, 
> after all. They express half of it accurately, but they beg the 
> central question. Folding does not require a relation symbol to denote 
> an individual: it only says that IF it also denotes an individual, 
> then that individual's relational extension must be the relation. In 
> other words, it is a conditional whose conclusion is your schema. 
> Unfortunately, the antecedent of that conditional cannot be expressed 
> in a (simple) logic, as it requires one to quantify over things that 
> are not in the universe.

> BTW, this complication is exactly why I introduced the 'header' idea, 
> in order to allow 'outer' quantification in the header to range over a 
> larger universe than 'inner' quantification in the body of the text. 
> Then indeed your schema could be used in the header without having 
> these regrettable Horrocks consequences. BTW, strong equality is = in 
> the header, weak equality is = in the body; and the abstract-syntax 
> SCL-> FOL translation can be viewed as moving everything into the 
> header (and into a purely relational FO logic). But all that is rather 
> complicated, I concede, and maybe cannot be done right now. It is kind 
> of elegant, however.
>
I have so far not seen a way to overcome this complication.

As you say above: "Folding does not require a relation symbol
to denote an individual: it only says that IF it also denotes an
individual, then that individual's relational extension must be the 
relation."

How on earth do we know whether a relation symbol denotes
an individual? Worse still, how are we going to predict
that it will/will not denote an individual in the future?

Simply put, it seems to me that you claim to have an answer,
but I am kind of suspicious that there can be an answer.

Suppose we have an axiom

(forall (x) (implies (x a b) (commutative x)))

Then the question whether some relation symbol
should denote an individual contains a question whether
this relation symbol is true on (a b), which is generally
undecidable, of course. Or do all relation symbols
denote an individual once we have an axiom like this?

All the choices seem to be arbitrary and unsatisfactory.

I could imagine that we may declare, header-like,
that some relation symbols can be given properties
with a formula above, while others cannot (was it
what the headers were for?)

For example, that "f" has an attached constant, while
"g" does not. We could this with headers, but (if
we want to allow this separation)
I'd recommend lexical categories instead.

Whenever you want to split an infinite domain into
two parts, it is easy to define that symbols like "p1:a",
"p1:b", etc denote elements in part p1, and none of the other
symbols denote elements in part p1. This is basically
the same method we commonly use for numeric constants,
strings, etc. Writing (+ 2 4) does not require a header
declaring that 2 and 4 are going to stand for integers!

This lexical separation seems trivial, but has enormous
advantages over headers. Besides being simpler and
easy to understand, the text has always the same meaning:
2 and 4 stand for the same integers in any formula, without
the worry that perhaps headers are slapped on later,
changing everything inside.

In the SCL context it seems that the default behaviour
could be denoting a constant (hence no lexical prefix
required) while any function/relation symbol which
should NOT denote an individual, could be prefixed
with something special, like "c:" or "gofol:" :-)

This is a bit similar to two term/relation syntaxes
I suggested, but it occurs at the lexical level,
which creates much fewer problems than
syntactic differences.

>
> I'll stop writing emails and get on with writing HTML. I hope to have 
> a draft by the end of the week.
>
Waiting with interest.

Regards,
                Tanel