Clausal Language (ver. 5.81.20, 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. 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 relation $A (x, y)$ is symmetric and transitive:

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

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

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

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

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

\forall x \neg A (x, x)

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

Show that the relation is asymmetric:

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

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

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

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

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

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

Query:

Heap used: 187700 free: 134028440

Time used: 0:0:1:0