[SCL] functions and functional relations: proposal to change the SCL semantics

[Chris Menzel]

On Thu, Feb 05, 2004 at 12:20:33AM -0600, Pat Hayes wrote:
> In SCL, however, the same symbol can be used for f and Rf, and the resulting 
> axiom IS a tautology (in the current semantics):
> (iff (= x (f y)) (f x y) )   ....... (1)
> This must be true in all interpretations, since the use of the symbol 
> in a functional position requires that it denote a functional 
> relation. In fact the general form
> (iff (= x (f @y)) (f x @y) )   .....(2)
> is a tautology also.
> ...
> Is this equivalence worth the meta-theoretic complication 
> that it produces? I suggest not, and that we should abandon it.
> 
> I can see arguments both ways.  If the thesis is to keep the status quo, 
> then:
> Pro:
> +1  it is semantically more elegant
> +2  it has been found convenient by KIF users
> Con:
> -1  it makes SCL less conventional as a first-order logic, especially 
> in its proof metatheory (eg SCL doesnt obey the deduction theorem)

You've probably show why this is so in an earlier msg, but could you indulge
me and explain (once again) what this is so?  I'm having a great deal of 
trouble believing it.

> -2  it complicates the embedding of SCL into FOL (which is 
> complicated enough already because of the treatment of =)
> -3  if we don't have it as a logical truth, then the equivalence can 
> be restored in particular cases by writing an SCL axiom, so we get 
> the practical benefit in any case.
> -4  The convention that relates function to relations is arbitrary 
> (value first or last??) and so should not be made into a logical 
> necessity.

I don't get this last argument.  Conventionality already reigns in standard
FOL:  the syntax of atomic formulas (e.g., predicates could occur last instead
of first); the syntax of boolean formulas; the number of variables that can be
bound by a single quantifier; etc.  So what if a little more conventionality
enters the picture here?  After all, it's not the *convention* that becomes a
logical necessity, it's the underlying truth; we just adopt a certain convention
about how to express it.

> Seems to me that -3 cancels +2, and that the remaining cons outweigh 
> the pros, so I propose to modify the FOL semantics so as to allow 
> functions to be distinct from relations.  (I have not yet made these 
> changes to the draft document, but will do so very soon unless anyone 
> objects strongly.)
> 
> Here's how it goes, in a sketch.  

I believe we actually considered a semantics like this some time ago.  It is ok
by me if you really think it has strong advantages, but it is not clear to me
that it does.  Rather, it seems to me that in cases where the same term being
used as both a function symbol and a predicate symbol is more likely to be a
functional relation; in fact, it's hard for me to envision the scenario you
describe in which A and B disagree over whether R indicates a function or a
relation unless there are systematic semantic connections between the two.  And
if the two uses of the term *are* completely unrelated, then why introduce a
methodology that permits the punning you suggest?  Shouldn't ambiguity be
identified and *avoided* rather than being tolerated?  I guess you wil respond
with your point about negotiation:

> This satisfies both A and B, but leaves them some room to negotiate further
> on what connection, if any, there might be between their interpretations of
> the symbol.

But if there is none, why permit the ambiguity to remain?  The existing
methodology seems to take the opposite tack -- use the same term as both
function sym and relation sym only if they have a certain close semantic
connection.  Otherwise, choose different symbols.

> The meta-theoretic gains of this change are considerable, and the 
> above story seems to provide a reasonable justification for the 
> slight extra semantic complication (which is in fact very minimal 
> when written out carefully). 

Probably so, and (though I reserve the right to do a 180 on this! :-) the
metatheoretic simplicity is probably worth the loss of elegance.

-chris