The Existential Quantifier in Equideductive Logic

(first incomplete draft)

Paul Taylor

12 January 2011

1 Ideas of existential quantification

I would appreciate some help with the details behind these historical comments, especially in the opening paragraphs and the second order (Russell??) definition of ∃ from ∀.

The existential quantifier ∃x. 𝔭(x) has been given many different syntactic and semantic meanings in mathematics, logic and category theory.

Perhaps the most natural meaning is the constructive one, in which we must exhibit a witness a and a proof of 𝔭(a) in order to assert that ∃x. 𝔭(x) [best ref? Brouwer?]. At first sight, this quantifier seems to have very little force, merely concealing the identity of a. However, with the formalisation of intuitionistic logics in proof theory came the existence theorem that

from any given explicit proof of ∃x. 𝔭(x), we may derive a term a and a proof of 𝔭(a).

[Who first proved this? Gentzen? Gödel?]

The constructive definition stood in opposition to the classical one, which said that a mathematical object always exists so long as it is “free from contradition”. Formally, this seems to mean that ∃ ≡ ¬∀¬. [Is there a better explanation than this?]

While logicians debate the properties of formulae like ∃x. 𝔭(x) containing a bound variable x, ordinary mathematicians work with an idiom of discourse in which the witness x is apparently an actual object. The phrase “there exists x such that ϕx” means not only the formal statement ∃x. ϕx but also that we may proceed to use an object x that has this property.

David Hilbert proposed a calculus [ref?] in which the operator ϵ applied to a predicate 𝔭 yields a particular witness a ≡ ϵ𝔭 for 𝔭(a). Boubaki subsequently began the first volume [ref] of Eléments de Mathématiques with this idea, using □ instead of ϵ. On the face of it, the meaning of the existential quantifier therefore relies on the Axiom of Choice.

However, no choice of witness is actually needed. Notice, in particular, that we are not permitted to make any analysis of the value a. So it is not a term. The symbol a must therefore be a variable.

Indeed, the idiom may be reconciled with intuitionistic sequent calculus without making any additional assumption whatever. The part of the idiomatic argument during which we “pretend” that we have a witness a actually provides the formal proof of the premise (top line) of the rule

{Γ, a, 𝔭(a) ⊢ 𝔮 \atop Γ, ∃x. 𝔭(x) ⊢ 𝔮.}

Then the consequent (bottom line) asserts that the proposition 𝔮 follows from the unwitnessed hypothesis ∃x. 𝔭(x).

There is something more here than a proof of 𝔮 from the witness a of 𝔭(a), just as there is something more in a proof by induction than its base case and induction step. However, the extra ingredient is not the axiom of choice but half of the definition of the existential quantifier. The proof rule above is found in any account of the sequent calculus [ref, P+T will do], where it is known as the left rule for ∃. The corresponding idea in natural deduction is called the elimination rule.

The vernacular of mathematics therefore agrees with standard formal logic. This correspondence is discussed in more detail in Section 5 and [?, §1.6].

The rule is, however, subject to the priviso that the conclusion 𝔮 must not export the identity of a. Indeed, if theorem with a parameter y : Y were to do this, it would exactly be asserting Choice of the form

∀x:X. ∃y:Y . 𝔭(x, y) ⊢ ∃f:X → Y . ∀x. 𝔭(x, fx).

The meaning that emerges from the idiom and rule for ∃ is that

knowing ∃x:X. 𝔭(x) gives us the right to pretend that we have a witness a for 𝔭(a), in order to prove conclusions 𝔮 of a certain form.

In this paper we consider different (tighter, more specific) restrictions on the syntactic form of the conclusion 𝔮 and thereby obtain a different (weaker, more general) existential quantifier. This means that the class of permissible conclusions 𝔮 is being subjected to study. The existential quantifier ∃x. 𝔭(x) is defined to have a certain property for all such 𝔮:

∃x:X. 𝔭(x) means ∀𝔮. (∀x. 𝔮(x) ⇒ 𝔮) ⇒ 𝔮.

This way of defining the quantifier using second order logic is due to [whom? Russell? ref?] and is also found in [Prawitz?]. Under the Curry–Howard correspondence between propositions and types, it also appears in Girard’s System F [ref? P+T].

The purpose of this paper is to show that this syntactic idea of an existential quantifier that is defined in terms of the universal one agrees with the semantic notion of epimorphism in category theory. Also, we shall not use second order logic or type theory but a new (weaker) “predicate calculus” for which the category of sober topological spaces is a model (Section 2 and [equdcl]).

We introduce the categorical ideas by starting with elementary set theory. There the existential quantifier is embodied in the notion of a surjective function, writing

e : X ↠ Y to mean ∀y:Y . ∃x:X. y = ex.

When we generalise this from functions between sets to morphisms between other kinds of mathematical objects, we find that the notion of surjectivity splits into several properties that are in general inequivalent.

The morphism e : X ↠ Y is epi if it has the cancellation property that, for any object Z and any pair g, h : Y ⇉ Z of morphisms, if g · e = h · e then already g = h:

[figure: X; e; Y; g; h; Z.]

On the other hand, e : X ↠ Y is regular epi if it is the coequaliser of some pair p, q : K ⇉ X:

[figure: K; p; q; X; e; Y]
[figure: f]
Z^{\begin{matrix}h \\  \end{matrix}. . . . . . . . .}

Being a coequaliser means that the composites e · p = e · q are equal and, whenever the composites f · p = f · q to another object Z are equal, there is a unique map h : Y → Z that makes the triangle commute (f = h · e). In algebra, coequalisers are called quotients and the algebra K is often given as a congruence. For groups, rings and vector spaces there are simpler representations of congruences that are peculiar to these theories, namely normal subgroups, ideals and subspaces.

Plainly we may reverse the arrows in each of these three definitions to obtain different notions of inclusion. These different forms of surjection and injection do not behave well in arbitrary circumstances, for example regular monos do not compose in the category of additive monoids. But in many mathematically important categories any morphism may be factorised as

• a regular epi followed by a mono, or

• an epi followed by a regular mono. In the settings of particular algebraic theories, results of the first kind are often known as isomorphism theorems, saying that that image of a morphism is isomorphic to the quotient of its domain by its kernel.

When we analyse this situation using category theory, we find that the force of these theorems lies in the orthogonality property:

X  [figure: e] I
.............. h
[figure: J; f; m; Y; g]

This says that, whenever we have a commutative square (g · e = m · f) in which e has whichever “surjectivity” property (regular or plain epi) we are considering and m has the “injectivity” one (mono or regular mono) then there is a unique diagonal fill-in h making the triangles commute (h · e = f and m · h = g).

Applied to the category of sets, the factorisation theorems, and in particular the orthogonality property, are directly related to the logical existential quantifier:

• the epi e corresponds to the introduction rule, 𝔭(x) ⊢ ∃x. 𝔭(x),

• the mono m corresponds to the conclusion 𝔮 above, and

• the diagonal fill-in h to the elimination rule. This connection was established in a more general type-theoretic setting by Martin Hyland and Andrew Pitts [ref] and discussed further in [prafm, §9.3].

However, there is still a piece of the categorical description missing. In symbolic logic, we may substitute under the quantifier:

[b/y]^{∗} ∃x. 𝔭(x, y) ⟺ ∃x. [b/y]^{∗}𝔭(x, y) ≡ ∃x. 𝔭(x, b)

and the proof-theoretic analysis of this is called commutation.

[figure: X′; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; X; Y′; e′; . . . . . . . . . . . . . . .; f; Y; e]

In the categorical setting, the substitution [b/y]^{∗} is given by pullback or inverse image along a function f (which is the reason for the star in the notation). For this formulation to agree with the symbolic one, the pullback of an epi e as above must be another epi e′.

We would like to take these ideas that came from logic, set theory and category theory and apply them to general topology. In that subject, all of the notions of injectivity and surjectivity that we have mentioned arise, together with others. A continuous function f : X → Y is

• mono iff it is a 1–1 function on points;

• regular mono iff it is mono and X carries the subspace topology inherited from Y; or

• regular mono iff it is surjective on points and Y carries the quotient topology inherited from X. However, the characterisation of epis is more delicate. It depends on the particular category

within which we are working, i.e. the generality of the spaces over which Z above ranges. (This is analogous to considering different classes of conclusions 𝔮.) Classically, a continuous function f : X → Y is epi iff

• it is surjective on points, in the case where all topological spaces in the traditional sense found in [Bourbaki] are admitted for Z;

• every point of Y may be expressed as a directed join of images of points of X with respect to the specialisation order, when all sober topological spaces are allowed;

• it is surjective on points, when just Hausdorff spaces are allowed.

Since the first and third cases are the same as in set theory, it is the middle one that is interesting. The basic example is the domain ϖ of ascending natural numbers. This has a point called ∞ that is the directed join of the (finite) natural numbers. Classically, its open subsets are ∅ and ↑ n ≡ ϖ \ {0, …, n − 1} (but not {∞}).

∞ ; ⋮ ; • ; • ; • ; •  [figure: 1; ∞; ϖ; ∅; ℕ; e]

If we want to prove that two continuous functions g, h : ϖ ⇉ Z are equal, where Z is sober, it is enough to show that g(n) = h(n) for all (finite) n ∈ ℕ, because then f(∞) = g(∞) follows automatically. Indeed, most proofs in classical domain theory work by restricting attention to the “finite” elements.

Therefore e : ℕ → ϖ is epi amongst sober topological spaces [?, Lemma II 1.11], even though it is not surjective on points. Categorically, this means that the pullback above is the empty space and does not preserve the epi.

This situation is very similar to the vernacular use of “there exists” in ordinary mathematics that we described earlier:

In order to show g = h, that is, ∀x:ϖ. gx = hx, it is legitimate to pretend that x = en for some n ∈ ℕ.

It is manifestly false that ∃n. ∞ = en, so in order to avoid talking utter nonsense, the rules for manipulating the new quantifier must be weaker than those for the ordinary one. Indeed, when we define the new quantifier and disjunction operation in Section 3, we shall find that there are severe restrictions on the variables and contexts that may occur in the proof rules. In order to remind ourselves of these restrictions whenever we use the new quantifier, we shall use a new symbol for it, writing the property above as

x : ϖ ⊢ �n:ℕ. x = en.

(The letter � is an e sound in the Russian alphabet, where � is pronounced ye.)

Section 6 sketches the category that is associated with the logic, for which the equivalence was proved in the earlier paper. Then � corresponds to a class of epis that is closed under products but not pullbacks. However, it is still the case that every morphism factorises as an epi followed by a regular mono and they obey the orthogonality property (Section 7). Sections 8–9 use these ideas to show that the category has stable disjoint unions.

The “constructive” existential quantifier with with we began this discussion is stronger than the classical one because it requires the witness to be identified. Our new quantifier, on the other hand, is much weaker because there need not be any witness at all. However, we have seen that it neverthless has its roots in the constructive traditions of proof theory and category theory.

2 Equideductive logic

The setting in which we define this new existential quantifier is not second order logic but a new calculus called equideductive logic. It is a “predicate calculus” whose object language is the sober λ-calculus. The origins of this logic, its syntax, its topological semantics and the equivalent category theory are fully explored in the paper Equideductive Categories and their Logic.

The following remarks were just put here as the targets of cross references in this paper since it was put together from sections taken out of the one mentioned. This section will become a summary of equideductive logic, at whatever level of formality turns out to be appropriate as the programme develops.

Remark 2.1 We refer to the types of the object language as urtypes in a syntactic setting and urspaces in a semantic one. In the leading classical model (sober topological spaces), the urspaces may be either algebraic lattices with the Scott topology or locally compact spaces. The system of urtypes must admit products and exponentials of the form Σ^{(−)}, so its urterms are formed using the symbols ⋆, ⟨ , ⟩, π_{0}, π_{0}, λ, ev and focus.

Remark 2.2 Urtypes are sober. This means that for any term Γ ⊢ P : Σ^{Σ^{A}} that is prime,

Γ, Φ : Σ^{3}A ⊢ ΦP = P (λx. Φ(λϕ. ϕx)),

we may form

Γ ⊢ focus P : A such that Γ, ϕ : Σ^{A} ⊢ ϕ(focus P) = P ϕ.

In particualr, for any Γ ⊢ a : A, the term Γ ⊢ P ≡ λϕ. ϕa is prime.

Remark 2.3 Any exponential urtype Σ^{B} is syntactically injective.

Remark 2.4 Equideductive predicates are formed from ⊤, equations between urterms of type Σ, conjunctions (&) and quantified implications

∀y⃗. 𝔮⃗(y⃗) =▷ αx⃗y⃗ = βx⃗y⃗

subject to the variable binding rule that any variable that appears on the left of =▷ must be bound by the quantifier ∀.

Several definitional extensions were made in the earlier paper (and others are added in this and later ones) that allow predicates instead of just equations on the right of =▷. However, any predicate is nevertheless equivalent to one in normal form, i.e. a conjunction of quantified implications with equations on the right and similar normal forms on the left.

Remark 2.5 Equality between urterms is extended from Σ to a predicate on any urtype A by the Leibnizian formula

a = b ≡ ∀ϕ:Σ^{A}. ϕa = ϕb.

In particular, equality for ϕ, ψ : Σ^{A} satisfies

Γ, ϕ = ψ ⊣⊢ ∀x:A. ϕx = ψx  (∗)

as well as the usual equality-transmitting and η-rules for the sober λ-calculus.

Any predciate respects equality in the sense that

Γ, 𝔭(a), a = b ⊢ 𝔭(b).

Remark 2.6 Any proof of

x : A, y : B, 𝔭(x) ⊢ 𝔮(x, y)

\begin{matrix}· \\ · \\ · \end{matrix}

y : B, z : C, 𝔯(z) ⊢ 𝔰(y, z)

may be translated into a proof of

y : B, ∀x′. 𝔭(x′) =▷ 𝔮(x′, y) ⊢ ∀z. 𝔯(z) =▷ 𝔰(y, z)

or of y : B ⊢ (∀x′. 𝔭(x′) =▷ 𝔮(x′, y)) =▷ (∀z. 𝔯(z) =▷ 𝔰(y, z)),

and vice versa.

3 Disjunction and existential quantification

Now we are ready to define the new existential quantifier � and disjunction ⋎ and show that they satisfy rules that are similar to those in the sequent calculus, albeit with severe restrictions on the use of variables.

Notation 3.1 We want the new connectives ⊥, ⋎ and � to satisfy the rules

x⃗ : A⃗, 𝔰⃗(x⃗), ⊥ ⊢ 𝔯(x⃗)  x⃗ : A⃗, y⃗ : B⃗, z⃗ : C⃗, 𝔰(z⃗), 𝔭(x⃗, y⃗) ⊢ 𝔯(x⃗, z⃗) ; = ; x⃗ : A⃗, z⃗ : C⃗, 𝔰(z⃗), �y⃗:B⃗. 𝔭(x⃗, y⃗) ⊢ 𝔯(x⃗, z⃗)

and x⃗ : A⃗, z⃗ : C⃗, 𝔰(z⃗), 𝔭(x⃗) ⊢ 𝔯(x⃗, z⃗)  x⃗ : A⃗, z⃗ : C⃗, 𝔰(z⃗), 𝔮(x⃗) ⊢ 𝔯(x⃗, z⃗) =

x⃗ : A⃗, z⃗ : C⃗, 𝔰(z⃗), (𝔭 ⋎ 𝔮)(x⃗) ⊢ 𝔯(x⃗, z⃗)

We shall see that it is essential that A⃗ and B⃗ be urtypes and that there be no other predicates that involve x⃗ or y⃗. However, the predicate 𝔯(x⃗, z⃗) on the right may depend on additional variables z⃗ and on hypotheses 𝔰(z⃗), but the latter must not involve x⃗ or y⃗. It is because of these issues with free variables that we state them explictly in the predicates.

As we did when we introduced ∀=▷, we consider just equations on the right first and develop the results for general predicates 𝔯(x⃗, z⃗) from this simple case. We obtain the definitions of the new symbols by applying the technique of Proposition 2.6 to the prospective rules above, with the equation ϕx⃗ = ψx⃗ instead of 𝔯(x⃗, z⃗) on the right.

