intuitionism and disjunction

intuitionism and disjunction

[Peter Freyd]

Paul Levy writes

  ...a model of intuitionistic logic is a *bi*cartesian closed category.

  I see no reason to regard disjunction as more "peripheral" to
  intuitionistic logic than implication.  (And, likewise, no reason to
  regard sum types as more peripheral to simple type theory than function
  types.)  Does anybody disagree?

The original intuitionists did, of course, see such reasons. But for
those who don't care about such issues as the nature of mathematical
existence there's this reason: if by a *bi*cartesian closed category
one were to mean a ccc category whose dual is also ccc then one would
be stuck with that fact that all *bi*cartesian closed categories are
just pre-ordered sets.

The status of disjunction and sum types in the presence of function
types is, indeed, significantly different from the status of
conjunction and products types.

Let me take the occasion to record a factoid I don't think I ever had
an excuse to record before (and don't really have one now). Define the
notion of a Heyting semi-lattice (HSL) by removing disjunction and
bottom from the definition of Heyting algebra. Define a _linear_ HSL
as one that satisfies the further equation

    ((x -> y) -> z) ^ ((y -> x) -> z)  =  z

e.g. any linearly ordered set with top (indeed, every linear HSL is
representable as a sub HSL of a product of linear ones).

In a linear HSL one may construct disjunction as

    ((x -> y) -> y) ^ ((y -> x) -> x)

The factoid of interest is this sort-of converse: the only HSL
varieties in which every member is a lattice are varieties of linear
HSLs.

Re: intuitionism and disjunction

[Paul B Levy]

Dear Peter.

>   I see no reason to regard disjunction as more "peripheral" to
>   intuitionistic logic than implication.  (And, likewise, no reason to
>   regard sum types as more peripheral to simple type theory than function
>   types.)  Does anybody disagree?
>
> The original intuitionists did, of course, see such reasons. But for
> those who don't care about such issues as the nature of mathematical
> existence

Can you explain the "of course" here, please?  What were these reasons,
and do they still hold water? I would have thought that tuples pose
less of an ontological difficulty than functions.

> there's this reason: if by a *bi*cartesian closed category one were to
> mean a ccc category whose dual is also ccc

What I meant was cartesian closed category with finite coproducts.

> then one would be stuck with that fact that all *bi*cartesian closed
> categories are just pre-ordered sets.
>
> The status of disjunction and sum types in the presence of function
> types is, indeed, significantly different from the status of
> conjunction and products types.

I don't know what you mean - maybe that product types are more similar to
function types than sum types are?  If so, I agree, but I was comparing
function types with sum types, not (function and sum) with (function and
product).

Paul

Re: intuitionism and disjunction

[Peter Freyd]

Paul Levy asks how the original intuitionists viewed disjunction. I
don't know how to say it better than this paragraph from Wikipedia
(anyone know who wrote it?).

  The disjunction and existence properties are validated by
  intuitionistic logic and invalid for classical logic; they are key
  criteria used in assessing whether a logic is constructive.... The
  disjunction property is a finitary analogue, in an evident sense.
  Namely given two or finitely many propositions P_i, whose
  disjunction is true, we want to have an explicit value of the index
  i such that we have a proof of that particular P_i. There are quite
  concrete examples in number theory where this has a major effect.

It is a (meta)theorem that in free Heyting algebras and free topoi
(and all sorts of variations thereon) that the disjunction property
holds. In the free topos that translates to the statement that the
terminator, 1, is not the join of two proper subobjects. Together with
the existence property it translates to the assertion that  1  is an
indecomposable projective object -- the functor it represents (i.e.
the global-section functor) preserves epis and coproducts. (And with
a little more work one can show it also preserves co-equalizers.)

Re: intuitionism and disjunction

[Paul B Levy]

I agree that intuitionistic logic satisfies the disjunction property.
But I don't see why this should make disjunction a more peripheral part of
intuitionistic logic than implication.

Paul

> Paul Levy asks how the original intuitionists viewed disjunction. I
> don't know how to say it better than this paragraph from Wikipedia
> (anyone know who wrote it?).
>
>   The disjunction and existence properties are validated by
>   intuitionistic logic and invalid for classical logic; they are key
>   criteria used in assessing whether a logic is constructive.... The
>   disjunction property is a finitary analogue, in an evident sense.
>   Namely given two or finitely many propositions P_i, whose
>   disjunction is true, we want to have an explicit value of the index
>   i such that we have a proof of that particular P_i. There are quite
>   concrete examples in number theory where this has a major effect.
>
> It is a (meta)theorem that in free Heyting algebras and free topoi
> (and all sorts of variations thereon) that the disjunction property
> holds. In the free topos that translates to the statement that the
> terminator, 1, is not the join of two proper subobjects. Together with
> the existence property it translates to the assertion that  1  is an
> indecomposable projective object -- the functor it represents (i.e.
> the global-section functor) preserves epis and coproducts. (And with
> a little more work one can show it also preserves co-equalizers.)
>
>
>

-- 
Paul Blain Levy              email: pbl@cs.bham.ac.uk
School of Computer Science, University of Birmingham
Birmingham B15 2TT, U.K.      tel: +44 121-414-4792
http://www.cs.bham.ac.uk/~pbl

Re: intuitionism and disjunction

[Toby Bartels]

Peter Freyd wrote:

>Paul Levy asks how the original intuitionists viewed disjunction. I
>don't know how to say it better than this paragraph from Wikipedia
>(anyone know who wrote it?).

>From the editing history <http://en.wikipedia.org/w/index.php?
 title=Disjunction_and_existence_properties&action=history>:
it looks like the part before the ellipsis
was written by English Wikipedia User Chalst
<http://en.wikipedia.org/wiki/User:Chalst>,
who is apparently Charles Stewart, a postdoc
at the International Centre for Computational Logic;
and the rest was written by English Wikipedia User Charles Matthews
<http://en.wikipedia.org/wiki/User:Charles_Matthews>,
who is now a hobbyist but was once an academic mathematician.
(I'm familiar with Charles Matthews and trust him,
if my opinion matters to anybody; I don't know Chalst.)
Of course, either may have copied from somewhere else
without proper attribution (that's been common ~within~ Wikipedia
--that is copying or moving from one WP article to another--
but it's pretty rare ~into~ Wikipedia, in my experience.)

>  The disjunction and existence properties are validated by
>  intuitionistic logic and invalid for classical logic; they are key
>  criteria used in assessing whether a logic is constructive.... The
>  disjunction property is a finitary analogue, in an evident sense.
>  Namely given two or finitely many propositions P_i, whose
>  disjunction is true, we want to have an explicit value of the index
>  i such that we have a proof of that particular P_i. There are quite
>  concrete examples in number theory where this has a major effect.

>It is a (meta)theorem that in free Heyting algebras and free topoi
>(and all sorts of variations thereon) that the disjunction property
>holds. In the free topos that translates to the statement that the
>terminator, 1, is not the join of two proper subobjects. Together with
>the existence property it translates to the assertion that  1  is an
>indecomposable projective object -- the functor it represents (i.e.
>the global-section functor) preserves epis and coproducts. (And with
>a little more work one can show it also preserves co-equalizers.)

I'm not sure how this affects Paul Levy's point,
but I guess that I'll let Paul speak on that.


-- Toby

Re: intuitionism and disjunction

[Thomas Streicher]

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

Re: intuitionism and disjunction

[Paul B Levy]

On Wed, 1 Mar 2006, Thomas Streicher wrote:

> 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).

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.)

> 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.

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

Re: intuitionism and disjunction

[Robert Seely]

On Fri, 3 Mar 2006, Paul B Levy wrote:

> 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.

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 =-

-- 
<rags@math.mcgill.ca>
<www.math.mcgill.ca/rags>

Re: intuitionism and disjunction

[Thomas Streicher]

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).