Subject: categories: Re: intuitionism and disjunction

From: Thomas Streicher <[email-masked]>
Date: Wed, 1 Mar 2006 16:17:34 +0100 (CET)

W.r.t. to the discussion on intuitionism and disjunction I would like to
remark that this relation depends heavily on whether the ambient setting is
predicative or not. In an impredicative setting like toposes (or the Calculus
of Constructions) one may define disjunction and existential quantification
`a la Russell-Prawitz by quantification over \Omega (that's what (some)
logicians call impredicative, i.e. the possibility to quantify over
propositions and thus also predicates).
However in a first order setting this is not possible. E.g. if one considers
Heyting arithmetic with ist usual axioms and as logic the
\neg,\wedge,->,\forall fragment of first order logic then all formulas are
provably double negation closed. This shows that disjunction and existence
are not definable from the rest via first order logic.

So far the logical side. What Paul Levy had in mind was slightly different
as I understand it. Categories of domains (cpos with \bot) are cartesian
closed and have weak finite sums but certainly no proper finite sums
(since every map has a fixpoint). For modelling his CBPV paradigm he needs
in addition a category of predomains which is bicartesian closed. The former
is an example of a ccc which is not bicartesian but can be embedded into the
latter which is.

So one doesn't get for free the finite sums from a ccc which is problematic
both in logic and semantics of computation.

Thomas

---

From: Paul B Levy <[email-masked]>
Date: Fri, 3 Mar 2006 12:41:29 +0000 (GMT)

> propositions and thus also predicates).

In the topos situation, we are really concerned with intuitionistic
provability, not with proof equality.  A model of intuitionistic
provability is a bi-Heyting algebra.  I agree that, in the provability
setting, disjunction can be encoded in terms of impredicative universal
quantification,

However, when we are concerned with proof-equality, this encoding doesn't
work as a translation of equational theories.  I mean that the eta-law for
the (encoded) sum types cannot be proved in the beta-eta-theory for
polymorphism.  (If we incorporate Plotkin-Abadi logic into the target
theory into, then the encoding works, if I recall correctly, but the
target theory isn't equational any more.)

> are not definable from the rest via first order logic.

Agreed.

> So far the logical side. What Paul Levy had in mind

I didn't have CBPV in mind; that is a calculus for effects (such as
divergence).

My point was just that intuitionistic logic corresponds to "pure" type
theory: no divergence or other effects.  Therefore a bi-ccc is required to
model it.  Categories that are suitable for modelling effects, such as the
category of domains, won't do for modelling intuitionistic proofs,

Admittedly, if we follow John's suggestion of weakening beta-eta laws into
morphisms a la Neil Ghani, then we won't need a bi-ccc any more.  All I am
saying is that, *if* we require the eta law for function types, then we
should also require it for sum types.

Paul

---

From: Robert Seely <[email-masked]>
Date: Fri, 3 Mar 2006 15:20:49 -0500 (EST)

> should also require it for sum types.

A couple of remarks about this.  First the trivial one: "bi-ccc" is a
misleading term (I've used it myself, with the same confusion induced
in others), when all you mean is a ccc with coproducts.

More importantly, when you look at the structure of proofs in
intuitionist logic, you find that sum and product are not really dual
- though I have to admit this is very much a matter of presentation.
The problem is an old one: Zucker (in the early 70's I think) pointed
out that normalization steps are not the same as cut elimination
steps, particularly for disjunction.  I looked at this in my 1977
thesis, using natural deduction (in the Gentzen-Prawitz formulation)
for the logic (this has the advantage over the sequent calculus of
giving a category without need for any equivalence relation on
derivations).  Taking eta and beta (one an expansion, the other a
reduction) as 2-cells, I looked at the 2-categorical structure of the
connectives (and quantifiers, though really forall and exists are very
similar respectively to conjunction and disjunction, not
surprisingly).  It's easy to see that conjunction is a weak adjoint
without any further structure, but disjunction is NOT - unless you add
some permuting conversions (equivalences): in fact exactly the
permuting rewrites Prawitz had already identified earlier.  And
function types are a mess in this setting, unless you make the
conjunction a real product (again by introducing equivalences - this
time just beta and eta).  You can find a sketch of all this in two
extended abstracts I published: one in the Durham 1977 Category
Meeting ("Applications of sheaves ...", SLNM 753), and the other in
LICS 1987.  (Both are available on my webpage.)

(BTW - this was all done long before Ghani looked at the matter
... Barry Jay also subsequently looked at this.  But the higher
dimensional structure of intuitionist logic is still largely
un-studied, and merits serious attention.)

-= rags =-

-- 
<[email-masked]>
<www.math.mcgill.ca/rags>

---

From: Thomas Streicher <[email-masked]>
Date: Mon, 6 Mar 2006 11:28:31 +0100 (CET)

I just want to remark that the second order encoding of disjunction `a la
Russell-Prawitz is not bound to work only for provability. E.g. in PER(N)
it holds that (\forall X) (A->X) -> (B->X) -> X is isomorphic to A + B.
(A related result for "polymorphic" natural numbers was proved by Peter Freyd
and extension of this result to polymorphic encodings free algebras was obtained
a bit later by Hyland, Robinson and Rosolini).
If your data type A lives in PER(N) then the 2nd order order encoding of
existential quantification

    (\exists x:A) P(x) \equiv (\forall Q) ((\forall x:A) P(x) -> Q) -> Q

is isomorphic to (\Sigma x:A) P(x) and thus we can project out the witness.
In the extended calculus of constructions XCC where Prop (i.e. PER(N)) closed
under small sums one can syntactically prove

      (\exists x:A) P(x)  \equiv  (\Sigma x:A) P(x)

and thus one can extract witnesses from proves of (\exists x:A) P(x).
Admittedly, this equivalence is not an isomorphism in general but it is in
PER(N) and a lot of other relizability models. (A tricky counterexample for
the general case was proided by Ivar Rummelhoff a cople of years ago!)

Thus in an impredicative setting the positive operations turn out as 2nd order
definable from -> and \forall.

The main defect of Domains (with bottom) as a model for proofs is that every
type = domain contains an element, namely bottom. But weak coproducts are
definitely available.

If one integrates dynamics = rewriting = computation into the model by
considering 2-categories things might turn out as different. However, there
are no indications (as far as I know) that this 2-categorical setting makes
sums definable from lambda calculus.

Thomas

PS Peter Freyd has remarked that the early constructivists (implicitly)
considered as an earmark of constructivity that

   (E)  |= \exists x:A. P(x)  entails that  |= P([a/x]  for some  a : 1 -> A

I am not going to contradict that BUT it definitely fails already for boolean
toposes: consider the topos Psh(G) for G a nontrivial group and A the
representable presheaf then it holds in Psh(G) that  \exists x:A. x=x
although A hasn't any global section.
Of course, Peter Freyd's glueing argument shows that in the free topos (E)
holds. This certainly is a most beautiful argument. Nevertheless, I think
it doesn't tell that (E) is necessarily an earmark of constructivity since
the free models (i.e. formulas modulo provability) are not necessarily
the intended models. Moreover, (E) holds in realizability models (as long as
type A is \neg\neg-separated, i.e. an assembly).