Notation 3.2 In the context [x⃗ : A⃗], with no predicates on x⃗, we define

⊥ ≡ ∀στ:Σ. σ = τ
(𝔭 ⋎ 𝔮)(x⃗) ≡ ∀ϕψ:ΣA⃗. (∀x′. 𝔭(x′) =▷ ϕx′ = ψx′)
& (∀x′′. 𝔮(x′′) =▷ ϕx′′ = ψx′′) =▷ ϕx⃗ = ψx⃗
�y⃗:B⃗. 𝔭(x⃗, y⃗) ≡ ∀ϕψ:ΣA⃗. (∀x′y⃗. 𝔭(x′, y⃗) =▷ ϕx′ = ψx′) =▷ ϕx⃗ = ψx⃗.

For clarity, we drop the strings of variables, since they can be recovered using product urtypes.

Lemma 3.3 These connectives obey the following introduction rules:

x : A, 𝔭(x) ⊢ (𝔭 ⋎ 𝔮)(x)  x : A, 𝔮(x) ⊢ (𝔭 ⋎ 𝔮)(x)  ⋎I_{0}, ⋎I_{1}
x : A, y : B, 𝔭(x, y) ⊢ �y. 𝔭(x, y).  �I

Proof For (�I), ∀E gives

x : A, y : B, 𝔭(x, y), ϕ, ψ : Σ^{A}, ∀x′y′. 𝔭(x′, y′) =▷ ϕx′ = ψx′ ⊢ ϕx = ψx.

Hence ∀ϕψ. (∀x′y. 𝔭(x′, y) =▷ ϕx′ = ψx′)) =▷ ϕx = ψx, which is �y. 𝔭(x, y).

Similarly, for (⋎I_{0}), by ∀E we have

x : A, 𝔭(x), ϕ, ψ : Σ^{A}, ∀x′. 𝔭(x′) =▷ ϕx′ = ψx′ ⊢ ϕx = ψx.

Weakening by ∀x′′. 𝔮(x′′) =▷ ϕx′′ = ψx′′ and using ∀I then give the definition of (𝔭 ⋎ 𝔮)(x). □

Lemma 3.4 Conversely, the connectives also obey the simple elimination rules, with just equations on the right:

x : A, ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ) ⊢ ϕx = ψx

{x : A, ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ), 𝔭(x) ⊢ ϕx = ψx x : A, ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ), 𝔮(x) ⊢ ϕx = ψx \atop x : A, ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ), (𝔭 ⋎ 𝔮)(x) ⊢ ϕx = ψx}

and {x′ : A, y : B, ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ), 𝔭(x′, y) ⊢ ϕx′ = ψx′ \atop x : A, ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ), �y. 𝔭(x, y) ⊢ ϕx = ψx}

Proof For ⊥E, use ∀E with σ ≡ ϕx and τ ≡ ψx.

By ∀I, the first premise of the rule for disjunction gives

ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ) ⊢ ∀x′. 𝔭(x′) =▷ ϕx′ = ψx′,

in which 𝔰′(ϕ, ψ) must not depend on x′, and the second premise provides the same for 𝔮. Applying ∀E to the definition of (𝔭 ⋎ 𝔮) and these two formulae gives ϕx = ψx.

Similarly, the premise of the rule for � gives

ϕ, ψ : Σ^{A}, 𝔰′(ϕ, ψ) ⊢ ∀x′y. 𝔭(x′, y) =▷ ϕx′ = ψx′,

in which 𝔰′(ϕ, ψ) must not depend on x′ or y. Applying ∀E to the definition of � with this gives ϕx = ψx, as required. □

Theorem 3.5 The connectives ⊥, ⋎ and � obey the general elimination rules in Notation 3.1. Proof Suppose first that 𝔯(x, z) is the equation αxz = βxz. Then the three general rules follow from the corresponding simple elimination rules with the substitutions

ϕ ≡ λx. αxz,  ψ ≡ λx. βxz  and 𝔰′(ϕ, ψ) ≡ 𝔰(z).

The case of a quantified implication,

𝔯(x, z) ≡ ∀z. 𝔰(z) =▷ αxz = βxz,

follows from that of an equation by ∀I. When 𝔯 is a conjunction we consider the conjuncts separately, whilst the case 𝔯 ≡ ⊤ is trivial. By Remark 2.4, these cases exhaust the possibilities for 𝔯. □

4 Properties of the new symbols

These connectives have many familiar properties that can be proved easily from the introduction and elimination rules.

Lemma 4.1 Disjunction and quantification are covariant:

{x : A, 𝔭(x) ⊢ 𝔭′(x) x : A, 𝔮(x) ⊢ 𝔮′(x) \atop x : A, (𝔭 ⋎ 𝔮)(x) ⊢ (𝔭′ ⋎ 𝔮′)(x)} {x : A, y : B, 𝔭(x, y) ⊢ 𝔭′(x, y) \atop x : A, �y. 𝔭(x, y) ⊢ �y. 𝔭′(x, y)}  □

Lemma 4.2 Disjunction is idempotent, absorptive, unital,

𝔭 ⊣⊢ 𝔭 ⋎ 𝔭 ⊣⊢ 𝔭 & (𝔭 ⋎ 𝔮) ⊣⊢ 𝔭 ⋎ (𝔭 & 𝔮) ⊣⊢ 𝔭 ⋎ ⊥,

absorbed by ⊤, commutative and associative,

𝔭 ⋎ ⊤ ⊣⊢ ⊤  𝔭 ⋎ 𝔮 ⊣⊢ 𝔮 ⋎ 𝔭  𝔭 ⋎ (𝔮 ⋎ 𝔯) ⊣⊢ (𝔭 ⋎ 𝔮) ⋎ 𝔯

where 𝔭 and 𝔮 may depend on any variables of urtype but not on any predicates as hypotheses. □

We find that the distributive law (for & over ⋎) and its analogue for � (which is known in categorical logic as the Frobenius law) can only be proved when the extra conjunct has no arguments in common with the disjunction:

Proposition 4.3 The weak distributive and Frobenius laws hold:

x : A, z : C, (𝔭 ⋎ 𝔮)(x) & 𝔰(z)  ⊣⊢ ((𝔭 & 𝔯) ⋎ (𝔮 & 𝔰))(x, z),
x : A, z : C, (�y. 𝔭(x, y)) & 𝔰(z) ⊣⊢ �y. (𝔭(x, y) & 𝔰(z)),

in which the variables x and z must be distinct (or, in the case of strings x⃗ and z⃗ of variables, disjoint). For ⊥, there is no difficulty regarding variables; it is strict because

⊥(x) & 𝔰(y) ⊣⊢ (⊥ & 𝔰)(x, y) ⊣⊢ ⊥(x, y) ⊣⊢ ⊥.  □

Lemma 4.4 The quantifiers satisfy the de Morgan laws

y : B, ∀x. (𝔭(x) =▷ 𝔯(y)) ⊣⊢ (�x. 𝔭(x)) =▷ 𝔯(y)

and y : B, (𝔭 =▷ 𝔯(y)) & (𝔮 =▷ 𝔯(y)) ⊣⊢ (𝔭 ⋎ 𝔮) =▷ 𝔯(y).  □

Corollary 4.5 Successive quantifiers commute and are the same as multiple ones.

Proof �zy. 𝔭(x, y, z) ≡ ∀ϕψ. (∀x′z′. ∀y′. 𝔭(x′, y′, z′) =▷ ϕx′ = ψx′) =▷ ϕx = ψx

⊣⊢ ∀ϕψ. (∀x′z′. (�y′. 𝔭(x′, y′, z′)) =▷ ϕx′ = ψx′) =▷ ϕx = ψx
≡ �z. (�y. 𝔭(x, y, z)).  □

Whereas the double quantifier is a single one over the product of the urtypes, the nullary version quantifies over 1. This is a kind of double negation.

Lemma 4.6 x : A, 𝔭(x) ⊣⊢ �y:1. 𝔭(x), which is

∀ϕψ. (∀x′. 𝔭(x′) =▷ ϕx′ = ψx′) =▷ ϕx = ψx.  □

