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

[Pat Hayes]

>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?

 From the syntax of the text. It does when it is used in a syntactic 
place where it is required to denote one, ie basically as an argument 
of a function or relation.

>Worse still, how are we going to predict
>that it will/will not denote an individual in the future?

Ah, that is a different question. I agree, we cannot know this in 
general in a Web context. But this is not a LOGICAL matter, but an 
architectural one, one that arises from the open nature of the Web. [ 
After all, think about it: there is no notion of 'future' in a 
logical model theory, right?]  The logic can also be used in 'closed' 
situations where we have a fixed text whose boundaries are never 
extended. In this case, if the text is GOFOL, then the MT should 
allow it to be interpreted as GOFOL without any translation or 
embedding. Part of the header idea was to allow the header to in 
effect declare that the text it encloses is GOFOL, so allow GOFOL 
text to be published openly but protected from contamination by 
general SCL text. This would allow GOFOL users to use SCL for 
interchange without having to give up their rights to restrict their 
universes to exclude relations.

>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?

Yes, although the folding-maps MT does not in fact do this: but it 
should.  We must arrange that this is the case.  In order that the 
proof theory be rational in a case like this, then the use of a 
variable in both a relation and an object position does indeed have 
to impose the condition that any named relation be an individual. 
This requires that the notion of 'name map' used in the quantifier 
semantics be made a bit more sophisticated.  The 'simplified' model 
theory sketched in my email can be easily adapted to handle this 
(sketch below). I'll get back to you ASAP: unfortunately the rest of 
this week has been blown away by other business.

>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.

Here was the plan which was slowly forming in my mind. Headers allow 
a name to be given to an ontology/module (= the text in the body). 
This is essential for the Web, independently of any other 
considerations.  Now, suppose that we require this name *when used as 
a predicate* (with any number of arguments) to be true of things in 
the universe of discourse of the ontology. This is likely to be of 
considerable use for information interchange in any case, as it 
allows ontologies to relate their universes of discourse to those of 
other ontologies. (Currently OWL ignores this issue, which is already 
a problem.) Of course such use only makes sense in the header, since 
in the body of the text, the universe is everything and all 
quantifiers range over it.  Given this convention, it would be easy 
to say in a header

(not (<thisOntologyName> P Q R))

to indicate that P Q and R do not denote individuals (in this 
ontology). Note that this would be a denial of a tautology if written 
inside the body. In the header one could even write an axiom

(forall (x) (implies (x @z) (not ((<thisOntologyName> x)) ))

which is consistent only with GOFOL text in the body, since it 
requires any expression occurring in a relation position to denote 
something not in the universe.

In terms of the current MT, quantifiers in the header range over D, 
not over U. Quantifiers in the body text range over D or U depending 
on where the variable is located in the text: variables in relation 
position range over D, in argument position over U. (This is the 
complication I mentioned above. It amounts to treating name maps in 
exactly the same way as the denotation rules for names, which makes 
perfect sense of course.  It ensures that a quantification like your 
example 'captures' any relation names that happen to be in use, but 
still allows GOFOL text to be interpreted classically.  Without this, 
BTW, one could have a situation with sentences P and Q with
P |=/= Q
but
P & (not Q) |== false
violating the deduction theorem.)

>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!

Only because the numerals are universally accepted as having a unique 
meaning. In many languages for machine use such declarations ARE 
needed, eg the RDF use of XSD datatypes in literals (even for 
integers!) . I don't think any lexical syntax-convention like this 
will be acceptable in a Web context, where the use of URIrefs for 
identifiers is ubiquitous.

>his 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.

One can think of a header as providing the information needed to 
interface the body text with other ontologies. It does not change the 
meaning of the body text, so much as put it into a different context. 
And, to emphasize, headers are OPTIONAL: one can always transmit bare 
SCL text without any header, or just use headers to give a name to a 
module without imposing any restrictions on it.

BTW, those examples above of using the ontology name also don't 
change the meaning of any body text: they are simply SCL-inconsistent 
with any body text which is not suitably GOFOLish. They advertise the 
restriction rather than impose it. For example,
(scl:module ex:myOntology
(scl:header (not (ex:myOntology P)) )
(Q P)
)
is SCL-inconsistent (even though its body alone is consistent), as 
can be demonstrated by 'projecting' the body into the header, a 
process which requires all terms in any denoting position to be 
guarded by the ontology name:

(scl:module ex:myOntology
(scl:header
(not (ex:myOntology P))
(and (Q P) (ex:myOntology P))
))

>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:" :-)

I agree that this is the right default arrangement.

>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


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes