Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:exists-forall_class_definition [2009/05/14 13:09] vkuncak |
sav08:exists-forall_class_definition [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Exists-Forall Class Definition ====== | + | ====== Exists-Forall Class (EPR, BSR) Definition ====== |
Also called [[wp>Paul Bernays|Berneys]]-[[wp>Schoenfinkel]] class and Effectively Propositional Logic (EPR). | Also called [[wp>Paul Bernays|Berneys]]-[[wp>Schoenfinkel]] class and Effectively Propositional Logic (EPR). | ||
Line 14: | Line 14: | ||
For binary relations $r,s,t$ to express $r \circ s \subseteq t$, we can introduce binary relation symbols $R$, $S$, $T$ and write formula | For binary relations $r,s,t$ to express $r \circ s \subseteq t$, we can introduce binary relation symbols $R$, $S$, $T$ and write formula | ||
- | \[ | + | \begin{equation*} |
\forall x, y, z. R(x,y) \land S(y,z) \rightarrow T(x,z) | \forall x, y, z. R(x,y) \land S(y,z) \rightarrow T(x,z) | ||
- | \] | + | \end{equation*} |
To express $r^{-1} = r$ we would write | To express $r^{-1} = r$ we would write | ||
- | \[ | + | \begin{equation*} |
\forall x, y. R(x,y) \leftrightarrow R(y,x) | \forall x, y. R(x,y) \leftrightarrow R(y,x) | ||
- | \] | + | \end{equation*} |
List contains no duplicates: | List contains no duplicates: | ||
- | \[ | + | \begin{equation*} |
- | \forall x,y. ListNode(x) \land ListNode(y) \land data(x) = data(y) \rightarrow x=y | + | \forall x,y,z. ListNode(x) \land ListNode(y) \land data(x,z) \land data(y,z) \rightarrow x=y |
- | \] | + | \end{equation*} |
Relation $r$ is a partial function | Relation $r$ is a partial function | ||
- | \[ | + | \begin{equation*} |
\forall x, y_1, y_1. R(x,y_1) \land R(x,y_2) \rightarrow y_1=y_2 | \forall x, y_1, y_1. R(x,y_1) \land R(x,y_2) \rightarrow y_1=y_2 | ||
- | \] | + | \end{equation*} |
We **cannot** express in this class that $R$ is a total function, or property like $\forall x. \exists y. R(x,y)$ because we need an existential quantifier after a universal one. | We **cannot** express in this class that $R$ is a total function, or property like $\forall x. \exists y. R(x,y)$ because we need an existential quantifier after a universal one. | ||