WFF Sort | Interpretation (WFF^I ) |
---|---|
a | a^I \in \Delta |
A | A^I \subseteq \Delta |
P | P^I \subseteq \Delta\times\Delta |
\neg C | \Delta\setminus C^I |
C \sqcap D | C^I \cap D^I |
C \sqcup D | C^I \cup D^I |
\exists P.C | \{x \in \Delta | \exists(y)(<x,y> \in P^I \land y \in C^I)\} |
\forall P.C | \{x \in \Delta | \forall(y)(<x,y> \in P^I \rightarrow y \in C^I)\} |
WFF Sort | Interpretation (WFF^I ) |
---|---|
C \sqsubseteq D | C^I \subseteq D^I |
C \sqsubseteq D | C^I \subseteq D^I and C^I \subseteq D^I |
a:C | a^I \in C^I |
<a, b>:P | <a^I, b^I> \in P^I |
NOTE: These all evaluate to True or False!
'abba'
as \[a1\!:\!A.\quad a2\!:\!A. \quad b1\!:\!B.\quad b2\!:\!B.\]\[<\!a1,b1\!>:next.\quad <\!b1,b2\!>:next. \quad<\!b2,a1\!>:next.\]'abba'
DL | FOL |
A | A(x) |
\neg C | \neg (Tr(C, x)) |
C \sqcap D | Tr(C, x) \land Tr(D, x) |
C \sqcup D | Tr(C, x) \lor Tr(D, x) |
P | Tr(P, x, y) |
\forall P.C | \forall(y^{new})(Tr(P(x, y^{new}) \rightarrow Tr(C, y^{new})) |
\exists P.C | \exists(y^new{new})(Tr(P(x, y^new) \land Tr(C, y^{new})) |
a:C, <a, b>:P | C(a), P(a,b) |
A \equiv C | \forall(x)(Tr(A, x) \leftrightarrow Tr(C, x)) |
DL | FOL |
A | A(var) |
\neg C | \neg (Tr(C, var)) |
C \sqcap D | Tr(C, var) \land Tr(D, var) |
C \sqcup D | Tr(C, var) \lor Tr(D, var) |
P | Tr(P, var, var') |
\forall P.C | \forall(var')(Tr(P(var, var') \rightarrow Tr(C, var')) |
\exists P.C | \exists(var')(Tr(P(var, var') \land Tr(C, var')) |
a:C, <a, b>:P | C(a), P(a,b) |
A \equiv C | \forall(\textbf{x})(Tr(A, \textbf{x}) \leftrightarrow Tr(C, \textbf{x})) |