Index of the slides:

Quantifiers in Pavlovic’s thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 A derivation from Lambek/Scott . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Seely’s PLC paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Seely’s PLC paper: trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Seely’s PLC paper: trees, in DNC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Local set theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Local set theories (1) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 Notes on reading SeelyHyp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .9 Quantifiers in Pavlovic’s thesis The rules IΠ, EΠ, IΣ, EΣ, as they appear in Pavlovič:

{[X : P : Δ′] \atop q : Q : Δ′′} ; λX.q : ΠX:P.Q : Δ′′ IΠΔ′Δ′′
\begin{matrix}p : P : Δ′ & r : ΠX:P.Q(X) : Δ′′ \\ rp : Q[X := p] : Δ′′ \end{matrix} EΠΔ′Δ′′
\begin{matrix}p : P : Δ′ & {[X : P : Δ′] \atop Q : Δ′} & q : Q(p) : Δ′′ \\ ⟨p, q⟩ : ΣX:P.Q : Δ′ \end{matrix} IΣΔ′Δ′′

\begin{matrix}r : ΣX:P.Q : Δ′′ & {[X : P : Δ′] \atop [Y : Q(X) : Δ′′]} ; s(X, Y) : S(⟨X, Y ⟩) : Δ \\ ν(r, (X, Y).s) : S(r) : Δ \end{matrix} EΣΔ′Δ′′

The same rules, but with a DNC-ish choice of letters:

{[b : B : Θ′] \atop c : C : Θ′′} ; λb.c : Πb:B.C : Θ′′ IΠΘ′Θ′′
\begin{matrix}b′ : B : Θ′ & f : Πb:B.C(b) : Θ′′ \\ fb : C[b := b′] : Θ′′ \end{matrix} EΠΘ′Θ′′
\begin{matrix}b′ : B : Θ′ & {[b : B : Θ′] \atop C : Θ′} & c : C(b′) : Θ′′ \\ ⟨b′, c⟩ : Σb:B.C : Θ′ \end{matrix} IΣΘ′Θ′′

\begin{matrix}p : Σb:B.C : Θ′′ & {[b : B : Θ′] \atop [c : C(b) : Θ′′]} ; d(b, c) : D(⟨b, c⟩) : Θ′′′ \\ ν(p, (b, c).d) : D(p) : Θ′′′ \end{matrix} EΣΘ′Θ′′

A derivation from Lambek/Scott Lambek/Scott, p.131:

\begin{matrix}{∀_{x∈A}φ(x) ⊢ ∀_{x∈A}φ(x) \atop ∀_{x∈A}φ(x) ⊢_{x} φ(x)} (2.4) & {∃_{x∈A}φ(x) ⊢ ∃_{x∈A}φ(x) \atop φ(x) ⊢_{x} ∃_{x∈A}φ(x)} (2.4′) \\ ∀_{x∈A}φ(x) ⊢_{x} ∃_{x∈A}φ(x) \end{matrix} ; (1.2) ; ∀_{x∈A}φ(x) ⊢ ∃_{x∈A}φ(x) ; (1.4)

\begin{aligned}a ⊢ b & \begin{matrix}{a; ∀b.P ⊢ ∀b.P \atop a, b; ∀b.P ⊢ P} (∀E) & {a; ∃b.P ⊢ ∃b.P \atop a, b; P ⊢ ∃b.P} (∃I) \\ a, b; ∀b.P ⊢ ∃b.P \end{matrix} \\ & a; ∀b.P ⊢ ∃b.P \end{aligned} ; (s)

Seely’s PLC paper (1.1.1. Orders) 1 and Ω are orders; if A and B are orders, then A × B and Ω^{A} are also orders. (1.1.2. Operators) In the following, “σ ∈ A” means σ is an operator of order A; the rest of the arity is left unspecified for simplicity. For each order, there is a countable set of variable operators (called “indeterminates”).