It would be a useful exercise to prove that (�y. 𝔭(x)) ⊢ 𝔭(x) in the case where 𝔭(x) ≡ ∀y. 𝔮(y) =▷ αxy = βxy, in order to see that this can only be done if 𝔮 does not depend on x.

Instead of �y : 1 we could quantify a variable y of any urtype where y does not actually occur in 𝔭. This is the counit of the adjunction between � and weakening:

Corollary 4.7 x : A, �y:1. 𝔭(x, y) ⊣⊢ �y:1. 𝔭(x, ⋆) ⊣⊢ 𝔭^{⊤}(x, λϕ. ϕ⋆) ⊣⊢ 𝔭(x, ⋆). □

Corollary 4.8 Γ, x : A, 𝔭(x) ⊣⊢ �y:A. (𝔭(y) & (x = y)). □

This “double negation” formula will turn up again all over the place. In a slightly more complicated form, it will also be used in the construction of exponential spaces in the following paper.

Notation 4.9 For F : Σ^{Σ^{A}}, 𝔭̄(F) ≡ ∀ϕψ. (∀x. 𝔭(x) =▷ ϕx = ψx) =▷ F ϕ = F ψ.

Section 7 explains what � means in terms of epi–mono factorisation and in Section 8 we use algebraic inconsistency (⊥) to define the initial object, and ⋎ and � for the coproducts.

5 Idioms of reasoning

This section will become an explanation of how the new existential quantifier could be incorporated into natural dededuction and the idioms of the vernacular of mathematics as described in my book. At the moment it just consists of a collection of relevant fragments of text that were originally written in other contexts.

For the purpose of presenting the calculus, it is clearer to use judgements (sequents), in which the contexts are stated in full in each step. However, when we use the rules to develop ordinary mathematics, we would like to adopt a Natural Deduction style, in which the contexts remain the same from one step to the next unless we explicitly make or discharge assumptions and variables. Since these must obey last-in first-out scoping rules, one way of formalising them is by means of boxes that delimit the scopes; this style is described in [prafm, §1.5].

The relationship between the formal rules for the ordinary quantifier ∃ and mathematical idiom is explained in [prafm, §1.6]. As with ∀, the first step is to translate the sequent style into boxes that delimit the scope of the witnesses. Then we observe that it doesn’t matter when the box is closed (discharging the hypothetical witness), because everything that follows the end of it can be brought inside instead. That is, so long as

(a) we do not export the identity of the witness from the box; and

(b) it is closed before the next enclosing one. The box is therefore redundant, and we may instead “pretend” that we have a witness, just as ordinary mathematicians do when they say that “there exists” something satisfying the predicate.

How can we adapt these ideas to the new quantifier and disjunction operator? Whereas there were restrictions on the introduction of λ, focus and =▷, we now have to be careful about how we use the elimination rules for ⋎ and �.

The necessary additional precautions are that

(c) substitution for x into �y. 𝔭(x, y) is not allowed; and

(d) elimination of �y. 𝔭(x, y) is only allowed when the context contains no other predicates that have x as a free variable.

Since we cannot deduce anything from �y. 𝔭(x, y) if it violates this restriction, it is useless (at least, in any role for which � is an appropriate notation). So we may as well strengthen the precaution (d) by putting it into the same pattern as those on λ and =▷, namely that

(e) we may only form �y. 𝔭(x, y) in a context in which x is of urtype, and not subject to any other predicate.

This completes our account of the purely syntactic aspects of the logic. Section 7 explains what � means in terms of epi–mono factorisation. In Section 8 we use algebraic inconsistency (⊥) to define the initial object, and ⋎ and � for the coproducts.

6 Equideductive categories

This section will give a brief sketch of the construction of the classifying category for equideductive logic. The full version is in the paper Equideductive Categories and their Logic. Some of the material in the Examples section of that paper may be moved here.

Remark 6.1 Recall that we used the name urtype in the sober λ-calculus that serves as the object language of equideductive logic. The reason for this is that we define a type to be an urtype together with a predicate,

{x : A | 𝔭(x)},

using the familiar “comprehension” or “subset-formation” notation from elementary set theory. Formally, these types behave in essentially the same way as contexts. We may also quantify over them, writing

∀x:{x : A | 𝔭(x)}. 𝔮(x) for ∀x:A. 𝔭(x) =▷ 𝔮(x)
�x:{x : A | 𝔭(x)}. 𝔮(x) for �x:A. 𝔭(x) & 𝔮(x).

These types provide the objects of the category of contexts and substititions for the logic. Morphisms are represented by uterms,

[figure: {x : A | 𝔭(x)}; .; .; .; .; .; {y : B | 𝔮(y)}; A; f; B]

where

x : A ⊢ fx : B such that x : A, 𝔭(x) ⊢ 𝔮(fx).

The same morphism may have many representing urterms, where

f = g if x : A, 𝔭(x) ⊢ fx = gx : B,

the latter being understood as the Leibnizian equality in Remark 2.5.

However, this simple definition of morphisms is based on the assumption that the urtype B is injective. For our purposes, it will be enough to take B ≡ Σ^{C}, so targets of maps are wlog of the form {Σ^{C} | 𝔯}.

Remark 6.2 In the category, quantified implication is represented by a partial product, for which see the main paper. Epis are orthogonal to partial product inclusions.

Remark 6.3 The functor Σ^{(−)} : B → B^{op} reflects invertibility.

Remark 6.4 The category Sob admits factorisation into epis (which are preserved by products) and regular monos (inclusions with the subspace topology).

Remark 6.5 Any equaliser is a partial product, so any regmono is in M, and conversely in Sob.

Remark 6.6 However, in the term model the class of regular monos is properly contained in M. Having a cokernel doesn’t help.

We need an example for which the predicate

∀y. αy = βy =▷ γxy = δxy

is not equivalent to ∀y. ϵxy = ζxy.

7 Factorisation

As our first application of the new quantifier to category theory, we show in this section that it agrees with the epis in the category, as we claimed in the Introduction. Epis are preserved by products and provide one of the classes of a factorisation system.

Notation 7.1 Let E be the class of morphisms e : X ≡ {A | 𝔭} → Y ≡ {B | 𝔮} for which

x : A, 𝔭(x) ⊢ 𝔮(ex) and y : B, 𝔮(y) ⊢ �x. (𝔭(x) & y = ex),

where the first condition is just the definition of a morphism. We shall show that E is the class of epis.

We also write M for the class of monos that arise from partial product diagrams. These are isomorphic to canonical inclusions {A | 𝔭} ↣ {A | 𝔮} with x : A, 𝔭(x) ⊢ 𝔮(x). The class M is therefore closed under composition.

All regular monos are in M but the converse need not be true.

Lemma 7.2 The second condition on E-maps is equivalent to

y : B, 𝔮(y) ⊢ ∀ϕ, ψ:Σ^{B}. (∀x:A. 𝔭(x) =▷ ϕ(ex) = ψ(ex)) =▷ ϕy = ψy.

Proof This is because

∀xy. 𝔭(x) & (y = ex) =▷ ϕy = ψy ⊣⊢ ∀x:A. 𝔭(x) =▷ ϕ(ex) = ψ(ex).  □

Lemma 7.3 Product with any type Z ≡ {C | 𝔯} preserves the E-property. Proof For any type Z ≡ {C | 𝔯}, Corollary 4.8 says that

z : C, 𝔯(z) ⊢ �z′. 𝔯(z′) & (z = z′).

So, given e ∈ E as above, we use Proposition 4.3 twice and Corollary 4.5 to deduce

y : B, z : C, 𝔮(y), 𝔯(z) ⊢ (�x. 𝔭(x) & (y = ex)) & (�z′. 𝔯(z′) & (z = z′))
⊢ �z′. (�x. 𝔭(x) & (y = ex)) & 𝔯(z′) & (z = z′)
⊢ �z′. �x. (𝔭(x) & (y = ex) & 𝔯(z′) & (z = z′))
⊢ �xz′. (𝔭(x) & 𝔯(z′) & ⟨y, z⟩ = ⟨ex, z′⟩),

