LARA

Problem 1

Let be the set of all first-order formulas (viewed as syntax trees) and let be the implication relation on formulas: Check whether is reflexive, antisymmetric, and transitive relation.

Problem 2

Let be a partial order such that every set has the greatest lower bound. Prove that then every set has the least upper bound.

Problem 3

Let be the interval of real numbers. Recall that, by definition of real numbers and complete lattice, is a complete lattice with least lattice element and greatest lattice element . Here is the least upper bound operator on sets of real numbers, also called supremum and denoted sup in real analysis.

Let function be given by (It may help you to try to draw .)

Part a)

Prove that is monotonic and injective (so it is strictly monotonic).

Part b)

Compute the set of fixpoints of .

Part c)

Define . (This is in fact equal to when is a monotonic bounded function.)

Compute (prove that the computed value is correct by definition of , that is, that the value is indeed of the set of values). Is a fixpoint of ? Is a fixpoint of ? Is an -continuous function?