Two Intermediate notions of disjunction

[Martin Escardo]

Quite accidentally, I have come across the following situation. It is
quite likely that some of you have seen the observations below before.

I'd like to know if you have seen things like this and/or have
something to add.

Work in (a suitable) intuitionistic logic (in which what I say below
can be formulated).

Say that a binary operation _%_ on propositions is an "intermediate
disjunction" if we have the chain of implications

p\/q -> p%q -> ¬(¬p/\¬q).

We say that p\/q is the intuitionistic disjunction of p and q, and
that ¬(¬p/\¬q) is their classical disjunction.

I have come accross two examples.

(2) The second example, distilled from the first, was

p$q := (p->q)->q.

This is an intermediate disjunction operation, but is not commutative
in general. Or, more precisely, we have that it is commutative iff
excluded middle holds:

(forall p,q, p$q->q$p) <-> (forall p, p\/¬p).

It always satisfies right-excluded middle:

forall p, p $ ¬p.

It also satisfies weak left-excluded middle:

forall p, ¬¬p $ ¬p.

But it satisfies (strong) left-excluded middle iff excluded middle
holds:

(forall p, ¬p $ p) <-> (forall p, p\/¬p).

Finally, we have that $ agrees with intuitionistic disjunction iff
excluded middle holds:

(forall p,q, p$q -> p\/q) <-> (forall p, p\/¬p).

So, in summary, TFAE:

- $ agrees with \/.
- Forall p, p\/¬p (excluded middle holds).
- $ is commutative.
- Forall p, ¬p $ p.

So, in particular, in classical logic, $ is the good old \/.

(1) The first example I stumbled upon was

p£q := p$q /\ q$p,

the commutativivization of $. This is again an intermediate
disjunction, of course.

But, what we have, instead, is that the following are equivalent:

- £ agrees with \/.
- Goedel-Dummett linearity (forall p,q, (p->q) \/ (q->p)).

Hence we can sensibly call £ "(Goedel-)Dummett disjunction" for
intuitionistic logic. We have that weak £-excluded middle holds:

forall p, ¬p£¬¬p.

But £-excluded middle holds iff excluded middle holds - TFAE:

- Forall p, p £ ¬p.
- Forall p, p \/¬p.

Hence again £ is just \/ is classical logic.

So the main difference between (1) and (2) is that the agreement of
intuitionistic disjunction with the intermediate disjunction is
respectively equivalent to the linearity axiom and the excluded middle
axiom.

Martin
--
Here is a file with the proofs in Agda notation in the MLTT case
(other logics with different notions of proposition, such as topos
type theory, CoC, HoTT, etc. also give the same results, with
essentially the same proofs), which also have some bibliographic
references a just a little bit more:

http://www.cs.bham.ac.uk/~mhe/Dummett-disjunction/Dummett-disjunction.html

[Robert Lubarsky]

Interesting observations.

I've never thought about anything like this. You may want to consult Linear Logic, which has decomposed the logical connectives. Maybe these have already come up there.

Bob

--
You received this message because you are subscribed to the Google Groups "constructivenews" group.
To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Paulo Oliva]

On 6 Sep 2016, at 21:14, Martin Escardo <m.es...@cs.bham.ac.uk> wrote:

(2) The second example, distilled from the first, was

 p$q := (p->q)->q.

This is an intermediate disjunction operation, but is not commutative
in general.

Hi Martin

This form of disjunction is used to axiomitise Lukasiewicz logic. Essentially,

Lukasiewicz logic is affine logic (linear logic + weakening) plus the

commutativity of p$q, i.e.

(*) p$q -> q$p

