ϵ">]>
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 predicate R (x,y) is symmetric and transitive:
Show that the predicate is reflexive on its domain of definition:
##
Exercise. Suppose that the binary predicate R (x,y) is ireflexive and transitive:
Show that the predicate is asymmetric:
Exercise. Suppose that the binary predicate R (x,y) is symmetric and antisymmetric:
Show that the predicate is the identity on its domain of definition:
Exercise. Suppose that the binary predicate R (x,y) is equivalence:
Show that the predicate satisfies the property:
Exercise. Suppose that the binary predicate R (x,y) satisfies the property:
Show that the predicate is equivalence: