refreshing

eyereasoner · Dec 4, 2024 · 729c193 · 729c193
1 parent b503685
commit 729c193
Showing 1 changed file with 8 additions and 17 deletions.
diff --git a/reasoning/deontic/example1.n3s b/reasoning/deontic/example1.n3s
@@ -46,13 +46,15 @@
     _:World a :PossibleWorld.
     _:Proposition a :Proposition.
     (   1
-        {   _:World :hasAccessTo _:AccessibleWorld.
+        {
+            _:World :hasAccessTo _:AccessibleWorld.
             _:Proposition :isTrueIn _:AccessibleWorld.
         }
         _:List
     ) log:collectAllIn _:Scope.
     (   1
-        {   _:World :hasAccessTo _:AccessibleWorld.
+        {
+            _:World :hasAccessTo _:AccessibleWorld.
         }
         _:List
     ) log:collectAllIn _:Scope.
@@ -77,15 +79,17 @@
     _:World a :PossibleWorld.
     _:Proposition a :Proposition.
     (   1
-        {   _:World :hasAccessTo _:AccessibleWorld.
+        {
+            _:World :hasAccessTo _:AccessibleWorld.
             _:Scope log:notIncludes {
                 _:Proposition :isTrueIn _:AccessibleWorld.
             }
         }
         _:List
     ) log:collectAllIn _:Scope.
     (   1
-        {   _:World :hasAccessTo _:AccessibleWorld.
+        {
+            _:World :hasAccessTo _:AccessibleWorld.
         }
         _:List
     ) log:collectAllIn _:Scope.
@@ -94,19 +98,6 @@
     }.
 }.
 
-# a proposition P is forbidden in world W if P does not hold in any world accessible from W
-(_:Proposition _:World) log:onNegativeSurface {
-    _:World a :PossibleWorld.
-    _:Proposition a :Proposition.
-    (_:AccessibleWorld) log:onNegativeSurface {
-        _:World :hasAccessTo _:AccessibleWorld.
-        _:Proposition :isTrueIn _:AccessibleWorld.
-    }.
-    () log:onNegativeSurface {
-        _:Proposition :isForbiddenIn _:World.
-    }.
-}.
-
 # K axiom
 (_:Proposition1 _:Proposition2 _:World) log:onNegativeSurface {
     () log:onNegativeSurface {