(Forth axiom in https://en.wikipedia.org/wiki/Łukasiewicz_logic)

The unit interval is sound and complete for Lukasiewicz logic, with true as 0,

false as 1, and implication as cut-off subtraction. p$q is interpreted as min(p,q).

Now what classical logic has that Lukasiewicz logic doesn’t is contraction:

(p -> p -> q) -> (p -> q)

With contraction one can then show that p$q coincides with the classical disjunction.

Your other construction, the commutativivization of $, I think has been used

to turn models of affine logic into models of Lukasiewicz logic. 

Note that (*) implies the double negation elimination (taking q = false), so in some

sense it’s a classical principle.

The intuitionistic version (kind of dual) is

p%q := p + (p -> q)

where + denotes the “multiplicative” conjunction (the one for which contraction doesn’t hold).

This is a form of conjunction, and the commutative of % can be used to define an

intuitionistic version of Lukasiewicz logic.

(see http://www.eecs.qmul.ac.uk/~pbo/papers/paper045.pdf)

Cheers,

--

Dr Paulo Oliva

Reader in Mathematical Logic

School of Electronic Engineering and Computer Science

Queen Mary University of London, London E1 4FZ

+44 (0) 207 882 5255

http://www.eecs.qmul.ac.uk/~pbo

[Paul Taylor]

Martin Escardo asked about forms of disjunction in partly classical
logic. I am not sure whether his emphasis was on intermediate
disjunction or intermediate classicality, but I will assume the former.

My own principal motivation for commenting on this question is to
ask for the historical origins of analogous formulae to Martin's
for the existential quantifier, in order to help me write the
introduction to my paper on the interpretation of these formulae
in my Equideductive Logic.


FORMULAE FOR DISJUNCTION

> Say that a binary operation _%_ on propositions is an
> "intermediate disjunction" if we have the chain of implications
>
> p\/q -> p%q -> ¬(¬p/\¬q).
>
> We say that p\/q is the intuitionistic disjunction of p and q,
> and that ¬(¬p/\¬q) is their classical disjunction.

The simpler of Martin's two examples of _%_ is

> p$q := (p->q)->q.

This "definition" of disjunction appears as the first sentence of
paragraph 18 of Bertrand Russell's "Principles of Mathematics"
(CUP 1903, not to be confused with the Principia Mathematica 1910-13).

The same paragraph of Russell's goes on to give another definition
of disjunction that presses the idea more strongly:

p U q := All s. (p->s) /\ (q->s) -> s

We would say that this is second order logic, although since Russell
believed excluded middle, for him s could only take two values.

In particular, letting s be p and then q, p U q entails

( (p->p) /\ (q->p) -> p ) /\ ( (p->q) /\ (q->q) -> q )

which (since p->p and q->q are redundant) is Martin's second example:

> p£q := p$q /\ q$p,

I'll skip Martin's further comments that seem to be about intermediate
forms of classicality, although they are intriguing.


EXISTENTIAL QUANTIFICATION

Early in my logical education I was told to find similar second order
formulae for the existential quantifier in Russell's Principles too.
However, so far as I can gather, they are not there. The Principia
is impenetrable, but last time I dared enter it in search of this
formula, I couldn't find it there either.

The formula I mean occurs in Jean-Yves Girard's System F in the form

Sigma X.T(X) := Pi Y. (Pi X. T(X) -> Y) -> Y.

This is really the same idea as the formula for disjunction, so surely
if Russell didn't have it, somebody not long him after must have found it.

I would very much like to know the original citation.


EQUIDEDUCTIVE LOGIC

My own interest in this question arises from the fact that formulae
similar to these can be written in my equideductive logic, even though
it is not second order logic or even a Heyting algebra.

There are several draft papers in this programme, mostly written in
2008/9:

www.paultaylor.eu/ASD/equideductive

The first sets out the category theory and logic itself and the second
shows how forms of disjunction and existential quantification can be
defined in it. Categorically, it arises from the interaction of
equalisers and exponentials in cartesian closed extensions of categories
of spaces. Logically, the formulae are generated from equations between
lambda terms by universally quantified implications.

In this setting the "existential quantifier" obeys the usual rules but
not substitution or the Frobenius law. Categorically, it corresponds
to (Sigma-)epis just as the usual quantifier corresponds to epis in
the category of sets and there is a factorisation system with regular
monos that is preserved by products and not pullbacks.

I would like to know the historical origins of the formulae, especially
for the existential quantifier, in order to write the introduction
to this paper properly.

Paul Taylor

[Toby Bartels]

Paul Taylor wrote in part (quoting Russell):

> p U q := All s. (p->s) /\ (q->s) -> s

Note that this is perfectly correct constructively (at least if we accept second-order reasoning as constructive). (As I'm sure you know, Paul.)

Paul noted that taking s to be p or q gives $ or its reverse (conjoining which gives £). Similarly, taking s to be FALSE gives classical disjunction. So these are all special cases of second-order constructive disjunction, ones which classically imply all other cases. (On the other hand, if we take s to be p \/ q itself, by which I mean actual constructive disjunction, then this special case implies all other cases even constructively, although of course that is no use as a definition.)

More generally, write p \/_s q for (p->s) /\ (q->s) -> s. If s and t are both statements that entail p \/ q, then if s entails t, then p \/_t q entails p \/_s q (contravariant). This is why $ and co-$ are independent but each entails classical-\/ (and so their conjunction, £, is intermediate); on the other hand, all of these are entailed by p \/ q. So we get a version of % by taking p \/_s q for any s that entails p \/ q.


—Toby Bartels

[Martin Escardo]

These remarks were already present in the Agda file I linked, and,
indeed, this is how I came to p£q, as explained there.

I also did discuss the existintial quantifier in the linked file, but
not in the constructive news message itself.

Martin