# Jitpro Exercises 4

Note 1: These are the first Jitpro exercises with definitions (symbols used as notations for more complex terms). For example, the symbol subset will be defined as λ x y.∀ z.z in x → z in y. To expand definitions, press the Expand Definitions button next to the formula on the branch, select the occurrences of defined symbols you want to expand, and press Use This.

Note 2: To solve some of these you will need to gave a term using a &lambda when using a forall. Use a backslash "\" to represent a λ. You may also need to indicate the type of the variable. For example, to enter λ x.x where x should have type I, give \x:I.x.

Note 3: These are the first Jitpro exercises where you can apply equations to replace equals with equals. To apply an equation of the form &forall x1 ... &forall xn . s = t to replace θ s in C[θ s] to obtain C[θ t], first select the Apply Eqn button next to the equation, next select the Replace Subterms button next to C[θ s], next select the occurrences to replace (you can replace several θ s occurrences with θ t and several θ t occurrences with θ s at the same time), and finally press Use This.

## Jitpro Exercise 4.1

Each of these problems should be easy. If they are not easy for you, please repeat them until they become easy for you!

## Jitpro Exercise 4.3: Transitive Sets

In this exercise you will prove the following are equivalent:
(1) X is a transitive set
(2) Every member of X is a subset of X
(3) X is a subset of the power set of X

Prove (1) implies (2).

Prove (2) implies (3).

Prove (3) implies (1)

## Jitpro Exercise 4.4: Power sets of transitive sets are transitive

You should do the informal proof on paper first!

## Jitpro Exercise 4.7

You need to use the Extend button for this problem.