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.
Each of these problems should be easy. If they are not easy for you, please repeat them until they become easy for you!
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