Relaxation of BHK interpretation that doesn't require empty type?

[Sunrise Confusion]

The standard way of doing logic in type theory uses the BHK interpretation. In particular, a proposition A is translated to a type A, and the proposition "NOT A" is translated to the type A->0. This requires the empty type. I was wondering about a somewhat different way of doing logic, which doesn't require the empty (or unit) type or an explosion principle. Namely, instead of representing a proposition A by one type, we translate it to two types PA, NA (or, if you wish, a tuple (PA,NA)). An inhabitant of PA is supposed to imply that A is true, and one of NA is supposed to imply that A is false. In the end, this seems to be enough to do propositional (and I think also predicate) calculus to me. For a start, we can still define (using non-nullary coproduct, product, dependent pair, dependent function types) any logical connectives we like:

-given A=(PA, NA) and B=(PB, NB), define A & B:==(PA x PB, NA+NB)==(PC,NC) (with == denoting judgmental equality). Then an inhabitant of PC can be constructed iff we have inhabitants of PA and PB (i.e. if we know that both A and B are true), and one of NC iff we know that one of them is false.

-similarly, for OR define A v B :==(PA + PB,NA x NB).

-NOT A :==(NA, PA).

-forall x A(x) gets translated to (\Pi_{x} PA(x), \Sum_{x} NA(x)),

-exists x A(x) to (\Sum_{x} PA(x), \Pi_{x} NA(x)).

I was interested in this for some specific reason (which I hope to discuss soon). But more generally, the reason this might be interesting from a philosophical (or maybe also technical) point of view is that it gives us more flexibility when one wants to assume that A is false. If NOT A is translated to the function type A->0, as far as I understand the only way one could add the assumption that A is false would be by setting A:==0 itself (and then using 0-recursion to construct q:0->0). In contrast, if NA could be any type, we can add the assumption that it is inhabited and still consider PA, NA as interesting objects with internal structure. This seems to be in accordance with the homotopy philosophy, where one wants to be able to say that things are "nontrivially the same" (two statements are false) but not "trivially the same" (two statements are judgmentally equal to the empty type).

I am sure that such an approach must have appeared in the literature somewhere, in some form, already - but I didn't find anything on Google. I also didn't get an answer when posting something similar on tcs.sx. Could someone give me a pointer?

