Index of the slides:

Prawitz’s example: original version . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2 Prawitz’s example: proper subtrees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Quantifiers: judgment rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Quantifiers: diagrammatic rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Dotted diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Names for some adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .7 Rules for the quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .8 Introduction of the existential . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Elimination of the existential . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 A derivation from Prawitz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 A derivation from Prawitz (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .12 Wild notes about exist-elim . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Notes about DTT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .14 Prawitz’s example: original version In [Prawitz], this example of a translation (from natural language) is used to introduce Natural Deduction:

An informal derivation of ∀x.∃y.(P xy&Qxy) from the two assumptions (1) ∀x.∀y.P xy

(2) ∀x.∀y.(P xy [figure]Qxy) may run somewhat as follows: From (1), we obtain:

(3) ∃y.P ay Let us therefore assume

(4) P ab. From (2), we have:

(5) P ab [figure]Qab and from (4) and (5)

(6) Qab. Hence, from (4) and (6), we obtain

(7) P ab&Qab and from (7) we get

(8) ∃y.(P ay&Qay) Now, (8) is obtained from assumption (4), but the argument is independent

of the particular value of the parameter b that satisfies (4). In view of (3), we therefore have:

(9) (8) is independent of the assumption (4). Because of (9), (8) depends only on (1) and (2) and thus holds on these

assumptions for any arbitrary value of a. Hence, the desired result: (10) ∀x.∃y.(P xy&Qxy).

The corresponding natural deduction is given below; the numerals refer to steps in the informal argument above (rather than to the way the assumptions are discharged).

\begin{matrix}{(1) ∀x∃yP xy \atop (3) ∃yP ay} & \begin{matrix}(4) P ab & \begin{aligned}(4) P ab & {∀x∀y(P xy [figure]Qxy) (2) \atop ∀y(P ay [figure]Qay)} ; P ab [figure]Qab (5) \\ & Qab (6) \end{aligned} \\ P ab&Qab (7) \end{matrix} ; ∃y(P ay&Qay) (8) \\ ∃y(P ay&Qay) (9) \end{matrix} ; ∀x∃y(P xy&Qyx) (10)

Prawitz’s example: proper subtrees We will use the same letters for free and bound variables, and we’ll often abbreviate ‘P ab’ and ‘Qab’ as just ‘P ’ and ‘Q’. In our notation, with all discharges indicated, that tree becomes:

\begin{matrix}\begin{aligned}[a]^{2} & ∀a.∃b.P \\ & ∃b.P \end{aligned} (∀E) & \begin{aligned}[P]^{1} & \begin{aligned}[P]^{1} & \begin{aligned}[b]^{1} & \begin{aligned}[a]^{2} & ∀a.∀b.P [figure]Q \\ & ∀b.P [figure]Q \end{aligned} (∀E) \\ & P [figure]Q \end{aligned} ; (∀E) \\ & Q \end{aligned} \\ & P &Q \end{aligned} ; ∃b.P &Q ; (∃I) \\ ∃b.P &Q \end{matrix} ; (∃E); 1 ; ∀a.∃b.P &Q ; (∀I); 2

Definition: a subtree of an ND derivation is \underline{improper} when it contains a bar that discharges hypotheses (say, “(∃E); 1” above) but it doesn’t contain all of the leaves associated to that discharge (in that case, [P]^{1}, [P]^{1}, and [b]^{1}).

It is easy to attribute a meaning (a “semantics”) for proper subtrees in which all the hypotheses and the conclusion have the same free variables. For example, this subtree,

\begin{matrix}∃b.P ab & ∀b.P ab [figure]Qab \\ ∃b.P ab&Qab \end{matrix}

corresponds to this inclusion between subsets of A:

{ b | ∃b.P ab and ∀b.P ab [figure]Qab }
⊆ { b | ∃b.P ab&P qb }

But how do we attribute a semantics for proper subtrees where the sets of free variables of the hypotheses and the conclusion are not all equal? Even worse: how can we interpret hypotheses like ‘b’ (or ‘f(a)’), that are terms (values for variables), instead of “truths”? This seems to make no sense in “subset semantics”...

To understand this we need to introduce other translations.

Quantifiers: judgment rules In [Jacobs], sec. 4.1, the rules for the quantifiers for first-order logic are stated in terms of “judgments”, as below: (his notation is very different, though -)

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

Each judgment of the form ‘a; P a ⊢ Qa’ can be understood as an inclusion { a | P a } ⊆ { a | Qa }. Judgments of the form a ⊢ b are functions A → B (or sections of a dependent projections, as we will see later).

In (∀E) and (∃I) there seems to be a missing ‘b’ in one of the hypotheses/conclusions; that b is taken to be the image of a by a ⊢ b.

Here’s how to translate the “judgment rules” to Natural Deduction...

\begin{matrix}[b]^{2} P a ; ⋮ . ; Qab ; ∀b.Qab (∀I); 2 & \begin{aligned}b & P a ; ⋮ . ; ∀b.Qab \\ & Qab \end{aligned} (∀E) \\ b P a ; ⋮ . ; Qab ; ∃b.Qab (∃I) & \begin{aligned}P a ; ⋮ . ; ∃b.Qab & [b]^{1} [Qab]^{1} Ra ; ⋮ . ; Sa \\ & Sa \end{aligned} ; (∃E); 1 \end{matrix}

in the ND form the free variables of each subtree are not shown - they must be inferred.

Quantifiers: diagrammatic rules Now let’s draw these rules in a diagrammatic form:

\begin{matrix}{a, b; P a ⊢ Qab \atop a; P a ⊢ ∀b.Qab} & (∀I) \\ \begin{aligned}a ⊢ b & a; P a ⊢ ∀b.Qab \\ & a; P a ⊢ Qab \end{aligned} & (∀E) \\ \begin{matrix}a ⊢ b & a; P a ⊢ Qab \\ a; P a ⊢ ∃b.Qab \end{matrix} & (∃I) \\ \begin{matrix}a; P a ⊢ ∃b.Qab & a, b; Qab, Ra ⊢ Sa \\ a; P a, Ra ⊢ Sa \end{matrix} & (∃E) \end{matrix}  \begin{matrix}[b]^{2} P a ; ⋮ . ; Qab ; ∀b.Qab (∀I); 2 & \begin{aligned}b & P a ; ⋮ . ; ∀b.Qab \\ & Qab \end{aligned} (∀E) \\ b P a ; ⋮ . ; Qab ; ∃b.Qab (∃I) & \begin{aligned}P a ; ⋮ . ; ∃b.Qab & [b]^{1} [Qab]^{1} Ra ; ⋮ . ; Sa \\ & Sa \end{aligned} ; (∃E); 1 \end{matrix}

[figure: P; Q; [b]^{1}; Q; Q; ∀b.Q; ∀I_{1}; a, b; a; P; ∀b.Q; ∀b.Q; Q; ∀E; b; Q; a, b; a; P; Q; b; Q; Q; ∃b.Q; ∃I; a, b; a; P; ∃b.Q; ∃b.Q; Q; ∃E; Q; S; R; S; ∃b.Q; b; ∃E; b; S; a, b; a]

Each proposition will be draw over (the list of) is free variables. We draw ‘b’ over ‘a’ for reasons that will be become clear later (briefly: in the system with dependent types the type for b will be B_{a}, which depends on a).

Let’s translate the example from [Prawitz] to diagrammatic form. We get a DAG over a, b ↦ b ↦ ∗, and we can translate the notion of “proper subtree” into a corresponding notion for DAGs.

A sub-DAG is “proper” when it is made of a subset of the vertices and arrows of the original DAG (ignore the base a, b ↦ b ↦ ∗ - think of it as being just the shadow of what’s above it) such that:

• If an arrow (α → β) ∈ D′ then the vertices α and β belong to D′;

• D′ has exactly one final node (its conclusion);

• If (α ↦ γ) and (β ↦ γ) belong to D, and if (α ↦ γ) ∈ D′, then (β ↦ γ) ∈ D′;

• If D′ contains a discharging arrow then it contains all the associated discharged nodes.

Dotted diagrams

\begin{matrix}\begin{aligned}[a]^{2} & ∀a.∃b.P \\ & ∃b.P \end{aligned} (∀E) & \begin{aligned}[P]^{1} & \begin{aligned}[P]^{1} & \begin{aligned}[b]^{1} & \begin{aligned}[a]^{2} & ∀a.∀b.P [figure]Q \\ & ∀b.P [figure]Q \end{aligned} (∀E) \\ & P [figure]Q \end{aligned} ; (∀E) \\ & Q \end{aligned} \\ & P &Q \end{aligned} ; ∃b.P &Q ; (∃I) \\ ∃b.P &Q \end{matrix} ; (∃E); 1 ; ∀a.∃b.P &Q (∀I); 2 \begin{matrix}{A \atop a} [v]^{3} & \begin{matrix}{A \atop a} & [v]^{3} \\ B \end{matrix} ; b ; [v]^{1} \\ W[P] \end{matrix} ; P [v]^{2}

P [figure]Q  ∀b.P [figure]Q [figure]^{∀E} ∀b.P [figure]Q  ∀a, ∀b.P [figure]Q [figure]^{∀E} P [figure]Q Q [figure] Q  P [figure]  P  ∃b.P [figure] _{∃E} ∃b.P  ∀a.∃b.P [figure] _{∀E} Q  P &Q [figure] P P &Q [figure] P &Q  ∃b.P &Q_{∃I} [figure] ∃b.P &Q  ∀a.∃b.P &Q_{∀I_{2}} [figure] P [figure]Q  b [figure]  ∃b.P b_{∃E} [figure] ∀b.P [figure]Q  [a]^{2} [figure] ∃b.P  [a]^{2} [figure] a, b  a [figure] a  ∗ [figure]

Names for some adjunctions

[figure: P; (b=b′)&P; P; Q; (b=b′)&P; Q; Q; Q; =^{♭}; =^{♯}; a, b; a, b, b′; P; ∃b.P; Q; Q; R; ∀b.R; P; Q; ∃b.P; Q; Q; R; Q; ∀b.R; ∃^{♭}; ∃^{♯}; ∀^{♭}; ∀^{♯}; a, b; a]

a, b  a [figure] a, b c[figure]  a b ↦ c [figure] c  b ↦ c [figure] [figure]_{↦^{♭}}_{↦^{♯}} [figure]  (a; a)  a [figure] (a; a) (b; c) [figure]  a b, c [figure] (b; c)  b, c [figure] [figure]_{×^{♭}}_{×^{♯}} [figure]  P &Q  P [figure] P &Q R[figure]  P Q [figure]R [figure] R  Q [figure]R [figure] [figure][figure: ♭] [figure: ♯] [figure]

Rules for the quantifiers

\begin{aligned}{a, b; P ⊢ Q \atop a; P ⊢ ∀b.Q} (∀I) & := & (∀^{♯}) \\ \begin{aligned}a ⊢ b & a; P ⊢ ∀b.Q \\ & a; P ⊢ Q \end{aligned} (∀E) & := & \begin{matrix}a ⊢ b & {a; P ⊢ ∀b.Q \atop a, b; P ⊢ Q} (∀^{♭}) \\ a; P ⊢ Q \end{matrix} ; s \\ \begin{matrix}a ⊢ b & a; P ⊢ Q \\ a; P ⊢ ∃b.Q \end{matrix} (∃I) & := & \begin{matrix}a; P ⊢ Q & \begin{matrix}a ⊢ b & {a; ∃b.Q ⊢ ∃b.Q \atop a, b; Q ⊢ ∃b.Q} (∃^{♯}) \\ a; Q ⊢ ∃b.Q \end{matrix} ; s \\ a; P ⊢ ∃b.Q \end{matrix} ; ∘ \\ \begin{matrix}a; P ⊢ ∃b.Q & a, b; Q, R ⊢ S \\ a; P, R ⊢ S \end{matrix} (∃E) & := & \begin{matrix}a; P ⊢ ∃b.Q & \begin{matrix}{a, b; Q, R ⊢ S \atop a, b; Q ⊢ R [figure]S} & ( [figure]^{♯}) \\ a; ∃b.Q ⊢ R [figure]S \end{matrix} ; (∃^{♯}) \\ a; P ⊢ R [figure]S \end{matrix} ; s ; a; P, R ⊢ S ; ( [figure]^{♭}) \end{aligned}

Introduction of the existential

[figure: P; Q; a;P a⊢Qab; P; ∃b.Q; a;P a⊢∃b.Qab; Q; Q; Q; ∃b.Q; Q; ∃b.Q; Q; ∃b.Q; ∃b.Q; ∃b.Q; ∃b.Q; ∃b.Q; ∃b.Q; ∃b.Q; ∃^{♯}; a; a, b; a⊢b; a, b; a]

\begin{matrix}a ⊢ b & a; P a ⊢ Qab \\ a; P a ⊢ ∃b.Qab \end{matrix} (∃I)  a; P a ; ⋮ . ; a; Qab ; a; ∃b.Qab

Elimination of the existential In Natural Deduction:

\begin{aligned}a; P a ; ⋮ . ; a; ∃b.Qab & [a, b; Qab]^{1} {a; Ra \atop a, b; Ra} ; ⋮ . ; a, b; Sa \\ & a; Sa \end{aligned} ; (∃E); 1

In Sequent Calculus:

\begin{matrix}a; P a ⊢ ∃b.Qab & a, b; Qab, Ra ⊢ Sa \\ a; P a, Ra ⊢ Sa \end{matrix} (∃E)

Categorically:

P  P &R [figure] P ∃b.Q_{a;P a⊢∃b.Qab} [figure]  P &R S_{a;P a,Ra⊢Sa} [figure] Q&R  Q [figure] Q  ∃b.Q [figure] Q&R S_{a,b;Qab,Ra⊢Sa} [figure]  Q R [figure]S [figure]  ∃b.Q R [figure]S [figure] S  R [figure]S [figure] R [figure]S R [figure]S [figure] R [figure]S  S [figure] [figure: ♯] [figure]  _{∃^{♭}} [figure]  [figure: ♭][figure] a, b  a, b a, b  a [figure] a  a

A derivation from Prawitz Prawitz, p.19:

\begin{matrix}{∀x∃yP xy \atop ∃yP ay} & \begin{aligned}P ab & \begin{aligned}P ab & {∀x∀y(P xy [figure]P yx) \atop ∀y(P ay [figure]P ya)} ; P ab [figure]P ba \\ & P ba \end{aligned} \\ & P ab&P ba \end{aligned} ; ∃y(P ab&P ba) \\ ∃y(P ay&P ya) \end{matrix} ; ∀x∃y(P xy&P yx)

\begin{matrix}\begin{aligned}[a]^{3} & ∀x∃yP xy \\ & ∃yP ay \end{aligned} (∀E) & \begin{aligned}[P ab]^{2} & \begin{aligned}[P ab]^{2} & \begin{aligned}[b]^{1} & \begin{aligned}[a]^{3} & ∀x∀y(P xy [figure]P yx) \\ & ∀y(P ay [figure]P ya) \end{aligned} (∀E) \\ & P ab [figure]P ba \end{aligned} ; (∀E) \\ & P ba \end{aligned} \\ & P ab&P ba \end{aligned} ; ∃y(P ay&P ya) ; (∃I); 1 \\ ∃y(P ay&P ya) \end{matrix} ; (∃E); 2 ; ∀x∃y(P xy&P yx) ; (∀I); 3

\begin{matrix}{∀x∃yP xy \atop a; ∃yP ay} (∀E) & \begin{matrix}[a, b; P ab]^{2} & \begin{aligned}[a, b; P ab]^{2} & \begin{matrix}{∀x∀y(P xy [figure]P yx) \atop a; ∀y(P ay [figure]P ya)} & (∀E) \\ a, b; P ab [figure]P ba \end{matrix} ; (∀E) \\ & a, b; P ba \end{aligned} \\ a, b; P ab&P ba \end{matrix} ; a; ∃y(P ay&P ya) ; (∃I); 1 \\ a; ∃y(P ay&P ya) \end{matrix} ; (∃E); 2 ; ∀x∃y(P xy&P yx) ; (∀I); 3

A derivation from Prawitz (2)

\begin{matrix}{∀a.∃b.P \atop a; ∃b.P} (∀E) & \begin{matrix}[a, b; P]^{2} & \begin{matrix}[a, b; P]^{2} & \begin{matrix}{∀a.∀b.P [figure]Q \atop a; ∀b.P [figure]Q} & (∀E) \\ a, b; P [figure]Q \end{matrix} ; (∀E) \\ a, b; Q \end{matrix} \\ a, b; P &Q \end{matrix} ; a; ∃b.P &Q ; (∃I); 1 \\ a; ∃b.P &Q \end{matrix} ; (∃E); 2 ; ∀a.∃b.P &Q ; (∀I); 3

\begin{matrix}{a ↦ b, q \atop a; b, q} (∀E) & \begin{aligned}[a, b; p]^{2} & \begin{aligned}[a, b; p]^{2} & \begin{aligned}[a; b]^{1} & \begin{aligned}[a]^{3} & a ↦ (b ↦ (p ↦ q)) \\ & a; b ↦ (p ↦ q) \end{aligned} (∀E) \\ & a, b; p ↦ q \end{aligned} ; (∀E) \\ & a, b; q \end{aligned} ; ( [figure]E) \\ & a, b; p, q \end{aligned} ; (&I) ; a; b, p, q ; (∃I); 1 \\ a; b, p, q \end{matrix} ; (∃E); 2 a ↦ b, p, q (∀I); 3

\begin{matrix}{∀a.∃b.P \atop a; ∃b.P} (∀E) & [a, b; P]^{2} {∀a.∀b.P [figure]Q \atop a; ∀b.P [figure]Q} (∀E) ; ⋮ . ; a; ∃b.P &Q \\ a; ∃b.P &Q \end{matrix} ; (∃E); 2 ; ∀a.∃b.P &Q ; (∀I); 3

Wild notes about exist-elim What do I know about the (∃E^{∨}) rule from ND?

P &Q  P [figure] P &Q  P^{π} [figure] P  ∃b.P [figure] P  ∃b.P^{□} [figure] ∃b.P  (∃b.P)&Q [figure] ∃b.P  (∃b.P)&Q [figure]^{π} R  Q [figure]R [figure] Q [figure]R  Q [figure]R [figure] Q [figure]R  R [figure] P &Q R[figure]  P Q [figure]R [figure]  ∃b.P Q [figure]R [figure]  (∃b.P)&Q R[figure] [figure]  [figure]  [figure] a, b  a, b a, b  a [figure] a  a

We do have a map P &Q ↦ (∃b.P)&Q:

[figure: P; ∃b.P; P; ∃b.P; co□; P; P &Q; ∃b.P; ∃b.(P &Q); ∃b.P; (∃b.P)&Q; P &Q; ∃b.(P &Q); P &Q; ∃b.(P &Q); co□; ∃b.(P &Q); (∃b.P)&Q; ♮; ∃b.(P &Q); (∃b.P)&Q; Frob; P &Q; Q; ∃b.(P &Q); Q; (∃b.P)&Q; Q; Q; Q; Q; Q; □; a, b; a; P &Q; (∃b.P)&Q; co□;♮; R; R; R; R; □; P &Q; R; (∃b.P)&Q; R; a, b; a]

I don’t know how to universalize the R, though... Ah, make the adjunction arrows bidirectional, and start with a pair of objects... ((a, b; P); (a; Q)) ...and then?

Notes about DTT Dependent types (or: “dependent spaces”): a, b, c ⊢ D

Spaces of witnesses: a, b, c ⊢ W[P (a, b, c)]

Sections: a ⊢ b

Substitutions:

\begin{matrix}a ⊢ b & a, b, c ⊢ D \\ a, c ⊢ D \end{matrix}

Arbitrary base maps The category of display maps Witnesses of equality Vertical maps

Ideas about display maps: One-step projections Generalized projections The category with just the projections is a poset Sections (monics, inverse to projections) Diagonal maps

We know how to attribute a semantics to proper trees in propositional ND, but what about ND for (intuitionistic, typed) first-order logic? Then each hypothesis, and the conclusion, may have a different set of free variables - and, worse, of the two hypotheses for the (∀E) rule,

\begin{matrix}b(a) & ∀b.P (a, b) \\ P (a, b(a)) \end{matrix} (∀E)

one is a value for a variable (as a term), the other is is a proposition...

Conjecture: my categorical inter-fiber semantics for ND can be extented to a semantics for DTT. Conjecture: in my semantics for inter-fiber ND trees, each ND tree corresponds to a structure that can convert sections (one for each hypothesis, and compatible somehow) into a section corresponding to the final conclusion.