11
$\begingroup$

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?
$\endgroup$
5
  • 1
    $\begingroup$ "STLC". Sorry, I'm drawing a blank. What is this? The question is hard for me to understand because I don't know what co-IL is supposed to mean beyond formally dualizing IL. $\endgroup$
    – Todd Trimble
    Sep 23, 2017 at 0:08
  • 2
    $\begingroup$ STLC = simply typed lambda calculus. I linked to a page which has several papers on the proof theoretic semantics of the result of the formal dualization: in that case it provides a calculus of refutation, i.e. "proofs" of denials rather than assertions. I believe there are other semantics out there including topological semantics. What I'm looking for is a corresponding simple type theory for the prop case and what the result would be when extending it and what that TT might be. I'm thinking it's not just something with "co-exponential" objects and reversed 'eval' but I dont know $\endgroup$
    – Anthony
    Sep 23, 2017 at 0:28
  • $\begingroup$ Well, it's not true that an arbitrary ccc models simply typed lambda calculus, since simply-typed means just one (non-terminal) object. Maybe you should say "typed lambda calculus" instead. A topological semantics for propositional co-IL would be the co-Heyting algebra of closed sets of a topological space. $\endgroup$
    – Todd Trimble
    Sep 23, 2017 at 0:48
  • 6
    $\begingroup$ @ToddTrimble actually, "simply typed" allows many types/objects; the meaning of "simple" is in contrast to "dependent". The single type/object case is called "untyped" or "unityped". $\endgroup$ Sep 23, 2017 at 5:09
  • $\begingroup$ @MikeShulman Oops. Thanks for the reminder. $\endgroup$
    – Todd Trimble
    Sep 23, 2017 at 9:52

2 Answers 2

2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks for the update :) Where were you reading about this? $\endgroup$
    – Anthony
    Aug 26, 2021 at 12:29
  • $\begingroup$ I mostly browsed nlab. I think it's related to Stone Duality for the case of finite sets? You mostly find resources talking about Stonean Duality and not the specific case of Set. It's also somehow related to forcing in ways I don't understand $\endgroup$ Aug 26, 2021 at 20:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.