% $Id: Swell.html,v 1.1 2003/10/01 07:22:16 connolly Exp $

% foundations of Swell, the Semantic Web Logic Language
% cf http://www.w3.org/DesignIssues/
% cf http://www.w3.org/2000/07/hs78/FOPC

Swell: trait
    includes
% each property URI (with optional fragment identifer) is
% a relation from subject URIs to object URIs
% for s \< p \> o you can read: p(s, o) is true,
% or p(s, o) is a theorem.
% @@hm... do a sort of modal extension, where
% p(s, o) is asserted by a message?
        Relation(URIwf, URIwf,
         __ \< __ \> __ for __ 〈 __ 〉 __,
        bot for ⊥, top for ⊤)

    introduces
% primitives
        false_ : → URIwf
        implies_: → URIwf
        forall_ : → URIwf

        subject : → URIwf
        predicate : → URIwf
        object : → URIwf

        first: → URIwf
        rest: → URIwf
        empty: → URIwf

% it's axiomatic that for any URIwf's p,s,o, they
% form a statement.. oops! maybe not! maybe subj/obj/pred are
% acyclic!
% hmm... can I reify this operator somehow?
% using some sort of lambda thingy?
% ( (lambda x . body) y ) == http://www.w3.org/2000/07/lambda?body=urlescape(body);arg=urlescape(y)

% short-hands
        quote: URIwf, URIwf, URIwf, URIwf → Bool % quote(p, s, o, x)
        insert: URIwf, URIwf, URIwf → Bool % insert(first, rest, l)

% derived stuff

        true : → URIwf
        negation, conjunction, implication : → URIwf

        second, restrest : → URIwf

    asserts
        ∀ p, s, o, x, y, a_l, a, l: URIwf

% shorthand (hmm... could build this on n-ary predicate mechanism)
        quote(p, s, o, x) = (x \< subject \> s
                            ∧ x \< predicate \> p
                            ∧ x \< object \> o);

        insert(a, l, a_l) = (a_l \< first \> a
                            ∧ a_l \< rest \> l);

% define negation
        quote(implies_, x, false_, y)
        ⇒ x \< negation \> y;

%negation \< type \> symmetric;
        x \< negation \> y
        ⇒ y \< negation \> x;

% and here we define true:
        false_ \< negation \> true;

% and here we give an axiom for implies_ ...
% this is known as the "level breaking" axiom
        true \< implies_ \> x
        ∧ quote(p, s, o, x)
        ⇒ s \< p \> o;

% the implication of a list of statements...
        empty \< implication \> true;

        a_l \< first \>  a
        ∧ a_l \< rest \> l
        ∧ l \< implication \> s
        ∧ quote(implies_, a, s, x)
        ⇒ a_l \< implication \> x;


% define second
        s \< first \> x
        ∧ o \< rest \> x
        ⇒ s \< second \> o;

% build a conjuction from implies_, false_
        empty \< conjunction \> true;

        ∀ a, l, a_l,  s, notS,
                a_notS, impliesANotS, notImpliesANotS: URIwf

        l \< conjunction \> s
        ∧ insert(a, l, a_l)
        ∧ s \< negation \> notS
        ∧ a_notS \< first \> a
        ∧ a_notS \< second \> notS
        ∧ a_notS \< restrest \> empty
        ∧ a_notS \< implication \> impliesANotS
        ∧ impliesANotS \< negation \> notImpliesANotS
        ⇒ a_l \< conjunction \> notImpliesANotS;

[Index]

HTML generated using lsl2html.