If Type Theories are all Logics.

Question

So it sounds like Higher Order Logic (HOL) and Type Theory are equivalent. Then there is Intuitionistic Logic and Intuitionistic Type Theory, but I'm not sure of the connection there.

I am just wondering what the difference is between a Logic and a Type Theory at this point. I always thought of Types from the programming perspective, where it allows you to define the structure of data (and proofs about the data), whereas a Logic was more about formal reasoning. But if the progression goes from $propositional \to first\ order \to second\ order \to \dots \to higher\ order$, and HOL is Type Theory, then Type Theory can be used for formal reasoning, which I guess makes sense why it is considered as a Foundation of Mathematics. But Type Theory is often contrasted with Set Theory. I haven't seen Set Theory contrasted with Logic or HOL. So makes me wonder what the connection is between Logic and Set Theory.

So to summarize, wondering:

1. What the difference is between a Logic and a Type Theory.
2. When a Logic becomes a Type Theory.
3. If all Type Theories can be considered Logics.

Answer 1

The answer to your question comes in three parts.

Part one, I think you're mixing up two slightly different uses of 'Type Theory'.

I am guessing Type Theory, as you are used to it, is the field of study where we make type theories, which are formal systems where we add types to terms such that we can combine them together in sensible ways, such that we avoid paradoxes and other nasty things.

The 'Type Theory' that is equivalent to HOL, is more properly called 'Simple Type Theory', which is a kind of type theory (I apologise for the confusing sentence). In essence, 'Simple Type Theory' is just a formal system of terms and types, and is just another name for Higher Order Logic.

Also, I have to be careful here, because Higher Order Logic also has two meanings. The first sense is as a kind of logic. First order logic can quantify over objects from the domain of discourse (the set of all things we want to talk about). For example $\forall x. \forall y. x = y$ is the statement in first order logic that everything in the domain of discourse is equal.

Second order logic can quantify over the set things can be in, third order logic can quantify over the set of sets things can be in, and so on. Higher order logic is then a logic that can quantify over everything $n$-order logic can, for all $n$. Simple Type Theory is just a (but not the only) higher-order logic.

The fact that 'higher order logic' is synonymous with simple type theory came about because, as best I can tell, the HOL proof assistant used a slight extension of the Simple Type Theory as their type theory/logic, and the name stuck.

Part two, on logic and type theory.

The difference between type theory and logic can be somewhat convoluted (I even confused myself in an earlier revision of this answer). This is mainly due to how intertwined they are.

Type theory came about, in part, because of fundamental problems with logic discovered in the early 1900s by Russell and his peers. Summarising Russell's basic idea, the problems he was having was due to self reference, so he added types to proofs such that every proof term lived in a type, and constructed it in a way such that they weren't self-referential.

Part three, the Curry-Howard correspondence.

Type Theory, Logic, and Computation are linked in a rather fundamental way in what is called the Curry-Howard correspondence, which you mentioned. This says that every type theory can be interpreted both as a logic, and also as a computation.

The quintessential example of this is the correspondence between the simply typed lambda calculus and intuitionistic logic.

To explain the notation I'm about to use, think of $\Gamma$ as a multiset which contains assumptions/in-scope variables. $\Gamma, x : A$ is an abbreviation for $\Gamma \cup \{x : A\}$.

$x : A$ means term $x$ has type $A$, and $\Gamma \vdash x : A$ means that 'under the assumptions $\Gamma$, $x$ has type $A$'.

Finally, $\dfrac{J_1 \quad\; J_2 \quad \dots \quad J_n}{J}$ is called an inference rule, and it says, if we have all the things on the top ($J_1,J_2,\dots,J_n$) we can deduce the bottom ($J$).

Here is a fragment of the simply typed lambda calculus:

The first rule is about assumptions, and it says that, if $x : A$ is in our assumptions, then under $\Gamma$, $x$ has type $A$. $$ \dfrac{x : A \in \Gamma}{\Gamma \vdash x : A}\text{assume} $$

Rules for lambda terms. Here we have 'abstract', which says if we have an assumption in $\Gamma$, and a construction of a typing $y : A$ we can construct a function from things of type $A$ to things of type $B$. 'apply' says that, if we have a function from $A$s to $B$s, and an $A$, we can get a $B$. $$ \dfrac{\Gamma, x : A \vdash y : B}{\Gamma \vdash \lambda x. y : A \to B} \text{abstract} \qquad \dfrac{\Gamma \vdash m : A \to B \quad\; \Gamma \vdash n : A}{\Gamma \vdash m \, n : B}\text{apply} $$

Rules for product. These talk about how to construct and destruct 2-tuples. $$ \dfrac{\Gamma \vdash x : A \quad\; \Gamma \vdash y : B}{\Gamma \vdash \langle x, y \rangle : A \times B} \qquad \dfrac{\Gamma \vdash z : A \times B}{\Gamma \vdash \mathbf{fst}\; z : A} \qquad \dfrac{\Gamma \vdash z : A \times B}{\Gamma \vdash \mathbf{snd}\; z : B} $$

Now, if you ignore everything to the left of the $:$ (that is, ignoring the terms), you get intuitionistic logic (well, specifically, the fragment with only implication and conjunction, but there are analogous constructs for disjunction, truth, and falsity).

If you ignore everything to the right of the $:$ you have the lambda calculus, which is a method of computation.

For more, see Philip Wadler's talk Propositions as Types.

Answer 2

"Type theories" are particular kinds of formal theories. Set theories are also particular kinds of formal theories.

There are really two very different kinds of "theories with types":

• In systems such as higher order logic, the types are part of the syntax of the theory, but the theory itself is not aware of the types. In other words, the types are used to control which expressions are well formed in the theory, but the theory itself does not have a way to refer to types. These could be described as "theories with types".

• In systems such as intuitionistic type theory, the theory itself has axiom referring to types. For example, the theory may have an axiom that if $A$ and $B$ are types then there is a product type $A \times B$, and the elements of this type looks like pairs $(x,y)$ where $x$ has type $A$ and $y$ has type $B$. These theories could be described as "theories about types".

There is a large difference in practice between these two kinds of theories. In higher-order logic, we use the usual logical apparatus of conjunction, disjunction, quantifiers, etc. In intuitionistic type theory, following the idea of propositions as types, we don't look at the logical operators, but instead look at operators on types within the type theory instead.

For example, in higher order logic, if we have two sentences $\alpha$ and $\beta$ we often form their conjunction $\alpha \land \beta$. In intuitionistic type theory, if we have two types $A$ and $B$ (which we might think of as propositions), we take the conjunction by looking at the product type $A \times B$ within the type theory. This is often referred to as the "internal logic" of the type theory; in intuitionistic type theory it is much less common to look at the actual logical operators $\land$, $\lor$, etc. than to look at the type-constructing operations. Even quantifiers are replaced with type constructions. To accomplish this, the syntax of intuitionistic type theory is also quite different from the syntax of higher-order logic.

The post has a somewhat anachronistic flavor in asking about "a logic" - that kind of terminology is not used very much in contemporary mathematical logic, where we have no very standard definition of "a logic". So the final three questions are hard to answer from this contemporary perspective. Instead, I would say that intuitionistic type theory is one kind of formal theory, while theories in higher order logic are another kind of formal theory.