Types

We consider three kinds of types.

Propositions

Tableau Refutations

A branch is a finite set of propositions. We say a proposition is on the branch if it is in the set.
A branch is closed if one of the following holds:
  • False is on the branch.
  • ¬ True is on the branch.
  • ¬ (s = s) is on the branch.
  • Both P and ¬ P are on the branch.
    • Various rules corresponding to logical operators allow one to refute a branch by refuting extended branches. Closed branches are considered refuted. Theorems are proven by adding the negation to a branch and then refuting the branch.
    We give rules as they are needed for examples.
    Rule (Negated Implication) If ¬ (P → Q) is on the branch, then we can extend the branch with P and ¬ Q.
    Example: Prove ¬ ¬ P → P by refuting the branch with the negation of the formula.
    Try to prove it yourself. Double Negation Example
    Rule (Implication) If P → Q is on the branch, then we can split into two subgoals to refute given by two extended branches: one extended by Q and the other extended by ¬ P
    Example: Prove ((P → Q) → P) → P by refuting the branch with the negation of the formula.
    Try to prove it yourself. Peirce Law Example
    Rule (And) If P ∧ Q is on the branch, then the branch can be extended with P and Q.
    Rule (NegAnd) If ¬ (P ∧ Q) is on the branch, then we can split into two subgoals to refute given by two extended branches: one extended by ¬ P and the other extended by ¬ Q.
    Rule (Remove Double Negation) If ¬ ¬ P is on the branch, then we can extend the branch with P.
    Example: Prove ¬ ¬ P ∧ ¬ ¬ Q → Q ∧ P by refuting the branch with the negation of the formula.
    Try to prove it yourself. Conjunction Example
    Rule (Or) If P ∨ Q is on the branch, then we can split into two subgoals to refute given by two extended branches: one extended by P and the other extended by Q.
    Rule (NegOr) If ¬ (P ∨ Q) is on the branch, then the branch can be extended with ¬ P and ¬ Q.
    Example: Prove P ∨ Q → Q ∨ P by refuting the branch with the negation of the formula.
    Try to prove it yourself. Disjunction Example
    The examples above are intended to be very easy. A short video showing all four being done is here in mp4 and webm formats.

    Terms of Function Type

    s [x := t] is the term resulting from substituting t for x (avoiding capture of bound variables when by changing the names of bound variables when necessary).
    When a lambda abstraction is applied to a term, we can β-reduce it by substituting the argument for the λ-bound variable.
    That is, (λ x.s) t β-reduces to s [x := t].
    We often write (λ x ... y.s) for several λ-abstractions in a row: (λ x ... λ y.s).

    Sets

    Object. The name In is a term of type set → set → prop. If s and t have type set, then In s t has type prop. We usually write s ∈ t for In s t. That is, we use ∈ as an infix operator corresponding to applying In. Furthermore, we may write ∀ x ∈ A. P to mean ∀ x : set. x ∈ A → P and write ∃ x ∈ A. P to mean ∃ x : set. x ∈ A ∧ P
    Definition. We define Subq to be λA B ⇒ ∀x ∈ A, x ∈ B of type set → set → prop.
    Notation. We use ⊆ as an infix operator corresponding to applying term Subq. Furthermore, we may write ∀ x ⊆ A, B to mean ∀ x : set, x ⊆ A → B.
    Definition. We define nIn to be λx X ⇒ ¬ In x X of type set → set → prop.
    Notation. We use ∉ as an infix operator corresponding to applying term nIn.

    Theorem: setminus is antimonotone.

    Object. The name setminus is a term of type set → set → set.
    Notation. We use ∖ as an infix operator corresponding to applying term setminus.
    Known. (setminusI)
    ∀X Y z, (z ∈ X) → (z ∉ Y) → z ∈ X ∖ Y
    Known. (setminusE)
    ∀X Y z, (z ∈ X ∖ Y) → z ∈ X ∧ z ∉ Y
    Theorem. (setminus_antimonotone) The following is provable:
    ∀A U V, U ⊆ V → A ∖ V ⊆ A ∖ U
    Try to prove it yourself. You will need to know about two more rules:
    Rule (Forall) If x has type α and ∀ x. P is on the branch, then the branch can be extended with P [x := t] whenever t has type α. Here P [x := t] is the result of substituting t for x (avoiding capture of bound variables when by changing the names of bound variables when necessary).
    Rule (NegForall) If x has type α and ¬ ∀ x. P is on the branch, then the branch can be extended with ¬ P [x := y] where y is a variable not occurring free on the branch. A special case is when x and y are the same variable. A special rule (NegForall*) can be applied to do several (NegForall) rules if the x and y are the same in each case.
    Prove setminus is antimonotone.
    A short video showing this theorem being proven is available in mp4 and webm formats.

    Theorem: Image is monotone.

    Object. The name Repl is a term of type set → (set → set) → set.
    Notation. {B| x ∈ A} is notation for Repl A (λ x . B).
    Known. (ReplI)
    ∀A : set, ∀F : set → set, ∀x : set, x ∈ A → F x ∈ {F x|x ∈ A}
    Note that {F x|x ∈ A} is notation for Repl A (λ x.F x) which η-reduces to Repl A F.
    Known. (ReplE)
    ∀A : set, ∀F : set → set, ∀y : set, y ∈ {F x|x ∈ A} → ∃x ∈ A, y = F x
    Theorem. (image_monotone) The following is provable:
    ∀f : set → set, ∀U V, U ⊆ V → {f x|x ∈ U} ⊆ {f x|x ∈ V}
    Try to prove it yourself. You may need a few more rules:
    Rule (Exists) If x has type α and ∃ x. P is on the branch, then the branch can be extended with P [x := y] where y is a variable not occurring free on the branch. A special case is when x and y are the same variable. A special rule (Exists*) can be applied to do several (Exists) rules if the x and y are the same in each case.
    Rule (NegExists) If x has type α and ¬ ∃ x. P is on the branch, then the branch can be extended with ¬ P [x := t] where t has type α.
    Rule (Apply Eqn) If s = t is on the branch and s (or t) occurs in a proposition on the branch, then the occurence can be replaced by t (or s).
    Prove image is monotone.
    A short video showing this theorem being proven is available in mp4 and webm formats.

    Theorem: Image is in power set.

    Object. The name 𝒫 is a term of type set → set.
    Known. (PowerI)
    ∀X Y : set, Y ⊆ X → Y ∈ 𝒫 X
    Known. (PowerE)
    ∀X Y : set, Y ∈ 𝒫 X → Y ⊆ X
    Theorem. (image_In_Power) The following is provable:
    ∀A B, ∀f : set → set, (∀x ∈ A, f x ∈ B) → ∀U ∈ 𝒫 A, {f x|x ∈ U} ∈ 𝒫 B
    Try to prove it yourself. Prove image is in power set.
    A short video showing this theorem being proven is available in mp4 and webm formats.

    Theorem: Knaster Tarski Fixed Point

    We start by introducing a new known proposition: set extensionality. Two sets are equal if they are included in each other.
    Known. (set_ext)
    ∀X Y : set, X ⊆ Y → Y ⊆ X → X = Y
    We next consider an operation which separates out the elements of a set satisfying a property.
    Object. The name Sep is a term of type set → (set → prop) → set.
    Notation. {x ∈ A | B} is notation for Sep A (λ x . B).
    Known. (SepI)
    ∀X : set, ∀P : (set → prop), ∀x : set, x ∈ X → P x → x ∈ {x ∈ X|P x}
    Known. (SepE1)
    ∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → x ∈ X
    Known. (SepE2)
    ∀X : set, ∀P : (set → prop), ∀x : set, x ∈ {x ∈ X|P x} → P x
    Known. (Sep_In_Power)
    ∀X : set, ∀P : set → prop, {x ∈ X|P x} ∈ 𝒫 X
    Known. (setminus_In_Power)
    ∀A U, A ∖ U ∈ 𝒫 A
    Theorem. (KnasterTarski_set) The following is provable:
    ∀A, ∀Φ : set → set, (∀U ∈ 𝒫 A, Φ U ∈ 𝒫 A) → (∀U V ∈ 𝒫 A, U ⊆ V → Φ U ⊆ Φ V) → ∃Y ∈ 𝒫 A, Φ Y = Y
    Proof:
    Let A and Φ be given.
    Assume Φ is a monotone function from the power set of A to the power set of A.
    We say X is a pre-fixed point if Φ X ⊆ X. We define Y to be the intersection of all pre-fixed points, giving the least pre-fixed point.
    Let Y be {u ∈ A|∀ X ∈ 𝒫 A . Φ X ⊆ X → u ∈ X}.
    • It is easy to prove Φ Y ⊆ Y. (Let u in Φ Y be given. To prove u ∈ Y, we must prove u ∈ X whenever X is a pre-fixed point. Let X be a pre-fixed point. Since Y ⊆ X and X is a pre-fixed point, Φ Y ⊆ Φ X ⊆ X and so u is in X.)
    • Using this, it is easy to prove Y ⊆ Φ Y. (By monotonicity and Φ Y ⊆ Y we have Φ (Φ Y) ⊆ Φ Y. That is, Φ Y is a pre-fixed point. Since Y is the least pre-fixed point, we have Y ⊆ Φ Y.)
    • By set extensionality Φ Y = Y as desired.
    ∎
    Try to prove it yourself.
    In each problem below we give an fp defined such that fp A Φ corresponds to the Y above, i.e., {u ∈ A|∀X ∈ 𝒫 A, Φ X ⊆ X → u ∈ X} of type set. We define fp using lpfp defined such that lpfp A Φ u corresponds to ∀X ∈ 𝒫 A, Φ X ⊆ X → u ∈ X so that fp A Φ is {u ∈ A|lpfp A Φ u}
    Three short videos show these subgoals and the main goal being proven are available:
    • Subgoal 1 in mp4 and webm formats.
    • Subgoal 2 in mp4 and webm formats.
    • Main Goal in mp4 and webm formats.

    Theorem: Schroeder Bernstein

    Definition. We define inj to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) of type set → set → (set → set) → prop.
    Definition. We define bij to be λX Y f ⇒ (∀u ∈ X, f u ∈ Y) ∧ (∀u v ∈ X, f u = f v → u = v) ∧ (∀w ∈ Y, ∃u ∈ X, f u = w) of type set → set → (set → set) → prop.
    Definition. We define equip to be λX Y : set ⇒ ∃f : set → set, bij X Y f of type set → set → prop.
    Object. The name If_i is a term of type prop → set → set → set.
    Notation. if cond then T else E is notation corresponding to If_i cond T E.
    Known. (If_i_1)
    ∀p : prop, ∀x y : set, p → (if p then x else y) = x
    Known. (If_i_0)
    ∀p : prop, ∀x y : set, ¬ p → (if p then x else y) = y
    Object. The name inv is a term of type set → (set → set) → set → set.
    Known. (inj_linv)
    ∀X, ∀f : set → set, (∀u v ∈ X, f u = f v → u = v) → ∀x ∈ X, inv X f (f x) = x
    Theorem. (SchroederBernstein) The following is provable:
    ∀A B, ∀f g : set → set, inj A B f → inj B A g → equip A B
    Proof:
    Let A, B, f and g such that inj A B f and inj B A g be given.
    Let Φ be λX ⇒ {g y|y ∈ B ∖ {f x|x ∈ A ∖ X}} of type set → set.
    We can prove the following two claims:
    • ∀U ∈ 𝒫 A, Φ U ∈ 𝒫 A.
    • ∀U V ∈ 𝒫 A, U ⊆ V → Φ U ⊆ Φ V.
    Hence Knaster Tarski applies and there is a fixed point Y of Φ.
    Let h be λx ⇒ if x ∈ Y then inv B g x else f x of type set → set.
    This h will be the desired bijection from A to B. Before proving this, it is helpful to prove the following properties of h:
    • If z is in Y, then there is a y in B ∖ {f x|x ∈ A ∖ X} such that g y = z and h z = y.
    • If z is not in Y, then h z = f z.
    • For every z in A, either there is a y in B ∖ {f x|x ∈ A ∖ X} such that g y = z and h z = y or z is not in Y and h z = f z.
    The third property follows easily from the first two. Proving this with a tableau refutation might be easier with the following rule:
    Rule (Cut) If P has type prop, then a branch is refutable if it is refutable extended with P and it is refutable extended with ¬ P.
    Using the third property above makes it easy to prove the first two properties for h to be a bijection.
    • ∀u ∈ A, h u ∈ B
    • ∀u v ∈ A, h u = h v → u = v
    The third property can also be proven: ∀w ∈ B, ∃u ∈ A, h u = w.
    Combining these we have bij A B h as desired.
    ∎
    Try to prove it yourself.
    In each problem we give
    a Φ defined such that Φ A B f g corresponds to the Φ above, i.e., λX ⇒ {g y|y ∈ B ∖ {f x|x ∈ A ∖ X}} of type set → set.
    and an h defined such that h A B f g Y is the bijection corresponding to h above, i.e., λx ⇒ if x ∈ Y then inv B g x else f x of type set → set where Y is intended to be a fixed point of Φ A B f g given by Knaster Tarski.
    Subgoal 5 (using Subgoals 3 and 4)
    Subgoal 6 (using Subgoal 5)
    Subgoal 7 (using Subgoal 5)
    Main Goal (using Subgoals 1, 2, 6, 7 and 8)