Stratification Axioms

I wrote up a simple demonstration of stratification which can be used
with an RDF negation vocabulary to keep things well-defined in the
face of self-reference.     The syntax is Otter's.

   -- sandro

================

%
%  RDF Negation defined with a class (lx_FalseSentence) and
%  three predicates (lx_subject, lx_predicate, lx_object).
%
%  We turn self-reference paradoxes into contradictions by 
%  declarating that these sentences are stratified; that is
%  sentences are always "higher" than their parts.
%
%  Alas, I have not been able to prove these axioms consistent!
%
%  The general problem I'm working on is discussed in 
%  http://lists.w3.org/Archives/Public/www-rdf-logic/2002Sep/0013.html
%


%
%   Connect -rdf with its reification
%

all X Y Z (
  (exists S (
    rdf(S, rdf_type, lx_FalseSentence) &
    rdf(S, lx_subject, X) &
    rdf(S, lx_predicate, Y) &
    rdf(S, lx_object, Z)
  ))
  <->
  -rdf(X, Y, Z)
).

%
%   Stratify sentences (anything which describes
%   a looping sentence is false).
%

%% A sentence is higher than its parts

all S P (
  rdf(S, lx_subject, P) 
  ->  
  higher(S, P)
).

all S P (
  rdf(S, lx_predicate, P) 
  ->  
  higher(S, P)
).

all S P (
  rdf(S, lx_object, P) 
  ->  
  higher(S, P)
).

%% "higher" is antisymmtric (like greater-than)

all S1 S2 (
  higher(S1, S2) -> -higher(S2, S1)
).

%% "higher" is transitive (like greater-than)

all S1 S2 S3 (
  higher(S1, S2) &
  higher(S2, S3) 
  -> 
  higher(S1, S3)
).


%
% There might be a kind of empty or singleton universe where this would be
% consistent.  Am I interested in that kind?
%

rdf(c1,c1,c1).
-rdf(c2,c2,c2).

%%   %
%%   % Example 1
%%   %
%%   
%%   % indirectly assert -rdf(a,b,c)
%%   rdf(s, lx_subject, a).
%%   rdf(s, lx_predicate, b).
%%   rdf(s, lx_object, c).
%%   rdf(s, rdf_type, lx_FalseSentence).
%%   
%%   % directly assert(a,b,c)
%%   rdf(a,b,c).
%%   
%%   ---------------- PROOF ----------------
%%   
%%   1 [] -rdf(A,rdf_type,lx_FalseSentence)| -rdf(A,lx_subject,B)| 
%%        -rdf(A,lx_predicate,C)| -rdf(A,lx_object,D)| -rdf(B,C,D).
%%   16 [] rdf(s,lx_subject,a).
%%   17 [] rdf(s,lx_predicate,b).
%%   18 [] rdf(s,lx_object,c).
%%   19 [] rdf(s,rdf_type,lx_FalseSentence).
%%   20 [] rdf(a,b,c).
%%   777 [hyper,20,1,19,16,17,18] $F.
%%   


%%   %
%%   % Example 2
%%   %
%%
%%   % describe a self-reference loop of size 9
%%   rdf(a, lx_subject, b).
%%   rdf(b, lx_subject, c).
%%   rdf(c, lx_subject, d).
%%   rdf(d, lx_subject, e).
%%   rdf(e, lx_subject, f).
%%   rdf(f, lx_subject, g).
%%   rdf(g, lx_subject, h).
%%   rdf(h, lx_subject, i).
%%   rdf(i, lx_subject, a).
%%   
%%   
%%   ---------------- PROOF ----------------
%%   
%%   6 [] -rdf(S,lx_subject,P)|higher(S,P).
%%   9 [] -higher(S1,S2)| -higher(S2,S1).
%%   10 [] -higher(S1,S2)| -higher(S2,S3)|higher(S1,S3).
%%   11 [] rdf(a,lx_subject,b).
%%   12 [] rdf(b,lx_subject,c).
%%   13 [] rdf(c,lx_subject,d).
%%   14 [] rdf(d,lx_subject,e).
%%   15 [] rdf(e,lx_subject,f).
%%   16 [] rdf(f,lx_subject,g).
%%   17 [] rdf(g,lx_subject,h).
%%   18 [] rdf(h,lx_subject,i).
%%   19 [] rdf(i,lx_subject,a).
%%   20 [hyper,11,6] higher(a,b).
%%   37 [hyper,12,6] higher(b,c).
%%   55 [hyper,37,10,20] higher(a,c).
%%   56 [hyper,13,6] higher(c,d).
%%   74 [hyper,56,10,55] higher(a,d).
%%   76 [hyper,14,6] higher(d,e).
%%   95 [hyper,76,10,74] higher(a,e).
%%   97 [hyper,15,6] higher(e,f).
%%   116 [hyper,97,10,95] higher(a,f).
%%   119 [hyper,16,6] higher(f,g).
%%   139 [hyper,119,10,116] higher(a,g).
%%   142 [hyper,17,6] higher(g,h).
%%   162 [hyper,142,10,139] higher(a,h).
%%   166 [hyper,18,6] higher(h,i).
%%   187 [hyper,166,10,162] higher(a,i).
%%   191 [hyper,19,6] higher(i,a).
%%   226 [hyper,191,9,187] $F.
%%

Received on Thursday, 12 September 2002 16:02:55 UTC