Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Chapter. Quantification Logic.

Section. Quantification Tableaux.

[CL] Remark. The module Mlogicq in the file mlogicq.cl contains the syntax of tableau rules for quantifier tableaux.

Exercise. Prove the following sentence:

\exists y \forall x R (x, y) \to \forall x \exists y R (x, y)

\exists y \forall x R (x, y) \to \forall x \exists y R (x, y)

Exercise. Prove the following sentences:

\exists x (A (x) \land B (x)) \to \exists x A (x) \land \exists x B (x)

\forall x A (x) \lor \forall x B (x) \to \forall x (A (x) \lor B (x))

\neg \exists x A (x) \leftrightarrow \forall x \neg A (x)

\exists x (A (x) \land B (x)) \to \exists x A (x) \land \exists x B (x)

\forall x A (x) \lor \forall x B (x) \to \forall x (A (x) \lor B (x))

\neg \exists x A (x) \leftrightarrow \forall x \neg A (x)

Section. Logical Consequence.

[CL] Remark. In the following examples you can use derived quantifier tableau rules as described in the module Mlogicd (see the file mlogicd.cl).

Exercise. Suppose that the binary predicate $R (x, y)$ is symmetric and transitive:

\forall x \forall y (R (x, y) \to R (y, x))

\forall x \forall y \forall z (R (x, y) \land R (y, z) \to R (x, z))

Show that the predicate is reflexive on its domain of definition:

\forall x (\exists y R (x, y) \to R (x, x))

Exercise. Suppose that the binary predicate $R (x, y)$ is ireflexive and transitive:

\forall x \neg R (x, x)

\forall x \forall y \forall z (R (x, y) \land R (y, z) \to R (x, z))

Show that the predicate is asymmetric:

\forall x \forall y (R (x, y) \to \neg R (y, x))

Exercise. Suppose that the binary predicate $R (x, y)$ is symmetric and antisymmetric:

\forall x \forall y (R (x, y) \to R (y, x))

\forall x \forall y (R (x, y) \land R (y, x) \to x = y)

Show that the predicate is the identity on its domain of definition:

\forall x \forall y (R (x, y) \to x = y)

Exercise. Suppose that the binary predicate $R (x, y)$ is equivalence:

\forall x R (x, x)

\forall x \forall y (R (x, y) \to R (y, x))

\forall x \forall y \forall z (R (x, y) \land R (y, z) \to R (x, z))

Show that the predicate satisfies the property:

\forall x \forall y (R (x, y) \leftrightarrow \forall z (R (x, z) \leftrightarrow R (y, z)))

Exercise. Suppose that the binary predicate $R (x, y)$ satisfies the property:

\forall x \forall y (R (x, y) \leftrightarrow \forall z (R (x, z) \leftrightarrow R (y, z)))

Show that the predicate is equivalence:

\forall x R (x, x)

\forall x \forall y (R (x, y) \to R (y, x))

\forall x \forall y \forall z (R (x, y) \land R (y, z) \to R (x, z))