∗ ∈ 1. ⊤ ∈ Ω. If σ, τ ∈ Ω, then σ ∧ τ and σ [figure]τ ∈ Ω. If σ ∈ Ω and α is an indeterminate of order A, then Σα ∈ A·σ and Πα ∈ A·σ ∈ Ω. (×I) If σ ∈ A, τ ∈ B, then ⟨σ, τ⟩ ∈ A × B. (×E) If σ ∈ A × B, then π_{1}σ ∈ A, π_{2}σ ∈ B. (P I) If α is an indeterminate of order A and σ ∈ Ω, then [α ∈ A : σ] ∈ Ω^{A}. (P E) If τ ∈ A, σ ∈ Ω^{A}, then σ(τ) ∈ Ω. Definition 1.1.3. A type is an operator of order Ω. (1.1.4. Terms) In the following, “a ∈ τ” means a is a term of type τ; the rest of the arity is left unspecified for simplicity. For each type, there is a countable set of variable terms (called “variables”). (⊤I) ∗ ∈ ⊤. ( [figure]I) If a ∈ τ, x a variable of type σ, then λx ∈ σ · a ∈ σ [figure]τ. ( [figure]E) If a ∈ σ [figure]τ, b ∈ σ, then a(b) ∈ τ. (∧I) If a ∈ σ, b ∈ τ, then ⟨a, b⟩ ∈ σ ∧ τ. (∧E) If a ∈ σ ∧ τ, then π_{1}a ∈ σ π_{2}a ∈ τ. (ΣI) If αis an indeterminate of order A, σ ∈ Ω, τ ∈ A, then I_{Σα·σ,τ} ∈ σ[τ/α] [figure] Σα ∈ A · σ. When clear from the context, we shall denote this term by I_{τ}, or even by I; in particular, if b ∈ σ[τ/α], then I(b) ∈ Σα ∈ A · σ. (ΣE) In a ∈ σ [figure]ρ, α an indeterminate of order A which is not free in ρ nor in the type of any free variable in a, then Vα ∈ A · a ∈ (Σα ∈ A · σ) [figure]ρ. (ΠI) If a ∈ σ, α an indeterminate of order A which is not free in the type of any free variable in a, then Λα ∈ A · a ∈ Πα ∈ A · σ. (ΠE) If a ∈ Πα ∈ A · α, τ ∈ A, then a{τ} ∈ σ[τ/α], where σ[τ/α] is σ with τ replacing α.

Seely’s PLC paper: trees Ω : Θ

1 : Θ  ∗ : 1
⊤ : Ω  ∗ : ⊤
\begin{matrix}A : Θ & B : Θ \\ A × B : Θ \end{matrix}  \begin{matrix}σ : A & τ : B \\ ⟨σ, τ⟩ : A × B \end{matrix}  {σ : A × B \atop π_{1}σ : A}  {σ : A × B \atop π_{2}σ : B}
{A : Θ \atop A → Ω : Θ} {σ : Ω \atop [α ∈ A : σ] : A → Ω}  \begin{matrix}τ : A & σ : A → Ω \\ σ(τ) : Ω \end{matrix}
\begin{matrix}σ : Ω & τ : Ω \\ σ ∧ τ : Ω \end{matrix}  \begin{matrix}a : σ & b : τ \\ ⟨a, b⟩ : σ ∧ τ \end{matrix}  {a : σ ∧ τ \atop π_{1}a : σ}  {a : σ ∧ τ \atop π_{2}a : τ}
\begin{matrix}σ : Ω & τ : Ω \\ σ [figure]τ : Ω \end{matrix} {a : τ \atop λx ∈ σ · a : σ [figure]τ}  \begin{matrix}b : σ & a : σ [figure]τ \\ a(b) : τ \end{matrix}
{σ : Ω \atop Σα ∈ A · σ : Ω}  \begin{matrix}σ : Ω & τ : A \\ I : σ[τ/α] [figure]Σα ∈ A · σ \end{matrix}  {a : σ [figure]ρ \atop Vα ∈ A · a : (Σα ∈ A · σ) [figure]ρ}
{σ : Ω \atop Πα ∈ A · σ : Ω}  {a : σ \atop Λα ∈ A · a : Πα ∈ A · σ}  \begin{matrix}τ : A & a : Πα ∈ A · α \\ a\{τ\} : σ[τ/α] \end{matrix}

