# 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.2: Cantor's Theorem (Type Version)

## 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

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

## Jitpro Exercise 4.5: Russell's Paradox

## Jitpro Exercise 4.6: Transitivity of Equality (SUPEREASY use of the new equality rule)

## Jitpro Exercise 4.7