so the map (e × Z) : X × Z ↠ Y × Z is also in E. □

Proposition 7.4 A map e : X → Y belongs to E iff it is epi:

[figure: X ≡ {A | 𝔭}; e; Y ≡ {B | 𝔮}; ϕ; ψ; Z ≡ {Σ^{C} | 𝔰}; Σ^{C}]

that is, it has the cancellation property that, whenever ϕ · e = ψ · e, already ϕ = ψ.

Hence the class E contains all isomorphisms and is closed under composition. Proof Suppose that e : X → Y is epi and let Z ≡ Σ. We may express the cancellation for this case in equideductive logic as

⊢ ∀ϕψ:Σ^{B}. (∀x:A. 𝔭(x) =▷ ϕ(ex) = ψ(ex)) =▷ (∀y:B. 𝔮(y) =▷ ϕy = ψy).

Using ∀E (Proposition 2.4) we may move ∀y:B. 𝔮(y) =▷ behind the ⊢ to get

y : B, 𝔮(y) ⊢ ∀ϕψ:Σ^{B}. (∀x:A. 𝔭(x) =▷ ϕ(ex) = ψ(ex)) =▷ ϕy = ψy,

which is the E-property.

Conversely, suppose that e ∈ E, so e×C ∈ E too for any urtype C by the Lemma. By reversing the previous argument, we have the cancellation property in the diagram

[figure: X × C; e × C; Y × C; ϕ̃; ψ̃; Σ.]

The exponential transpose of this is the epi property in the case Z ≡ Σ^{C}, but the general case follows from this because any object Z has a mono Z ↪ Σ^{C}. □

Conversely, we may recover the existential quantifier from the epis:

Proposition 7.5 Given any predicate y : B, z : C, 𝔰(y, z) ⊢ 𝔮(y),

y, B, 𝔮(y) ⊢ �z. 𝔰(y, z)

holds iff the map π_{0} : {y : B, z : C | 𝔰(y, z)} ⟶ {y : B | 𝔮(y)} is epi. Proof By Corollary 4.8, the condition for π_{0} ∈ E is that (𝔰 ⊢ 𝔯 and)

y : B, 𝔮(y) ⊢ �y′z. 𝔰(y′, z) & (y′ = y) ⊣⊢ �z. s(y, z).  □

Proposition 7.6 Any map factorises as f = m · e with e ∈ E and m ∈ M.

[figure: X ≡ {A | 𝔭}; e; Y ≡ {B | 𝔯}; m; Z ≡ {B | 𝔮}; A; f; B]

Proof Let the intermediate object Y be the image {B | 𝔯}, where

y : B ⊢ 𝔯(y) ≡ �x:A. 𝔭(x) & (y = ex),

so we already the second condition for e ≡ f : X → Y to be an epi. The first, that it is a well defined map, is

x : A, 𝔭(x) ⊢ 𝔯(fx),

which is �I.

The inclusion m : Y ↣ Z is also well defined because

y : B, 𝔯(y) ⊢ 𝔮(y)

by �E, from the defining property of f : X → Y, which was x : A, 𝔭(x) ⊢ 𝔮(fx). □

The universal property of this factorisation is expressed by

Proposition 7.7 The classes E and M are orthogonal, cf. Proposition 6.2.

A  \overline{e} B
[figure]
X ≡ {A | 𝔭}  [figure: e ∈ E] Y ≡ {B | 𝔮}
.................................. h

[figure: U ≡ {C | 𝔯}; f; m ∈ M; V ≡ {C | 𝔰}; g]
[figure]
[figure: C; f; = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = =; C; g]

in any commutative square like the one in the middle of this diagram, there is a unique map h : Y → U that makes both triangles commute. Proof Since the inner square commutes and m ∈ M, by Lemma 2.5,

x : A, 𝔭(x) ⊢ 𝔯(fx) and fx = g(ex), so 𝔯(g(ex)).

so x : A, y : B, 𝔭(x), (y = ex) ⊢ 𝔯(gy).

Since e ∈ E, y : B, 𝔮(y) ⊢ �x. 𝔭(x) & (y = ex),

and then �E gives y : B, 𝔮(y) ⊢ 𝔯(gy),

so (the given representative of) g also serves for h. □

Theorem 7.8 Any equideductive category has a factorisation system in which

(a) E consists of the epis and is stable under product; and

(b) M is the class of maps that arise from partial products. □

Corollary 7.9 In any particular context Γ, equideductive predicates form a lattice Sub(Γ), in which ⊥, ⋎ and � are joins.

This lattice need not be distributive, or even modular. Logically, these symbols allow weakening but not contraction or cut of variables. They only allow weakening by a hypothesis if it has no variable in common. Topologically, they are preserved by products but not by pullbacks or inverse images. Proof The foregoing results only apply to contexts consisting only of urtypes. A general context [x : A, 𝔭(x)] is a subspace of an urtype A, and Sub([x : A, 𝔭(x)]) = Sub(A) ↓ 𝔭 is still a lattice. □

Warning 7.10 Although our new connective � is very useful, it is not the same as the usual one on points, and so we must be extremely careful in using it.

Example 7.11 Let f : ℕ → Σ^{ℕ} be fn ≡ λm. m < n. Its factorisation

[figure: ℕ; ϖ ≡ {θ : Σ^{ℕ} | �n. θ = λm. m < n}; Σ^{ℕ}]

defines the ascending natural number domain when this diagram is interpreted in Sob. However,

θ : ϖ ⊢ �n. 𝔭(n, θ) but n : ℕ, 𝔭(n, ∞) ⊢ ⊥,

where 𝔭(n, θ) ≡ (θ = fn) and ∞ ≡ λm. ⊤ = ⋁ ; _{n} λm. m < n. □

Questions 7.12 (Giuseppe Rosolini)

(a) The variable rule for � is reminiscent of linear (rather, affine) logic; is there a monoidal structure that would explain this?

(b) Does the counit of this structure (Corollary 4.7) throw light on the need for the variablebinding rule in order to interpret �y : 1?

(c) Can one characterise the maps along which epis, � or the factorisation can be pulled back? The class of such maps may provide the dependent types.

Remark 7.13 There is another existential quantifier for maps with dense image:

�^{di}y:B. 𝔭(x, y) ≡ ∀ϕ:Σ^{A}. (∀x′y′. 𝔭(x′, y′) =▷ ϕ(x′) = ⊥) =▷ ϕx = ⊥.

8 Coproducts

In the second application of the new quantifier and disjunction, we now show that the category has finite coproducts.

Proposition 8.1 The initial object is 0 ≡ {Σ | ⊥}.

[figure: 0 ≡ {Σ | ⊥}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; {Σ^{C} | 𝔯}; Σ; κ : x ↦ λc. x; Σ^{C}]

Proof The dotted map is well formed because, by ⊥E,

x : Σ, ⊥ ≡ ∀στ. σ = τ ⊢ 𝔯(λc. x).

It is unique because

x, y : Σ, ⊥ ⊢ λc. x = λc. y.  □

Notation 8.2 The urtypes of the variables that we use are a : A, ϕ : Σ^{A}, b : B, ψ : Σ^{B}, H : Σ^{(Σ^{A}×Σ^{B})}, Θ : Σ^{2}(Σ^{A} × Σ^{B}), along with subscripts. Then define

ν_{0}a ≡ λϕψ. ϕa  ν_{1}b ≡ λϕψ. ψb
ϕ_{Θ} ≡ λa. Θ(ν_{0}a)  ψ_{Θ} ≡ λb. Θ(ν_{1}b)
ϕ_{1} ∼^{𝔭} ϕ_{2} ≡ ∀x. 𝔭(x) =▷ ϕ_{1}x = ϕ_{2}x  ψ_{1} ∼^{𝔮} ψ_{2} ≡ ∀y. 𝔮(y) =▷ ψ_{1}y = ψ_{2}y
X + Y ≡ {H | prime(H) & [𝔭, 𝔮](H)}  prime(H) ≡ ∀Θ. ΘH = Hϕ_{Θ}ψ_{Θ}

