# Logic vs. type system

What's the difference between logic (in a narrow sense, i.e. a logical system such as ZOL, FOL, etc.) and type system?

I will sketch my understanding of this -- please correct if I err. Under propositions-as-types, they coincide. In propositions-as-some-types, a logic(al system) is a proper subset of the type system. In logic-enriched type theory (LTT), they are distinct components. "Untyped" always means "single-typed" (as in untyped $λ$-calculus, which has only functions), and describes the object level of the formalism (i.e. its objects belong to a single type); together with its meta level there are more types (e.g. the syntactic operators $λ$, . in $λ$-calculus). I'll finish with some examples of the possible combinations:

typed logic : FOL
typed nonlogic : a data type system
untyped logic : untyped lambda-calculus*
untyped nonlogic : a teapot

* not a logic but can encode one

A set-theoretic foundational system is usually based on two main pillars:

1. The deductive system of the theory, usually first-order classical logic;
2. The body of axioms of the theory, such as $$\mathsf{ZFC}$$.

The type-theoretic approach is different from that of set-theory. Instead of sets, we place functions as the first class mathematical objects. Also, types get their meaning from the way we use them, having their corresponding formation, construction, elimination, computation (and possibly uniqueness) rules for each type.

The propositions-as-types correspondence states that it is possible to interpret logic within a type theory, by viewing the statement that we want to prove, typically a judgment of the form "proposition $$A$$ is true",

$$A \; \mathsf{true},$$

as the claim that the type that this proposition corresponds is inhabited,

$$\frac{a : A}{\mathsf{true}}.$$

There are interesting philosophical aspects to this interpretation (see e.g. Martin-Löf (1996)). But my main point here is that a type-theoretic foundation comprises both components of the set-theoretic approach mentioned above, as we can regard types as sets and propositions.

Some examples are shown on the following table (for more see the Homotopy Type Theory Book):

$$\begin{array} {|c|} \hline \textsf{Types} & \textsf{Logic} & \textsf{Sets} \\ \hline A & \text{proposition} & \text{set} \\ \hline a:A & a\text{ is a proof of }A & a\text{ is an element of }A \\ \hline A\rightarrow B & A \text{ implies } B & \text{set of functions from }A \text{ to }B\ \\ \hline A\times B & A \text{ and } B & \text{cartesian product of }A \text{ and }B\ \\ \hline \end{array}$$

• Honestly the identification between $A \times B$ and $A \wedge B$ has never truly made sense to me. If $A$ is a set, then $A \times A$ won't, in general be isomorphic to $A$. But if $A$ is a truthvalue, then $A$ and $A \wedge A$ are always equal. – goblin Jun 22 '15 at 8:53
• @goblin That is only true if $A$ is what homotopy type theorists call a "mere proposition". Such a type has the property that all inhabitants are equal (but note there may be no inhabitants). If a set contains 0 or 1 elements, then we do have $A \times A \cong A$. However, if we have a type with multiple inhabitants, then they are not isomorphic, just as in the set case. – John Colanduoni Jun 22 '15 at 9:36
• @JohnColanduoni, yes, that's obvious. Nonetheless, still it makes no sense to me. Since $A \wedge A = A$, hence the space of proofs of $A \wedge A$ must equal the space of proofs of $A$. Write $[A]$ for the space of proofs of $A$. From $A \wedge A = A$, deduce $[A \wedge A] \cong [A]$, and hence $$(*)\qquad [A] \times [A] \cong [A].$$ Huh, what? If $A$ has $3$ proofs, then $(*)$ appears to be saying that $A$ has $9$ proofs. Well, which is it? Is it $3$, or $9$? – goblin Jun 22 '15 at 10:12
• @goblin Thats the whole point. Such an $A$ is not a mere proposition. $A \times A = A$ only holds if $A$ has no more than one proof. Otherwise they won't be equal, because there will not be a bijection between them. – John Colanduoni Jun 22 '15 at 10:14
• @goblin You are confusing $(A \wedge A \to A) \wedge (A \to A \wedge A)$ with $A \wedge A = A$. The former is of course always true; but it does not imply the later. For $A \wedge A = A$ we need a bijection, which clearly does not exist if $A$ has more than one inhabitant. In essence, the classical iff is not the same as equality in type theory. – John Colanduoni Jun 22 '15 at 10:20

In my understanding formal logic-systems (like FOL, propositional logic, etc) and type theories (or type systems) are all families of derivation systems: i.e. systems having an underlying set of formulas (usually described by a formal grammar) and inference rules defined on these formulas (which can be thought as operation for generating tree of formulas, the proofs).

These kind of formal systems differ in their presentations (the grammar for their languages and, consequently, their inference rules) but they are isomorphic (as derivation systems) as Curry-Howard isomorphism shows: this means that there is a way of mapping formulas and proofs from one system in formulas and proofs of the other one, in such a way that if $p$ is a proof of $F$ from the hypothesis $H_1,\dots,H_n$ the its image $[p]$ is a proof of the image formula $[F]$, image of $F$, from the hypothesis $[H_1],\dots,[H_n]$, images respectively of $H_1,\dots,H_n$.