# Differences

This shows you the differences between two versions of the page.

 sav08:exists-forall_class_definition [2010/05/03 11:15]vkuncak sav08:exists-forall_class_definition [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2010/05/03 11:17 vkuncak 2010/05/03 11:15 vkuncak 2009/05/14 13:09 vkuncak 2008/04/03 13:42 vkuncak 2008/04/03 13:42 vkuncak 2008/04/03 13:41 vkuncak created Next revision Previous revision 2010/05/03 11:17 vkuncak 2010/05/03 11:15 vkuncak 2009/05/14 13:09 vkuncak 2008/04/03 13:42 vkuncak 2008/04/03 13:42 vkuncak 2008/04/03 13:41 vkuncak created 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,z. ListNode(x) \land ListNode(y) \land data(x,z) \land data(y,z) \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.