[𝔭, 𝔮](H) ≡ ∀ϕ_{1}ϕ_{2}ψ_{1}ψ_{2}. (ϕ_{1} ∼^{𝔭} ϕ_{2}) & (ψ_{1} ∼^{𝔮} ψ_{2}) =▷ Hϕ_{1}ψ_{1} = Hϕ_{2}ψ_{2}.

Of course, X + Y is for now just an abbreviation: we have to prove that it has the universal property of a coproduct, but first we explore the basic properties of this notation.

Lemma 8.3 This notation satisfies

\begin{matrix}ϕ ∼^{⊤} ψ & ⊣⊢ & ϕ = ψ & [𝔭, 𝔮](ν_{0}x) & ⊣⊢ & 𝔭(x) \\ [⊤, ⊤] & ⊣⊢ & ⊤ & [𝔭, 𝔮](ν_{1}y) & ⊣⊢ & 𝔮(y). \end{matrix}

Proof The first part is Axiom 2.1 and the second follows from this. For the third,

[𝔭, 𝔮](ν_{0}x) ≡ ∀ϕ_{1}ϕ_{2}ψ_{1}ψ_{2}. (ϕ_{1} ∼^{𝔭} ϕ_{2}) & (ψ_{1} ∼^{𝔮} ψ_{2}) =▷ ν_{0}xϕ_{1}ψ_{1} = ν_{0}xϕ_{2}ψ_{2}
⊣⊢ ∀ϕ_{1}ϕ_{2}. (ϕ_{1} ∼^{𝔭} ϕ_{2}) =▷ ϕ_{1}x = ϕ_{2}x ≡ 𝔭^{⊤}(x) ⊣⊢ 𝔭(x)

from Lemma 4.6, and the last one is similar. □

Lemma 8.4 The inclusion maps ν_{0} : X → X + Y and ν_{1} : Y → X + Y are well defined, mono and natural. Proof H ≡ ν_{0}a ≡ λϕψ. ϕa is prime because, for any Θ,

(ν_{0}a)ϕ_{Θ}ψ_{Θ} ≡ (λϕψ. ϕa)ϕ_{Θ}ψ_{Θ} ≡ ϕ_{Θ}a ≡ Θ(ν_{0}a).

We have already shown that if 𝔭(x) then [𝔭, 𝔮](ν_{0}x). The map ν_{0} is mono because

ν_{0}a = ν_{0}b ≡ λϕψ. ϕa = λϕψ. ϕb ⊣⊢ ∀ϕψ. ϕa = ϕb ⊣⊢ a = b

by Lemma 2.5 and Definition 2.5.

[figure: A; ν_{0}; Σ^{Σ^{A}×Σ^{B}}; ν_{1}; B]

[figure: C; f; ν_{0}; Σ^{Σ^{C}×Σ^{D}}; Σ^{Σ^{f} ×Σ^{g}}; ν_{1}; D; g]

For naturality,

Σ^{Σ^{f} ×Σ^{g}}(ν_{0}a) = λθξ. ν_{0}a(Σ^{f}θ)(Σ^{g}ξ)
= λθξ. (Σ^{f}θ)a
= λθξ. θ(fa) = ν_{0}(fa).  □

The key step in showing that X + Y is the coproduct is that the ν_{0}x for x ∈ {A | 𝔭} and ν_{1}y for y ∈ {B | 𝔮} “exhaust” X + Y, in an essentially familiar way, but using the new connectives ⋎ and � from Section 3. In traditional categorical language the inclusions X → X + Y ← Y are jointly epi, so this is the dual of extensionality for products (Axiom 2.1).

Proposition 8.5 For H : Σ^{Σ^{A}×Σ^{B}},

prime(H), [𝔭, 𝔮](H) ⊣⊢ (�x. 𝔭(x) & H = ν_{0}x) ⋎ (�y. 𝔮(y) & H = ν_{1}y).

Proof Let Γ be the context [H, prime(H), [𝔭, 𝔮](H)] on the left.

The backwards direction is the easy one. By Lemmas 2.2, 2.5 and 8.3,

H : Σ^{Σ^{A}×Σ^{A}}, x : A, 𝔭(x), (H = ν_{0}x) ⊢ prime(H) & [𝔭, 𝔮](H) ≡ Γ.

Then

H : Σ^{Σ^{A}×Σ^{A}}, �x. 𝔭(x) & (H = ν_{0}x) ⊢ Γ  �E

and H : Σ^{Σ^{A}×Σ^{A}}, RHS ⊢ Γ.  ⋎E

Conversely, to prove the disjunction on the right (Notation 3.2), we consider Θ_{1}, Θ_{2} : Σ^{2}(Σ^{A} ×Σ^{B}) such that

∀H′. (�x. 𝔭(x) & H′ = ν_{0}x) =▷ Θ_{1}H′ = Θ_{2}H′  (∗)

and ∀H′. (�y. 𝔮(y) & H′ = ν_{1}y) =▷ Θ_{1}H′ = Θ_{2}H′,  (†)

so we write Δ ≡ [Θ_{1}, Θ_{2}, ∗, †] for this context. We must deduce that Γ, Δ ⊢ Θ_{1}H = Θ_{2}H. For x : A with 𝔭(x), H′ ≡ ν_{0}x ≡ λϕψ. ϕx satisfies

x : A, 𝔭(x) ⊢ �x′. 𝔭(x′) & (H′ = ν_{0}x′)

by �I (Lemma 3.3), whence (∗) gives Θ_{1}H′ = Θ_{2}H′ in

Δ, x : A, 𝔭(x) ⊢ ϕ_{1}x ≡ ϕ_{Θ_{1}}x ≡ Θ_{1}(ν_{0}x) ≡ Θ_{1}H′ = Θ_{2}H′ ≡ ϕ_{2}x,

where ϕ_{Θ_{1}} was defined in Notation 8.2.

Hence Δ ⊢ ∀x. 𝔭(x) =▷ ϕ_{1}x = ϕ_{2}x, which is ϕ_{1} ∼^{𝔭} ϕ_{2}, and ψ_{1} ∼^{𝔮} ψ_{2} is similar. This means that we may invoke [𝔭, 𝔮](H) for the inner equality below, together with prime(H) for the outer ones:

Γ, Δ ⊢ Θ_{1}H = H(ϕ_{Θ_{1}}, ψ_{Θ_{1}}) ≡ Hϕ_{1}ψ_{1} = Hϕ_{2}ψ_{2} = Θ_{2}H,

which is what was required to prove the disjunction. □

Theorem 8.6 X + Y is the coproduct.

[figure: X ≡ {A | 𝔭}; ν_{0}; X + Y; ν_{1}; {B | 𝔮} ≡ Y]
[figure: g; ^{................}; h; ................; f]
{Σ^{C} | 𝔰} ≡ Z
[figure: A; ν_{0}; Σ^{Σ^{A}×Σ^{B}}; ν_{1}; B]
[figure: g; ^{................}; h; ................; f]
[figure: Σ^{C}]

Proof By Proposition 6.1, without loss of generality the test object Z is a canonical type, i.e. a subspace of some Σ^{C} with C ∈ A. Given f : X → Z ≡ {Σ^{C} | 𝔰} and g : Y → Z ≡ {Σ^{C} | 𝔰}, so

x : A, 𝔭(x) ⊢ 𝔰(fx) and y : B, 𝔮(y) ⊢ 𝔰(gy),

the mediator is necessarily the restriction of some h′ : Σ^{(Σ^{A}×Σ^{B})} → Σ^{C}, by injectivity of Σ^{C} (Lemma 2.1). Indeed,

hH ≡ λc. H(λa. fac, λb. gbc)

makes the diagram commute from A or B to Σ^{C} because

h(ν_{0}a) = λc. fac = fa and h(ν_{1}b) = λc. gbc = gb.

We must show that this h is a well defined map X + Y → Z and that it is the only one that makes the triangles commute. These are both applications of the general elimination rules for � and ⋎ in Section 3.

Since h(ν_{0}x) = fx and 𝔰(fx), by Lemma 2.5,