Thinking about it, I claim the following (I'll go into more details/try to produce Coq if there is interest and noone quickly points me to a paper that discusses this):

1. In this formalization, the asymmetry between LEM and absurdity which is present in the full BHK interpretation would be reduced. In BHK, "forall P (P v NOT P)" is nontrivial and can't be derived from 1. The categorically opposite statement about absurdity, "exists P (P ^ NOT P)", is trivially wrong, i.e. can be used to derive 0. In the formalization above, LEM and ABS can't be derived from nothing resp. be used to derive anything, and constructions involving them are roughly related to each other by reversing the arrows (and exchanging products with coproducts). For example:

Denote by LEM(A)==LEM((PA,NA)) the type PA + NA, and by ABS(A)==ABS((PA,NA)) the type PA x NA. Then whenever we have defined a new type C==(PC,NC) by a Boolean expression from A and B as A ^ B, A v B, or NOT A as above, (I claim that) we can use the recursors of +,x to define a function l_C:(LEM(A) x LEM(B))->LEM(C) resp. l_C:LEM(A)->LEM(C). In words, if we know that LEM holds for A and B, we can conclude that it must hold for C as well. We can also define "categorically opposite" functions r_C:ABS(C)->(ABS(A)+ABS(B)) resp. r_C:ABS(C)->ABS(A), i.e. if the constructed proposition is absurd, then one of the propositions used in the construction must already have been absurd.

For quantification (which, I have to point out, I checked less thoroughly, as I was mainly interested in the PK proof system), the situation seems to be less symmetric: Deriving absurdity still works easily; we can e.g. construct

r_C: ((\Pi_{x} PA(x)) x (\Sum_{x} NA(x)) -> (\Sum_{x} (PA(x) x NA(x))),

but I don't see how one could directly define a function 

l_C: (\Pi_{x} (PA(x) + NA(x))) -> (\Pi_{x} PA(x)) + (\Sum_{x} NA(x)).

But nevertheless, I think it's possible to construct such an l_C "along the way" when we are constructing the dependent types PA: P->U and NA: P->U from more elementary types using +, x (i.e. when we are defining PA and NA using + and x-recursion, or possibly recursion over other types such as an integer type).

1.5 By concatenating the functions l and r above, we can efficiently construct l_P: LEM(A_1)xLEM(A_2)xLEM(A_3)x...->LEM(P) whenever we build a Boolean expression P out of some atomic type tuples A_1,A_2,A_3,...  Conversely, an absurdity in P can be converted to an absurdity of one of the atomic type tuples.

2. We can efficiently convert an arbitrary PK sequent calculus proof (without a symbol representing absurdity) into type theory in this interpretation. I think this also works for LK proofs, but I didn't check it carefully enough so far to claim anything. This works as follows:

-For each atomic proposition A_i appearing in the proof (of which there will be finitely many), we assume a tuple of types A_i==(PA_i,NA_i):U x U (equivalently, all objects constructed are dependent functions taking A_i as input).

We also define the types LEM_0:==LEM(A_0)xLEM(A_1)x..., ABS_0:==ABS(A_0)+ABS(A_1)+..., expressing LEM resp. absurdity for the atomic propositions.

-Any Boolean expression P appearing in the proof is translated to a constructed type as in 1. While performing these constructions, we construct the LEM/ABS functions l_B:LEM_0->LEM(B), r_B:ABS(B)->ABS_0 along the way as in 1.5.

-A sequent of the form A_1,A_2,... |- B_1,B_2,... gets translated to a function (LEM_0 x PA_1 x PA_2 x ...) -> (PB_1 + PB_2 + ... + ABS_0). In words, we take LEM (over the atomic propositions) as additional required assumption, and add an absurdity in one of the atomic propositions as additional possible conclusion.

Then for each admissible deduction of sequents, one can write down a corresponding well-typed construction in type theory. The non-intuitionistic rules (NOT-introduction) will use the LEM_0 assumption (when NOT is introduced on the right side) or consider ABS_0 as a possible conclusion (when NOT is introduced on the left side), using the constructed l_B rest. r_B functions for the expression B that changes the side of the sequent.

I finally have the following question that I couldn't answer: A deduction of a Boolean tautology in PK, i.e. a sequent of the form |- B, would correspond to construction of a function f:LEM_0->A+ABS_0. If B is a tautology, it will actually be possible to construct a function f':LEM->B by "brute force" (i.e. case distinction over all possible inhabitants of LEM, which can be interpreted as a case distinction over all possible assignments of truth values to the atomic propositions). But this generally requires an exponential number of steps in the number of atomic propositions. Is there an efficient way to translate any PK proof |-A into a construction f:LEM_0->A? I found one way which works for all rules except cuts, but because cut elimination can introduce an exponential overhead, this is not enough.

[Ben Sherman]

Two references I can think of off-hand that you might be interested in:

- Michael Shulman’s blog post and associated paper on linear logic for constructive mathematics: https://golem.ph.utexas.edu/category/2018/05/linear_logic_for_constructive.html

Check out the “Chu construction”!

- A paper (of which I’m an author) on similar structures that arise in locale theory when one wants to consider Boolean-valued suplattice maps (see in particular section 5 and theorem 5.3, which gives an algebraic characterization of these structures as a quasi-Boolean algebra) https://dl.acm.org/citation.cfm?id=3209108.3209193. The operations you described have a natural symmetry in locale theory, even for quantification! 

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

[Michael Shulman]

As Ben says, this is essentially a Chu construction. The fact that a
Chu construction is *-autonomous and hence models *classical linear*
logic, rather than ordinary intuitionistic or classical logic,
probably accounts for much of the behavior you are seeing with
connectives. In particular, you may want to check out the
multiplicative conjunction "tensor" and multiplicative disjunction
"par"

A (x) B = (PA x PB, (PA -> NB) x (PB -> NA))
A (+) B = ((NA -> PB) x (NB -> PA), NA x NB)

which also play important roles in linear logics.

My paper that Ben mentioned uses the Chu construction with dualizing
object 0 (which in particular therefore has to exist), which amounts
in your notation to requiring PA x NA -> 0. But you can also use
dualizing object 1, which amounts to imposing no such requirement at
all, as you suggest; a reference for this approach is Anna Patterson's
1998 thesis "Implicit Programming and the Logic of Constructible
Duality", which shows that such a Chu construction models the
"constructible falsity" logic introduced by David Nelson in 1949.

By the way, you shouldn't neglect to consider the nullary connectives
"true" and "false" in your logic. In linear logic these also have
multiplicative and additive versions. The additive true and false in
any Chu construction are (1,0) and (0,1) respectively, which in
particular means that they don't exist if you don't assume that 0
exists to start with. With dualizing object 0, the multiplicative
nullary connectives are the same as the additive ones (so the logic is
"affine"); whereas with dualizing object 1, the multiplicative "true"
and "false' are *both* (1,1) (which one might argue makes for a
somewhat bizarre logic).

Finally:

On Wed, Aug 29, 2018 at 7:33 AM Sunrise Confusion
<hobbye...@gmail.com> wrote:
> If NOT A is translated to the function type A->0, as far as I understand the only way one could add the assumption that A is false would be by setting A:==0 itself (and then using 0-recursion to construct q:0->0).

This is not quite true, there is no problem with assuming an
inhabitant of A->0. However, it is true that the type A->0 is
(assuming function extensionality) always an h-proposition, and hence
has no interesting "internal structure". My paper about the Chu
construction applies it only to h-propositions, but Remark 9.13
suggests there is potentially some interest in applying to more
general types, so that as you say negations could be "interesting
objects with internal structure".

Best,
Mike

[Sunrise Confusion]

Thank you for your quick and detailed answers! The keyword "Chu
construction" and the references you give are apparently indeed
exactly what I need to connect to the literature. I need to read them
more carefully to understand better what they say. But at this point,
I haven't seen a reference so far about my observations/statements
regarding derivation of LEM/from absurdity of propositions, starting
with LEM/concluding absurdity of some atomic propositions. (But it's
very plausible that I just didn't understand that this was being done
somewhere by skimming up to now). I also haven't seen an explicit
reference to the classical sequent calculus I feel more comfortable
with, i.e. something that states "this can efficiently do everything
that LK can do, in this or that sense". This is probably implied by
some chain of reductions.

I also still wonder about the problem I formulated in the end of my
last message.

> By the way, you shouldn't neglect to consider the nullary connectives
> "true" and "false" in your logic.

What I wanted to do when translating proofs of nontrivial PK/LK
tautologies was just to simplify all expressions explicitly containing
true or false (by replacing A v true by true, A ^ true by A etc.)
until they aren't contained explicitly anymore, before translating to
type theory. Morally (and for the concrete thing I want to do), this
still seems to capture all the power of the logic to me, as any
nontrivial original statement (containing true or false) could be
re-derived efficiently from such an expression. In fact, the
definition of LK given in the Wikipedia article on sequent calculus
initially doesn't mention an absurdity symbol. Is there a theory in
which it is important to have explicit symbols for true or false?

That said (although I admit it can become a bit like a word game at
this point), if one wants objects behaving like true or false, one can
add an object of a type T as additional assumption, and another object
of another (unspecified) type F as possible conclusion. Then the tuple
(T,F) should behave like true, and (F,T) like false, and one still
didn't need to define the entire empty or unit type in the theory.

>> If NOT A is translated to the function type A->0, as far as I understand
>> the only way one could add the assumption that A is false would be by
>> setting A:==0 itself (and then using 0-recursion to construct q:0->0).
>
> This is not quite true, there is no problem with assuming an
> inhabitant of A->0.

I stand corrected. But what do you mean with remark 9.13? I didn't
find it in the arXiv version of "Linear logic for constructive
mathematics".

[Michael Shulman]

It's true that a "nontrivial" Boolean expression involving true and
false can be simplified to one not involving them, but don't be too
dismissive of triviality. There are situations in which it's hard to
do without "true" and "false". For instance, suppose you want to
define inequality of natural numbers by recursion:

(0 <= n) := true
(m+1 <= 0) := false
(m+1 <= n+1) := (m <= n)

You need something to slot in as the base cases.

On Wed, Aug 29, 2018 at 4:25 PM Sunrise Confusion
<hobbye...@gmail.com> wrote:

> I stand corrected. But what do you mean with remark 9.13? I didn't
> find it in the arXiv version of "Linear logic for constructive
> mathematics".

Sorry, it's remark 9.12.

[Ben Sherman]

On Aug 29, 2018, at 7:25 PM, Sunrise Confusion <hobbye...@gmail.com> wrote:

But at this point,
I haven't seen a reference so far about my observations/statements
regarding derivation of LEM/from absurdity of propositions, starting
with LEM/concluding absurdity of some atomic propositions. (But it's
very plausible that I just didn't understand that this was being done
somewhere by skimming up to now).

These observations are present, if densely stated, for the case of nondeterministic and/or partial Boolean values in locales in section 5 of our paper that I previously mentioned: Computable decision making on the reals and other spaces: via partiality and nondeterminism.

I’ll try to unpack it a bit here. The Booleans, as a topological space or locale, have two basic opens, which we can call ‘is_true’ and ‘is_false’. It suffices to define a Boolean-valued continuous map by defining the inverse images of these two basic opens. For instance, the Boolean and function, `and : bool * bool -> bool`, is defined as follows:

is_true(and(x, y)) = is_true(x) /\ is_true(y)

is_false(and(x, y)) = is_false(x) \/ is_false(y)

This “style” of defining continuous maps of locales is explained by Steve Vickers in, e.g., Locales and Toposes as Spaces. One must verify that this definition of ‘and’ indeed gives a continuous map. This includes that the inverse image of the entire output space must be the entire input space, i.e., and^*(\top) = \top. Said otherwise, ‘and’ preserves totality.  To say that a point of bool lies in the entire space means that either is_true or is_false holds of it, which is equivalent to your LEM.  Because a point within the space bool^n lies in the entire space if and only each component point of bool does, this means that just by virtue of being a continuous map, ‘and’ preserves LEM. 

There is something similar for ABS. By virtue of ‘and’ being continuous, its inverse image preserves binary meets (intersections of opens), so in particular

and^*(is_true /\ is_false) = and^*(is_true) /\ and^*(is_false)

. This says that ‘and’ preserves determinism: when ‘and’ is lifted to apply to potentially nondeterministic Boolean values, the output will be deterministic if all the inputs are. The connection here is that your definition of non-absurdity of propositions is connected to the notion of determinism here. We know of the Booleans that

is_true /\ is_false <= \bot

and since and^* is a frame homomorphism, we get

and^*(is_true) /\ and^*(is_false) <= \bot

This implies that, because ‘and’ preserves determinism, it also preserves non-absurdity.

These facts about the Boolean ‘and’ function, that it preserves totality (LEM) and determinism (non-ABS), follow entirely from the fact that it is a continuous map from bool^n to bool (for n = 2). They hold for any continuous maps of theses sorts, including Boolean or, Boolean negation, and (somewhat degenerately for) the constants true and false.

In section 5.1.1, there is a short explanation of the fact that the universal quantification functional (over a compact-overt space) preserves both totality (covering) as well as determinism (disjointness), and that symmetrically holds for the existential quantification functional.

Note that in the world of compact-overt locales, we indeed get the quantification law

forall_K(P \/ Q) <= forall_K(P) \/ exists_K(Q)

(see section 5.1.1 of our paper, which cites Vickers’ Constructive Points of Powerlocales) and so we indeed do get the symmetry that you are asking for, in contrast to the type-theoretic formulation that you presented, where the above law may not hold.

I’m happy to explain any of this in further detail if you’re interested.

[Sunrise Confusion]

Thank you for your answers and explanations so far. I wanted to post this a lot earlier, but life got in the way. I think I should study category theory more thoroughly before it makes sense for me to read Ben’s paper.

But I think I can now answer the question I posed at the end of my first message affirmatively: I want to present a way to translate a deduction into a construction f:LEM->A, with polynomial overhead.

The idea is to construct the desired function f:LEM->A “in stages”, where in each stage k, we are allowed to assume that at least k atomic propositions are true. If applying f yields an inhabitant of (the to-be-defined analogue of) ABS, rather than an inhabitant of A, we will be allowed to assume that one more PA_i is inhabited. For n input variables, we will be certain to obtain an inhabitant of A after going through n+1 stages.

Now a more precise sketch: Suppose we are given a PK proof concerning n atomic propositions PA_1,...,PA_n. We define:

1. types LEM_{i,j} for 1<=i<=n, j<=i, which express the law of excluded middle on i atomic propositions, together with the assertion that at least j propositions are true. They are defined in a natural way:
1. LEM_{i,0} is the usual LEM on i propositions,
2. LEM_{i,i}:==PA_1 x ... x PA_i,
3. for i>j>0, LEM_{i,k}:=LEM_{i-1,j} x NA_i + LEM_{i-1,j-1} x PA_i.

2. types NA’_{i,j,k}:==NA_j x (PA_j->LEM_{i,k+1}) for all i<=n,j<=i,1<=k<=i, and

3. LEM’_{i,j}, ABS’_{i,j} and A’_j by replacing all NA_k by NA’_{i,j,k}. Intuitively, these types combine a negation-as-in-BHK with a negation-as-Chu.

It turns out that we can construct s_{n,j}:LEM_{n,j}->LEM’_{n,j}. This is the goal of the next two paragraphs.

We construct q_{i,j,k}:LEM_{i,j}->PA_k+(PA_k->LEM_{i,j+1}) whenever the types are well-defined in an inductive way, following the inductive definition of LEM_{i,j}:

• q_{i,0,k} is defined by a simple case distinction,
• q_{i,i,k} is defined by projecting and embedding the appropriate PA_k,
• the case i>j>0 is split into the two subcases k=i and k<i, both of which can be treated by case distinctions and q_{i’,j’,k’} constructed at earlier stages of the induction. In total, this takes a polynomial number of steps.

Together with the inhabitants lem_i:PA_i+NA_i that we get from l:LEM, we construct r_{n,j,k}:LEM_{n,j}->PA_j+NA’_{n,j,k}. From these, we get s_{n,j}:LEM_{n,j}->LEM’_{n,j} as desired.

For j<n, we can also construct t_{n,j}:ABS’_{n,j}->LEM_{n,j+1}. The reason is that, by a case distinction over ABS’_{n,j}, we can always assume to be given a tuple of the form (f,g), where f:PA_k, and g: PA_k->LEM_{n,j+1}. Then g(f) is of the desired type.

From the projection operators pr_1:NA’_{n,j,k}->NA_j, we can build a projection prA_j:A’_j->A_j.

Next, we use the construction of f from the first message (e.g. defining f as a dependent function over the types NA_j:U, and then plugging in NA’_{n,j,k} for each NA_j) to get f_j:LEM’_{n,j}->A’_{n,j}+LEM’_{n,j+1} for j<n using a polynomial number of steps.

Next, we put together the f_j, s_{n,j}, prA_j, t_{n,j} to obtain f’_j:LEM_{n,j}->A+LEM_{n,j+1} for 0<=j<n. For j=n, f’_n:LEM_{n,n}->A can be constructed efficiently as well: By projections from l:LEM_{n,n}, we obtain inhabitants of PA_k for all possible k, and can construct an element of A from these.

Nesting the f’_j obtained, we obtain a function f:LEM_{n,0}->A. Because LEM_{n,0}==LEM_0, this is the function we wanted to construct.