Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
sav08:exists-forall_class_definition [2008/04/03 13:41] vkuncak created |
sav08:exists-forall_class_definition [2010/05/03 11:17] vkuncak |
||
|---|---|---|---|
| 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). | ||
| Notation according to [[Classical Decision Problem]] classification: $[\exists^* \forall^*,all,(0)]_{=}$ | Notation according to [[Classical Decision Problem]] classification: $[\exists^* \forall^*,all,(0)]_{=}$ | ||
| Line 9: | Line 11: | ||
| * no function symbols | * no function symbols | ||
| - | === Example === | + | ===== Examples ===== |
| 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 | ||
| Line 21: | Line 23: | ||
| \] | \] | ||
| - | Relation $r$ is a partial function | + | List contains no duplicates: |
| \[ | \[ | ||
| - | \forall x, y_1, y_1. R(x,y_1) \land R(x,y_2) \rightarrow y_1=y_2 | + | \forall x,y,z. ListNode(x) \land ListNode(y) \land data(x,z) \land data(y,z) \rightarrow x=y |
| \] | \] | ||
| - | List contains no duplicates: | + | Relation $r$ is a partial function |
| \[ | \[ | ||
| - | \forall x,y. ListNode(x) \land ListNode(y) \land data(x) = data(y) \rightarrow x=y | + | \forall x, y_1, y_1. R(x,y_1) \land R(x,y_2) \rightarrow y_1=y_2 |
| \] | \] | ||
| + | |||
| + | 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. | ||