What does first-order co-intuitionistic logic look like (and does it have an equivalent type theory)?

Question

So, this is where I'm at so far:

1. Heyting algebras model propositional intuitionistic logic (IL)
2. so do Cartesian closed categories which also model the simply typed lamda calculus
3. co-Heyting algebras model propositional co-intuitionistic logic (co-IL) and ??
4. Locally Cartesian closed categories model dependent type theory (TT)
5. Locally (and not) co-Cartesion co-closed categories model ?what exactly?

I became interested in co-Heyting algebras because of mereology for linguistics but then I learned that they model co-IL. I found a proof theory using a single-assumption multiple-conclusion natural deduction that works well as a refutation calculus dual to IL. This led me to a few questions which I can't find much research on (and I don't know much category theory.)

1. Are there any term assignments for co-IL? What exactly would be "the construction c [that] refutes A −< B iff c [which]is a general method of construction such that applied to a hypothetical construction a that refutes A, c(a) refutes B"?
2. Can one generalize to first-order quantifiers and if so, what do they look like? Would it be the coproduct that takes on some more computational meaning rather than how product does in TT?

Answer 1

Hey I'm not really a mathematician but I struggled with this myself.

There are more than a few ways to do this but I don't think there's really any standard notation.

Interpret typed lambda calculus backwards

The typed lambda calculus can be mapped to cartesian closed categories. We can also map it to the opposite of co cartesian closed categories.

Instead of the (negative) rules for tuples.

$$ \frac{\Gamma \vdash x : A , \Gamma \vdash y : B}{\Gamma \vdash \langle x , y \rangle : A \times B} $$

$$ \frac{\Gamma \vdash x : A \times B}{\Gamma \vdash \pi_1 x: A} $$

We have the rules for sums:

$$ \frac{\Gamma \vdash x : A , \Gamma \vdash y : B}{\Gamma \vdash [ x ; y ] : A + B} $$

However, we have to interpret the environment as a sum of variables instead of a product of variables.

If we have two patterns/case statements/contravariant functors we can sum them together.

$$ \frac{\Gamma \vdash x : A + B}{\Gamma \vdash \mathbb{left} \,x: A} $$

If we have a pattern match patterns/case statements/contravariant functor matching a sum type we can contravariantly make it more specific.

In a similar manner coexponential types are dual to exponential types.

$$ \frac{ \Gamma , x : A \vdash e : B}{\Gamma \vdash \, \mathbb{adbmal} \, x : A . e : B - A } $$

$$ \frac{ \Gamma \vdash f : B - A , \Gamma \vdash x : A}{\Gamma \vdash \, f x : B } $$

Interpreting everything backwards works but it's just really really confusing.

Directly work with the categorical point-free combinators

Just have the usual sum types and

$$ \mathbb{councurry} : \mathbb{Hom}(A - C, B) \rightarrow \mathbb{Hom}(C, A + B) $$ $$ \mathbb{cocurry} : \mathbb{Hom}(C, A + B) \rightarrow \mathbb{Hom}(A - C, B) $$

This is kind of nice sometimes but really I miss variables.

Reverse the categorical kappa/zeta decomposition

I wanted a nicely categorical language but with also nice variables so I found Decomposing typed lambda calculus into a couple of categorical programming languages In Proc. 6th International Conference on Category Theory and Computer Science (CTCS'95), Springer LNCS 953 (1995) 200-219

Pretty directly you get a sort of continuation passing style

Reversing (the positive tuple rules)

$$ \frac{\Gamma , x : 1 \rightarrow A \vdash e : B \rightarrow C }{\Gamma \vdash \kappa \, x : 1 \rightarrow A . e : A \times B \rightarrow C } $$

to

$$ \frac{\Gamma , x : A \rightarrow 0 \vdash e : C \rightarrow B }{\Gamma \vdash \mathbb{cokappa} \, x : A \rightarrow 0 . e : C \rightarrow A + B } $$

$$ \frac{\Gamma \vdash x : A \rightarrow 0}{\Gamma \vdash \mathbb{colift} \, x : A + B \rightarrow B } $$

You can kinda interpret this as like a case statement. It's still pretty confusing though.

Coexponentials become something like

$$ \frac{\Gamma , x : A \rightarrow 0 \vdash e : C \rightarrow B }{\Gamma \vdash \mathbb{cozeta} \, x : A \rightarrow 0 . e : A - C \rightarrow B } $$

$$ \frac{\Gamma \vdash x : A \rightarrow 0}{\Gamma \vdash \mathbb{copass} \, x : B \rightarrow B - A } $$

It's maybe a little clearer but still pretty awful.

Summary

Just do intuitionistic logic but in reverse.

Yeah I don't really have any better ideas. Currently I'm trying to figure out the positive polarity presentation of functions. My guess is that finding dual of the positive presentation might be cleaner. I'm also still looking at the dependently typed setting. I'm going to try to reverse the calculus of constructions after I look at it enough.

Answer 2

There's also an entirely different approach I still don't understand.

I wanted to figure out how to do it before giving an answer but I'm still really far away from grasping it.

Categorically there is a well known equivalence via the powerset functor between $\text{Set}^{\text{op}}$ and the category of complete atomic boolean algebras.

I don't really understand it but if you make a language for working with CABAS you should be someway towards a language for working with $\text{Set}^{\text{op}}$. It's not strictly equivalent but it's an interesting angle to look at. You can maybe think of this in terms of nondeterminism or relational programming.

Also the constructive variation of CABAs is complicated.

The problem with a straightforward interpretation of the internal language of CABAs is that then every "set" is inhabited by $\top$ because everything is a CABA and every category has a $\top$ and $\bot$.

But anyway it's still all weird and I just don't get it. Sorry this math is beyond me but I wanted to inform you about CABAs.