Re: FO semantics for condition language (Action 84)

Peter F. Patel-Schneider wrote:
> 
> This proposal is nothing more than a simple modification to standard
> first-order semantics to account for the syntax of the condition language.
> 
> 
> 
>    A Proposal for a First-Order Semantics for the Condition Language
> 
> I propose that the semantics for the condition language be based (solely)
> on a standard first-order semantics.
> 
> The syntax for condition language (with negation) is:
> 
>  Data     ::= value
>  Ind      ::= object
>  Var      ::= '?' name
>  TERM     ::= Data | Ind | Var | Expr
>  Expr     ::= Fun '(' TERM* ')'
>  Atom     ::= Rel '(' TERM* ')' | TERM '=' TERM
>  LITFORM  ::= Atom
>  QUANTIF  ::= 'Exists' Var+ '(' CONDIT ')'
>  CONJ     ::= 'And' '(' CONDIT* ')'
>  DISJ     ::= 'Or' '(' CONDIT* ')'
>  CONDIT   ::= LITFORM | QUANTIF | CONJ | DISJ
>  LITFORM ::= Atom | 'Neg' Atom | 'Naf' Atom | 'Naf' 'Neg' Atom
> 
> The semantics for this condition language are essentially compatible with
> the standard semantics for first-order logic.
> 
> More formally:
> 
> 
> Let D be a non-empty set (of domain elements), divided into DD (data) 
> and DI (non-data).
> 
> Let Data be the set of syntax elements recognized by the Data / value 
> production,
>    Ind be the set of syntax elements recognized by the Ind / object 
> production,
>    Var be the set of syntax elements recognized by the Var / ?name 
> production,
>    Fun be the set of syntax elements recognized by the Fun production,
>    Rel be the set of syntax elements recognized by the Rel production.
> 
> An interpretation I is then five mappings
>    ID from Data to elements of DD
>    II from Ind to elements of DI
>    IV from Var to elements of D
>    IF from Fun to functions from D* into D
>    IR from Rel to subsets of D*
> 
> Interpretations are extended to terms as follows:
>    I(v) = ID(v)     for v a value
>    I(o) = II(o)    for o an object
>    I(?v) = IV(?v)    for v a variable
>    I(f(t1,...,tn)) = I(f)(I(t1),...,I(tn))
> 
> An interpretation satisfies a piece of syntax as follows
>    I satisfies R(t1,...,tn)    iff    < I(t1),...,I(tn) > is in IR(R)
>    I satisfies t1  = t2        iff    I(t1) = I(t2)
>    I satisfies Neg a        iff    I does not satisfy a
>    I satisfies Naf a        iff    I does not satisfy a

Hmmm, this looks strange to me... It makes no difference between naf and 
neg, hmmmm...

Actually, as far as I know, the difference depends on what 
interpretations 'I' looks like, if you allow only classical models, then 
there is not really a difference...

But formalisations for different semantics for naf have different 
non-classical logics underneath (and there are several approaches for 
which logics to use) with multivalued models:

Particularly, LEM law of the excluded middle which is an axiom in 
standard first-order semantics) does not necessarily hold, i.e. models 
are not necessarily 'total'.

The "least commitment" semantics where LEM doesn't hold is AFAIK 
intuitionistic logics... Actually, with for instance Gerd we have 
experts on this issue in our WG, who will hopefully be able to help more 
on clarifications here:

I suggested in the Teleconf to give a try to clarify these matters a bit 
more in a separate wiki-page, would appreciate help/comments of course!


axel

>    I satisfies Naf Neg a        iff    I satisfies a

Rather:  I satisfies Naf Neg a        iff    I does not satisfy neg a


>    I satisfies And(c1,...,cn)    iff    I satisfies ci for each 1<=i<=n
>    I satisfies Or(c1,...,cn)    iff    I satisfies ci for some 1<=i<=n
>    I satisfies Exists v1 ... vn c    iff    there is some I* that
>                        agrees with I except for
>                        the mappings of v1 ... vn
>                        and I* satisfies c       
> Built-ins are handled by requiring that interpretations have to be
> compatible with the intended interpretation of the built-in Fun or Rel.
> This can be used to handle ontologies as well.
> 
> Note 1:  The condition language may need to be tweaked somewhat as it
> currently divides constants between data and individuals, but does not so
> divide variables or functions.
> 
> Note 2:  This treatment pushes variables into the interpretation itself,
> which is not the most common treatment, but works just the same.  If
> someone cares, the treatment can easily be changed to the other way.



-- 
Dr. Axel Polleres
email: axel@polleres.net  url: http://www.polleres.net/

Received on Tuesday, 29 August 2006 16:34:13 UTC