H, x : A, 𝔭(x), H = ν_{0}x ⊢ 𝔰(hH)
H, �x. 𝔭(x) & (H = ν_{0}x) ⊢ 𝔰(hH)  �E
H, (�x. 𝔭(x) & (H = ν_{0}x)) ⋎ (�y. 𝔮(y) & (H = ν_{1}y)) ⊢ 𝔰(hH)  ⋎E
H, prime(H), [𝔭, 𝔮](H) ⊢ 𝔰(hH)

by Proposition 8.5, so h is well defined. The uniqueness argument is similar:

H, x : A, 𝔭(x), H = ν_{0}x ⊢ h′H = fx = hH  given
H, �x. 𝔭(x) & (H = ν_{0}x) ⊢ h′H = hH  �E

and similarly with 𝔮(y) and H = ν_{1}y, so

H, (�x. 𝔭(x) & (H = ν_{0}x)) ⋎ (�y. 𝔮(y) & (H = ν_{q}y)) ⊢ h′H = hH  ⋎E
H, prime(H), [𝔭, 𝔮](H) ⊢ h′H = hH.

Hence h′ = h in the sense of Definition 6.1. □

9 Extensivity

Finally we show that the coproducts that we constructed in the previous section are stable and disjoint, and the initial object is strict. We do this using the modern categorical notion of extensivity [Cockett etc refs]:

Definition 9.1 A category is called extensive if, in any diagram

[figure: X; Z; Y; 1; 0; 2; k; 1; 1]

the top row is a coproduct iff the two squares are pullbacks.

Give a brief introduction to extensivity and distributivity, showing that the former entails that the initial object is strict and coproducts are stable and disjoint (Corollary ??).

We do, however, have to make a small additional assumption:

Lemma 9.2 If an equideductive category Q has disjoint coproducts then Σ has a point.

Proof If coproducts are disjoint then 0 → 1 ⇉ 2 is an equaliser. Then injectivity of Σ with respect to 0 → 1 provides a point 1 → Σ. □

Proposition 9.3 For any urtype A, the type 0 ≡ {A | ⊥} is a strict initial object, and

x : 0 ⊢ 𝔭(x)

for any predicate 𝔭.

[figure: 0 ≡ {A | ⊥}; h; .; .; .; .; .; .; .; k........; {Σ^{C} | 𝔰} ≡ Z; A; h; .; .; .; .; .; .; .; .; .; .; .; .; .; .; k..............; Σ^{C}]

Proof The judgement x : 0 ⊢ 𝔭(x) is x : A, ⊥ ⊢ 𝔭(x), which is ⊥E (Notation 3.1). The map 0 → Z is given by h ≡ λac. ⋆, and it is unique because x : 0 ⊢ hx = h′x.

If there is a also map k : Z → 0 then we already have k · h = id_{0} by uniqueness of maps out of 0. But also, z : Z ⊢ ⊥(kz) ⊢ h(kz) = z, so Z ≅ 0. □

Notation 9.4 2 ≡ 1 + 1 ≡ {Σ^{Σ×Σ} | prime} with elements 0 ≡ λστ. σ and 1 ≡ λστ. τ.

Proposition 9.5 These satisfy

(a) H : Σ^{Σ×Σ}, prime(H), σ : Σ ⊢ σ = Hσσ;

(b) H : 2, prime(H) ≡ ∀Θ. ΘH = H(Θν_{0}, Θν_{1}) ⊢ (H = 0) ⋎ (H = 1);

(c) the map 2 ↣ Σ^{Σ×Σ} is mono;

(d) ∀x:2. 𝔭(x) ⊣⊢ 𝔭(0) & 𝔭(1); and

(e) �x:2. 𝔭(x) ⊣⊢ 𝔭(0) ⋎ 𝔭(1). Proof Although [b] is an example of Proposition 8.5, the restriction on the use of ⋎ stops us from substituting into it. This is why we prove [a] first, using Proposition 8.5, and [b] follows from this. [c] This map is in M. [d,⊢] By ∀E. [d,⊣]

x : 2, 𝔭(0), 𝔭(1) ⊢ (x = 0 ⋎ x = 1) & 𝔭(0) & 𝔭(1)
⊢ (x = 0 & 𝔭(0)) ⋎ (x = 1 & 𝔭(1)) ⊢ 𝔭(x)

by weak Frobenius (Proposition 4.3), Lemma 2.5 and ⋎E. [e,⊣] By �I. [e,⊢] Using (d) and the definitions of � and ⋎,

�x:2. 𝔭(x) ≡ ∀στ. (∀x:2. 𝔭(x) =▷ σ = τ) =▷ σ = τ
⊢ ∀στ. ((𝔭(0) =▷ σ = τ) & (𝔭(1) =▷ σ = τ)) =▷ σ = τ
≡ 𝔭(0) ⋎ 𝔭(1).  □

The consequence of these properties of 2 is that any map Z → 2 gives rise to a partition of Z. That is, we may use pullbacks to split Z into two parts, and recover the original object as a coproduct.

If the two squares in the definition of extensivity above are pullbacks then the top row is a coproduct.

Lemma 9.6 Z ≡ {z : C | 𝔯(z)} ≅ {z : C | 𝔯(z) & kz = 0} + {z : C | 𝔯(z) & kz = 1}.

[figure: Z ≡ {C | 𝔯}; C; 2; k; Σ^{Σ×Σ}; k]

Proof By sobriety, the two sides of the claimed isomorphism are

Z ≡ {C | 𝔯}  ≅ {F : Σ^{Σ^{C}} | prime &𝔯^{⊤}}  Lemma 6.1
W ≡ {C | 𝔯 & k = 0} + {C | 𝔯 & k = 1} ≡ {H : Σ^{Σ^{C}×Σ^{C}} | prime &[𝔯 & k = 0, 𝔯 & k = 1]}.

We must therefore show that there is a bijection given by

F ≡ λθ. Hθθ and H ≡ λϕψ. F (λz. kz(ϕz)(ψz)).

[F ↦ H ↦ F]: From Proposition 9.4(b) we have

θ : Σ^{Σ×Σ}, prime(θ), σ : Σ ⊢ σ = θσσ.

Combining this with the defining property of k : Z → 2 ↣ Σ^{Σ×Σ},

z : C, 𝔯(z) ⊢ prime(kz)

gives z : C, 𝔯(z), ϕ : Σ^{C} ⊢ ϕz = kz(ϕz)(ϕz),

which means that ϕ : Σ^{C} ⊢ ϕ ∼^{𝔯} λz. kz(ϕz)(ϕz). Hence

prime(F), 𝔯^{⊤}(F) ⊢ F = λϕ. F (λz. kz(ϕz)(ϕz)).

[H ↦ F ↦ H]: If H = ν_{0}z with 𝔯(z) then F = ηz with prime(F) and 𝔯^{⊤}(F), so by �E,

H, �z. 𝔯(z) & (H = ν_{0}z) & (kz = 0) ⊢ λϕψ. F (λz. ϕz) = λϕψ. ϕz ≡ ν_{0}z = H.

By Proposition 8.5, prime(H), [𝔯 & k = 0, 𝔯 & k = 1] ⊢

(∃z. 𝔯(z) & kz = 0 & H = ν_{0}z) ⋎ (∃z. 𝔯(z) & kz = 1 & H = ν_{1}z).

Since we can recover H in each case, H ↦ F ↦ H by ⋎E. □

The converse of this is that the naturality squares for the coproduct inclusions are pullbacks. If both rows are coproducts then the squares are pullbacks.

Lemma 9.7 The square on the left is a pullback:

[figure: X ≡ {A | 𝔭}; ν_{0}; X + Y ≡ {Σ^{Σ^{A}×Σ^{B}} | prime &[𝔭, 𝔮]}; Σ^{Σ^{A}×Σ^{B}}]
[figure: ν_{0}]
A
[figure]
[figure: 1; 0; 2; k; Σ^{Σ×Σ}; k]

Proof The downward maps called k both take H to λστ. H(λa. σ, λb. τ). Then both maps from A to Σ^{Σ×Σ} take a to λστ. σ, so the quadrilateral commutes. Also, 2 → Σ^{Σ×Σ} is mono by construction, so the left-hand square commutes too.

We need to define a unique map

