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?
  • $\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 '17 at 0:08
  • 1
    $\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 '17 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 '17 at 0:48
  • 2
    $\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$ – Mike Shulman Sep 23 '17 at 5:09
  • $\begingroup$ @MikeShulman Oops. Thanks for the reminder. $\endgroup$ – Todd Trimble Sep 23 '17 at 9:52

Your Answer

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

Browse other questions tagged or ask your own question.