blob: fef66885e1ca9788beb082ed2911eee8575096b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
--# -path=.:englishExtended
abstract HigherOrder = Merge ** {
fun SingleValuedRelation : (c : Class) -> (El c -> Formula) -> Formula;
def SingleValuedRelation c f = forall c (\x -> forall c (\y -> impl (and (f (var c c ? x)) (f (var c c ? y))) (equal (var c Entity ? x) (var c Entity ? y))));
fun AntisymmetricRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def AntisymmetricRelation c f = forall c (\x -> forall c (\y -> impl (and (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? x))) (equal (var c Entity ? x) (var c Entity ? y))));
fun IntentionalRelation : (c1,c2 : Class) -> (El c1 -> El c2 -> Formula) -> Formula ;
def IntentionalRelation c1 c2 f = forall c1 (\x -> forall c2 (\y -> inScopeOfInterest (var c1 CognitiveAgent ? x) (var c2 Entity ? y)));
-- assume binary predicate, since it is mostly used for that
fun ReflexiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def ReflexiveRelation c f = forall c (\x -> f (var c c ? x) (var c c ? x));
fun SymmetricRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def SymmetricRelation c f = forall c (\x -> forall c(\y -> impl (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? x))));
fun EquivalenceRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def EquivalenceRelation c f = and (and (ReflexiveRelation c f) (SymmetricRelation c f)) (TransitiveRelation c f);
fun TransitiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def TransitiveRelation c f = forall c (\x -> forall c (\y -> forall c(\z -> impl (and (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? z))) (f (var c c ? x) (var c c ? z)))));
fun IrreflexiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def IrreflexiveRelation c f = forall c (\x -> not (f (var c c ? x) (var c c ? x)));
fun AsymmetricRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def AsymmetricRelation c f = and (AntisymmetricRelation c f) (IrreflexiveRelation c f);
fun PropositionalAttitude : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def PropositionalAttitude c f = (AsymmetricRelation c f);
fun ObjectAttitude : (c1,c2 : Class) -> (El c1 -> El c2 -> Formula) -> Formula ;
def ObjectAttitude c1 c2 f = IntentionalRelation c1 c2 f ;
fun IntransitiveRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def IntransitiveRelation c f = forall c (\x -> forall c (\y -> forall c(\z -> impl (and (f (var c c ? x) (var c c ? y)) (f (var c c ? y) (var c c ? z))) (not (f (var c c ? x) (var c c ? z))))));
fun PartialOrderingRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def PartialOrderingRelation c f = and (and (TransitiveRelation c f) (AntisymmetricRelation c f)) (ReflexiveRelation c f);
fun TrichotomizingRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def TrichotomizingRelation c f = forall c (\x -> forall c (\y ->
or
(or
(and
(and (f (var c c ? x) (var c c ? y))
(not (equal (var c Entity ? x) (var c Entity ? y))))
(not (f (var c c ? y) (var c c ? x))))
(and
(and (not (f (var c c ? x) (var c c ? y)))
(equal (var c Entity ? x) (var c Entity ? y)))
(not (f (var c c ? y) (var c c ? x)))))
(and
(and (f (var c c ? y) (var c c ? x))
(not (equal (var c Entity ? x) (var c Entity ? y))))
(not (f (var c c ? x) (var c c ? y))))));
fun TotalOrderingRelation : (c : Class) -> (El c -> El c -> Formula) -> Formula ;
def TotalOrderingRelation c f = and (PartialOrderingRelation c f) (TrichotomizingRelation c f) ;
fun OneToOneFunction : (c1, c2 : Class) -> (El c1 -> Ind c2) -> Formula ;
def OneToOneFunction c1 c2 f = forall c1(\x ->
forall c1(\y -> impl (not(equal (var c1 Entity ? x) (var c1 Entity ? y))) (not (equal (el c2 Entity ? (f (var c1 c1 ? x))) (el c2 Entity ? (f (var c1 c1 ? y)))))));
fun SequenceFunction : (c : Class) -> (El Integer -> Ind c) -> Formula ;
def SequenceFunction c f = OneToOneFunction Integer c f ;
fun AssociativeFunction : (c : Class) -> (El c -> El c -> Ind c) -> Formula ;
def AssociativeFunction c f = forall c(\x ->
forall c(\y ->
forall c(\z -> equal (el c Entity ? (f (var c c ? x) (el c c ? (f (var c c ? y) (var c c ? z))))) (el c Entity ? (f (el c c ? (f (var c c ? x) (var c c ? y))) (var c c ? z))))));
fun CommutativeFunction : (c1,c2 : Class) -> (El c1 -> El c1 -> Ind c2) -> Formula ;
def CommutativeFunction c1 c2 f = forall c1 (\x ->
forall c1 (\y ->
equal (el c2 Entity ? (f (var c1 c1 ? x) (var c1 c1 ? y))) (el c2 Entity ? (f (var c1 c1 ? y) (var c1 c1 ? y)))));
fun identityElement : (c : Class) -> (El c -> El c -> Ind c) -> El c -> Formula ;
def identityElement c f elem = forall c(\x -> equal (el c Entity ? (f (var c c ? x) elem)) (var c Entity ? x));
fun distributes : (c : Class) -> (El c -> El c -> Ind c) -> (El c -> El c -> Ind c) -> Formula ;
def distributes c f g = forall c (\x -> forall c (\y -> forall c (\z -> equal (el c Entity ? (g (el c c ? (f (var c c ? x) (var c c ? y))) (var c c ? z))) (el c Entity ? (f (el c c ? (g (var c c ? x) (var c c ? z))) (el c c ? (g (var c c ? y) (var c c ? z))))))));
fun inverse : (c : Class) -> (El c -> El c -> Formula) -> (El c -> El c -> Formula) -> Formula ;
def inverse c f g = forall c (\x -> forall c (\y -> equiv (f (var c c ? x) (var c c ? y)) (g (var c c ? y) (var c c ? x))));
fun subRelation2El : (c1,c2,c3,c4 : Class) -> (El c1 -> El c2 -> Formula) -> (El c3 -> El c4 -> Formula) -> Formula ;
def subRelation2El c1 c2 c3 c4 f g = forall c1 (\x -> forall c2 (\y -> impl (f (var c1 c1 ? x) (var c2 c2 ? y)) (g (var c1 c3 ? x) (var c2 c4 ? y))));
fun KappaFn : (c : Class) -> (Ind c -> Formula) -> Class ;
};
|
