1
$\begingroup$

It is well-known that the types in a given programming language form a category, based on Set, with their functions as morphisms.

It is also well-known that any program is basically a proof in constructive logic - the result is called in Curry–Howard correspondence and it is used in theorem prover software like Coq and Agda.

Doesn't, then, constructive logic form a category, in its own right? The objects are logical assertions, the morphisms are implications and True and False are, as in Coq, the initial and terminal object? And if yes, why isn't that category defined anywhere?

I am asking this is because it seems weird to me that many people talk about the connection between logic and Category theory, but as far as I know no one formalizes it.

$\endgroup$
  • 1
    $\begingroup$ Yes, you can do that if you want. Do you have any application in mind? Are you just asking for he name of this "missing" category (which I don't know)? $\endgroup$ – realdonaldtrump Nov 9 '17 at 7:55
  • 1
    $\begingroup$ My implicit question is "why isn't that category defined anywhere?" $\endgroup$ – Bobby Marinoff Nov 9 '17 at 8:19
  • $\begingroup$ I think that it will serve as a great example of a "categorization" of a well-known concept (I think that the main issue with teaching CT is that there are too few examples). $\endgroup$ – Bobby Marinoff Nov 9 '17 at 8:21
  • 2
    $\begingroup$ Regarding the first sentence: math.andrej.com/2016/08/06/hask-is-not-a-category $\endgroup$ – Dap Nov 9 '17 at 9:06
  • $\begingroup$ OK, I know that Haskell is not a real category, due to the existence of bottom values, but I think that a subset of Haskell is a category. Am I wrong? And is this why logic also can't be thought as a category? $\endgroup$ – Bobby Marinoff Nov 9 '17 at 10:06
4
$\begingroup$

It sounds like you're looking for the "term model" or syntactic category of a type theory. This is defined in Sketches of an Elephant: A Topos Theory Compendium D1.4.

This will in general distinguish between proofs - otherwise you just get a poset called the Lindenbaum–Tarski algebra. This is a Heyting algebra if your theory obeys the axioms of intuitionistic logic.

$\endgroup$
  • $\begingroup$ So my category would be called, something like Con(Intui) in which an object would be a set of assertions, for example (A -> B, A) and a morphism would convert one set of assertions to another, like (A -> B, A) -> (A). Right? $\endgroup$ – Bobby Marinoff Nov 10 '17 at 8:46
  • $\begingroup$ After reading your second sentence, indeed using category theory for that would be overkill, since in logic we are not interested in the multiple ways in which one set of assertions follows from another. $\endgroup$ – Bobby Marinoff Nov 10 '17 at 8:52
  • 1
    $\begingroup$ @BobbyMarinoff "...in logic, we are not interested in the multiple ways in which one set of assertions follows from another..." This is a bold assertion! There is a whole branch of logic that actually cares for this. Martin-Löf type theory and Homotopy of type theory wouldn't even exist otherwise. $\endgroup$ – Pece Nov 13 '17 at 12:14
  • $\begingroup$ Thanks for the comment. I mostly think of these comments as questions, although I didn't formulate them as such. $\endgroup$ – Bobby Marinoff Nov 13 '17 at 18:24

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.