Seely’s PLC paper: trees, in DNC Ω : Θ

1 : Θ  ∗ : 1
ω[⊤] : Ω ⊤ : ω[T]⊤
\begin{matrix}A & B \\ A × B \end{matrix}  \begin{matrix}a & b \\ a, b \end{matrix}  {a, b \atop a}  {a, b \atop b}
{A \atop A → Ω}  {ω[P] \atop a↦ω[P]}  \begin{aligned}a & a↦ω[P] \\ & ω[P] \end{aligned}
\begin{matrix}ω[P] & ω[Q] \\ ω[P &Q] \end{matrix} \begin{matrix}P & Q \\ P &Q \end{matrix} {P &Q \atop P}  {P &Q \atop Q}
\begin{matrix}ω[P] & ω[Q] \\ ω[P [figure]Q] \end{matrix} {Q \atop P [figure]Q}  \begin{aligned}P & P [figure]Q \\ & Q \end{aligned}

\begin{matrix}{ω[P] \atop ω[∃b.P]} & \begin{matrix}a, b ⊢ ω[P] & a ⊢ b \\ a ⊢ P [figure](∃b.P) \end{matrix} & \begin{matrix}a ⊢ ω[Q] & a, b; ⊤ ⊢ P [figure]Q \\ a; ⊤ ⊢ (∃b.P) [figure]Q \end{matrix} \\ {ω[P] \atop ω[∀b.P]} & \begin{matrix}a ⊢ ω[P] & a, b; P ⊢ Q \\ a; P ⊢ ∀b.Q \end{matrix} & \begin{aligned}b & ∀b.P \\ & b \end{aligned} \end{matrix}

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 [figure] Q := (P∧Q)<=>P
(L5) ∀b.P := {b|P}={b|⊤}
(L6)  ⊥ := ∀ω[P].P
(L7)  ¬P := P [figure] ⊥
(L8)    P∨Q := ∀ω[R].(((P [figure] R)∧(Q [figure] R)) [figure] R)
(L9) ∃b.P := ∀ω[Q]. ...

Local set theories (1)

(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

Notes on reading SeelyHyp SeelyHyp, §4: (5’) (i) For t : X → Y, φ over X, we define

Σ_{t}φ =^{def} ∃ξ(tξ = y ∧ φ(ξ)),

Π_{t}φ =^{def} ∀ξ(tξ = y [figure]φ(ξ)),

\begin{matrix}∃ξ(tξ = y ∧ γ(ξ)) & \begin{matrix}\begin{matrix}{tx = y ∧ γ(x) \atop [γ(x)]} & (∧E) \\ ⋮ . P \end{matrix} ; φ(x) & {tx = y ∧ γ(x) \atop tx = y} (∧E) \\ tx = y ∧ φ(x) \end{matrix} ; (∧I) ; ∃ξ(tξ = y ∧ φ(ξ)) ; (∃I) \\ ∃ξ(tξ = y ∧ φ(ξ)) \end{matrix} ; (∃E)

For f : A → B, define:

Σ_{f}{ a || P (a) } =^{def} { b || ∃a.(f(a) = b & P (a)) }

Π_{f}{ a || P (a) } =^{def} { b || ∀a.(f(a) = b [figure]P (a)) }

\begin{matrix}∃a.(f(a) = b ∧ P (a)) & \begin{matrix}{[f(a) = b ∧ P (a)]^{1} \atop f(a) = b} (∧E) & {[f(a) = b ∧ P (a)]^{1} \atop P (a)} (∧E) ; ⋮ . ; Q(a) \\ f(a) = b ∧ Q(a) \end{matrix} ; (∧I) ; ∃a.(f(a) = b ∧ Q(a)) ; (∃I) \\ ∃a.(f(a) = b ∧ Q(a)) \end{matrix} ; (∃E)