# Logic within Type theory. Is there a rough academic consensus on how this should be done?

I guess because of it's presence in several blogs on math and even physics, I've recently started to learn some type theory, often from people who know about it and from books which use it. I want to write down some personal notes, specifically about how mathematics is done in it, but I kind of have a problem in that there seem to be dozens of ways to implement logic in it and I don't even see which one is more canon than the other. "My work" so far consisting in collecting the ideas which I have encounter.

A rule like

$$\frac{\Gamma\vdash a:P\hspace{1cm}\Gamma\vdash f:P\to Q}{\Gamma\vdash f(a):Q}$$

is essentially using the "if-then" idea three times at once. The vertical axis $\frac{foo}{bar}$ is used as for natural deduction, the $\vdash$ being substituted by implications $\implies$. Other times we seem to do proof theory with the object language being written horizontally. The context $\Gamma$ is sometimes a series of typing judgements separated by commas $\Gamma=(a:A,b:B,c:C)$, but in a strengthened system we can have them be a type itself, $\Gamma=(a,b,c):A\times B\times C$. Turnstile denote derivability and $foo\vdash bar$ are classical sequents. Here I wonder if we really need to draw two dimensional and if not, then is the vertical axis the in-build meta-logic? When we write $\frac{A\ \ \ B}{C}$, the empty space between $A$ and $B$ must be a formalized "and". Curious then, that people were so motivated to work out the seemingly difficult task of giving semantics to product-types-lacking formal systems. Then people do untyped calculi in type theory, which is the same as collapsing one type. The logical propositions becomes the terms. Or we use the Curry Howard correspondence. Terms are proofs then, types are propositions. Hence function type $\to$ are implications $\implies$. When it comes to its categorical semantics, things get really out of hand. The first thing I read, in a depended type context, was that categories are the basic types and functors are implications in the logical interpretation. But then objects are the types and I figured these are objects with elements (like set) as types have terms. But the terms (or proofs, in the logical interpretation) are only contained in the objects in a sneaky way, because the objects are mostly the context. The morphisms are the turnstiles. But sometimes they are computer programs, i.e. proofs, i.e. the implications from a proposition (=type (=object)) to another. In fact, the are equivalence classes of computations w.r.t $\beta\eta$-conversion. But if you have 2-categories, then the 2-morphisms are the conversion. The last bit sounds reasonable to me.

In any case, what is the most natural way to use type theory to capture propositional logic, so that I don't have to rewrite my notes completely once I pass to predicate logic? (=depended types (=fibered categories?)). My motivations are a clear presentation of math, not really proof theory and not a huge emphasis on computation.

-
it looks like typed sequent Calculus. For (normal) sequent calculus see en.wikipedia.org/wiki/Sequent_calculus, hope this helps – Willemien Dec 28 '13 at 23:34
Good question. By the way, I think that $\frac{A}{B}$ should be viewed as saying: if $A$ is written down, we may write down $B$, as opposed to saying "if $A$, then $B$." Its a rule, not a claim. – goblin Jan 15 '14 at 22:05
@user18921: Yes, I agree. I view the vertical axis the way you say it, the arrow $\implies$ as object language implication and turnstyle $\vdash$ as more formalized or meta implication. I'm tempted to go with the flow and learn concepts as presented in these lecture notes. I've also previously asked a related question on the ComputerScience board here. – NikolajK Jan 15 '14 at 22:19
@user18921: I'm actually a physicist and one of my motivation for types comes the work of Urs Schreiber, which I try to understand. That's probably a rather exotic angle, see my interest here. – NikolajK Jan 15 '14 at 22:20
Thanks, those notes look interesting. To be honest, I didn't really understand the physics question. – goblin Jan 15 '14 at 22:28

The main orgainizing principle in Jacobs framework is to arrange expresions of the languages into levels like terms, propositions, types and kinds and then look at what kinds of dependecies can exist between expressions from different levels. More specifically level $L_2$ depends on level $L_1$ (written $L_2 \succ L_1$) if you can derive sequents $\Gamma \vdash A:L_1$ and $\Gamma, x:A \vdash B[x]:L_2$. For example propositional logic and equivalently simply typed lambda calculus has only one level called $Type$ and no dependencies. Martin-Lof type theory also has only one level but with the reflexive dependency $Type \succ Type$. Higher order calculi generally have at least a second level usually called $Kind$ with $Type \succ Kind$ and the axiom $\vdash Type : Kind$. Given a sequent calculus presentation of a logic this framework lets you determine the levels and dependencies and lays out the broad structure of the categorical sematics based on these. It also shows how to model the semantics of sum product and exponent types within and across the levels.