Notes on other downcasings

These are notes on downcasings that I have not completed yet. They are for personal use; they contain errors.

• 1. Local Set Theories

1. Local Set Theories
=====================

(T1)  |-*

(T2)  a|-a

      a|-b  b|->c
(T3)  -----------
        a|-c

      a|-b_1 ... a|-b_n
(T4)  -----------------
      a|-(b_1,...,b_n)

      a|-(b_1,...,b_n)
(T5)  -----------------
          a|-b_i

      a,b|-ω[P]
(T6)  ---------
      a|-{b|P}

      a|-b  a|-b'
(T7)  -----------
      a|-ω[b=b']

      a|-b  a|-{b|P}
(T8)  --------------
       a|-ω[b∈{b|P}]


(L1)  P<=>Q := ω[P]=ω[Q]
(L2)      ⊤ := *=*
(L3)    P∧Q := (ω[P],ω[Q])=(ω[⊤],ω[⊤])
(L4)    P⊃Q := (P∧Q)<=>P
(L5)   ∀b.P := {b|P}={b|⊤}
(L6)      ⊥ := ∀ω[P].P
(L7)     ¬P := P⊃⊥
(L8)    P∨Q := ∀ω[R].(((P⊃R)∧(Q⊃R))⊃R)
(L9)   ∃b.P := ∀ω[Q]. ...


(Tautology)     P|-P
(Unity)         |-*'=*
(Equality)      b'=b''|-c[b:=b']=c[b:=b'']
(Products)      |-π<b,c>=b
                |-π'<b,c>=c
                |-<π(b,c),π'(b,c)>=(b,c)
(Comprehension) |-b∈{b|P}<=>P


                  P|-R
(Thinning)        ------
                  P,Q|-R

                  a;P|-Q   a;P,Q|-R
(Cut)             -----------------
                       a;P|-R

                    a,b;P|-Q   a|-b'
(Subst)           --------------------
                  a;P[b:=b']|-Q[b:=b']

                  a,b;P|-b∈{b|Q}<=>b∈{b|R}
(Extensionality)  ------------------------
                    a;P|-{b|Q}<=>{b|R}

                  P,Q|-R   P,R|-Q
(Equivalence)     ---------------
                     P|-Q<=>R