{H : Σ^{Σ^{A}×Σ^{B}} | prime(H) & [𝔭, 𝔮](H) & kH = 0} ⟶ {A | 𝔭},

so we let Γ be the context (object) on the left, in which

kH = 0 ⊣⊢ λστ. H(λa. σ, λb. τ) = λστ. σ.

First we exclude the possibility that

Γ, H = ν_{1}y ⊢ 0 = kH = 1 ⊢ λστ. σ = λστ. τ ⊣⊢ ∀στ. σ = τ ≡ ⊥.

Since 𝔭 ⋎ ⊥ ⊣⊢ 𝔭 (Lemma 4.2), Proposition 8.5 gives �x. 𝔭(x) & (H = ν_{0}x).

Using �E, we deduce from this and

H′ : Σ^{Σ^{A}×Σ^{B}}, x : A, (H′ = ν_{0}x) ⊢ H′ = λϕψ. H′ϕ(λb. ⋆)

that H = λϕψ. Hϕ(λb. ⋆) = λϕψ. F ϕ where F ≡ λϕ. Hϕ(λb. ⋆) and �x. F = ηx.

Hence F is prime, so by sobriety (Axiom 2.2) we may introduce

Γ ⊢ a ≡ focus F ≡ focus (λϕ. Hϕ(λb. ⋆)) : A,
with  F = ηa,  H = ν_{0}a and [𝔭, 𝔮](ν_{0}a) ≡ 𝔭(a)

by Lemma 8.3. It is unique by Lemma 8.4. □

Theorem 9.8 The category is extensive. □

Corollary 9.9 Coproducts are stable and disjoint, the initial object is strict and product distributes over coproduct: the map

(X × Z) + (Y × Z) ^{[⟨ν_{0}·π_{0},π_{1}⟩,⟨ν_{1}·π_{0},π_{1}⟩]} (X + Y) × Z

is an isomorphism. □

Proposition 9.10 The coproduct of any list of urtypes exists and has an exponential that is itself an urtype:

Σ^{0} ≅ 1,  Σ^{A+B} ≅ Σ^{A} × Σ^{B},  Σ^{∐ A_{i}} ≅ ∏_{i} Σ^{A_{i}}.

Proof Using distributivity, there is a natural bijective correspondence amongst maps

(Γ × A) + (Γ × B) ≅ Γ × (A + B) ⟶ Σ =

(Γ × A) → Σ ; = ; Γ → Σ^{A}  (Γ × B) → Σ ; = ; Γ → Σ^{B}

= Γ ⟶ Σ^{A} × Σ^{B}

and similarly between the unique maps 0 ≅ Γ × 0 → Σ and Γ → 1 ≡ Σ^{0}. □

10 Overt spaces

Depending on whether I decide to publish this paper separately from or alongside the others in the equideductive programme, it may be appropriate to add a narrative section about how the logic is developed into one for topology. In particular, an overt space is one for which the quantifier on predicates is represented by an urterm. Then something could be said about the role of overt spaces in the connection between general topology and recursion theory.

11 Recursion

This section is just parked here temporarily. It will form the core of another paper about discrete mathematics in equideductive topology.

Axiom 11.1 We express primitive recursion over the natural numbers in the restricted λcalculus by adding the base (ur)type ℕ and the introduction rules

⊢ 0 : ℕ and n : ℕ ⊢ n + 1 ≡ succ n : ℕ.  ℕI

The ℕE-rule is the recursion scheme, which we formulate with active and passive parameters as follows. For any urtype B and urterms

Γ ⊢ z : B and Γ, n : ℕ, b : B ⊢ s(n, b) : B,

there is an urterm

Γ, n : ℕ ⊢ r(n) ≡ rec(n, z, s) : B

that has the property that

Γ ⊢ r(0) = z : B  and Γ, n : ℕ ⊢ r(n + 1) = s(n, r(n)) : B.  ℕβ

The rec construction also respects equality (ℕE=) and the ℕη-rule is rec(n, 0, succ) = n.

In order to use ℕ in equideductive logic, we also need the

Axiom 11.2 The induction scheme for ℕ says that, for any predicate 𝔯(n) on ℕ (with no other parameters),

𝔯(0), ∀n:ℕ. 𝔯(n) =▷ 𝔯(n + 1) ⊢ ∀n:ℕ. 𝔯(n).

Remark 11.3 For logical and programming purposes it is more convenient to define combinatorial structures using the urtype 𝕋 of binary trees. These rename 0 as nil , and have a binary constructor [− | −] instead of the unary succ. The recursion scheme is easily adapted from that for ℕ, whilst the induction scheme,

𝔯( nil ), ∀xy:𝕋. 𝔯(x) & 𝔯(y) =▷ 𝔯([x | y]) ⊢ ∀z:𝕋. 𝔯(z),

obeys the variable-binding rule.

On the other hand, we cannot write

∀x. (∀y. y ≺ x =▷ 𝔯(y)) =▷ 𝔯(x) ⊢ ∀z. 𝔯(z)

to define a well founded relation ≺ because the variable-binding rule for x is violated in y ≺ x.

Lemma 11.4 ℕ ≅ 1 + ℕ (this is extensionality).

Proof n : ℕ ⊢ (n = 0) ⋎ (�m. n = m + 1) is

∀ϕψ:Σ^{ℕ}. (∀n′. n′ = 0 =▷ ϕn′ = ψn′) & (∀n. (�m. n = n + 1) =▷ ϕn′ = ψn′) =▷ ϕn = ψn,

which is an easy case of the induction scheme.

Theorem 11.5 In the category Cn_{L}^{∀}, ℕ is a parametric natural numbers object.

Γ × ℕ ^{Γ × succ} Γ × ℕ
[figure: Γ × 0]
[figure: Γ ≅ {A | 𝔭}; ζ; Y ≡ {Σ^{B} | 𝔮}; R; . . . . . . . . . . . . . . . .; S; Γ × ℕ × Y; ⟨id, R⟩; . . . . . . . . . . . . . . . . .]

[figure: A; ζ; Σ^{B}; S; A × ℕ × Σ^{B}]

Proof Categorically, the data are as shown above, and we have to find the map R. Symbolically, we are given

x : A, 𝔭(x) ⊢ ζ_{x} : Σ^{B}, 𝔮(ζ_{x})  DZ

and x : A, 𝔭(x), n : ℕ, ϕ : Σ^{B}, 𝔮(ϕ) ⊢ S_{x}(n, ϕ) : Σ^{B}, 𝔮(S_{x}(n, ϕ)).  DS

By syntactic injectivity (Theorem 2.3), without loss of generality, formation of the urterms ζ_{x} and S_{x}(n, ϕ) does not depend on the hypotheses. Therefore, by recursion in the restricted λ-calculus, there is a unique urterm

x : A, n : ℕ ⊢ R_{x}(n) : Σ^{B}

such that

x : A ⊢ R_{x}(0) = ζ_{x} : Σ^{B}  RZ

and x : A, n : ℕ ⊢ R_{x}(n + 1) = S_{x}(n, R_{x}(n)).  RS

Now consider the equideductive predicate

n : ℕ ⊢ 𝔯(n) ≡ ∀x:A. 𝔭(x) =▷ 𝔮(R_{x}(n)).

By the hypotheses DZ and DS, the two equations RZ and RS for R_{x}(n) and ∀I, this satisfies

⊢ 𝔯(0) ≡ ∀x:A. 𝔭(x) =▷ 𝔮(ζ_{x})

and

𝔯(n) ≡ ∀x:A. 𝔭(x) =▷ 𝔮(R_{x}(n)) ⊢ 𝔯(n + 1) ≡ ∀x:A. 𝔭(x) =▷ 𝔮(S_{x}(n, R_{x}(n))).

Therefore the induction scheme gives ⊢ ∀n. 𝔯(n), which by ∀E is

n : ℕ, x : A, 𝔭(x) ⊢ 𝔮(R_{x}(n)),

but this says that the morphism R : Γ × ℕ → Y is well defined. It makes the triangle and square commute because it did for urterms. To show that it is unique we consider induction for the predicate

𝔯(n) ≡ ∀x. 𝔭(x) =▷ R′_{x}(n) = R_{x}(n).  □