7
$\begingroup$

While type theory certainly has traditionally been used for different purposes than model theory, as noted in this Philosophy SE post, I wonder to what extent type theory could model model theory itself.

My motivation for this question is based on an observation that we can view the typing relation in type theory as analagous to the "is a model of" relation in model theory. For example, one might regard the Sigma type $Magma(A) :\equiv\Sigma_{a:A} A \rightarrow A \rightarrow A$ as the theory of magmas over a type A, and components of said type models of the theory.

Now certainly, model theory has more structure to it than a simple "x is a model of y" relation between theories and models of those theories, but I think the idea of interpreting types and terms as a theory/model relation begs the question: Can we develop a richer language in type theory to deal with this types as theories, terms as models interpretation in order to interpret traditional (i.e. ZFC-based) model theory within a type theoretic framework? And, if full interpretation with classical model theory is not possible, is there still some meaningful type-based model theory that we could develop?

$\endgroup$
6
  • $\begingroup$ The theory of magmas is not really interesting, since it has no axioms! Can you describe how you would handle theories with axioms? (Even so, I'm not sure I understand your example. Isn't $\Pi_{a:A}A$ normally just a way to write $A\to A$? Why are you using both that and $\to$ in your expression?) $\endgroup$
    – hmakholm left over Monica
    Commented Mar 14, 2016 at 16:52
  • 1
    $\begingroup$ Not quite. Pi types are more general than function types. But I believe I actually should have used a sigma type in this instance, so I will edit my post. You can basically read $\Pi$ as $\forall$, and $\Sigma$ as $\exists$. One could express the theory of semigroups as: $Semigroup(A) :\equiv \Sigma_{m:A \rightarrow A \rightarrow A}\Pi_{a,b,c:A}Id(m(a,m(b,c)),(m(m(a,b),c))$ Where $Id$ is the identity type of proofs that two terms are equal, for a more interesting example. Similarly, you could describe the theory of groups, or rings. $\endgroup$
    – Nathan BeDell
    Commented Mar 14, 2016 at 17:08
  • 1
    $\begingroup$ x @Sintrastes: My understanding (but it's a long time since I worked with dependent types) is that $\Pi$ reduces to a function arrow when the bound variable isn't free in the body, as in $\Pi_{a:A} A$ -- and similarly $\Sigma_{a:A}A$ would be the same as $A\times A$. $\endgroup$
    – hmakholm left over Monica
    Commented Mar 14, 2016 at 17:15
  • 3
    $\begingroup$ I think you are asking whether, rather than studying model theory using set theory, you could study model theory using type theory as your metatheory. Sure, you could do that. $\endgroup$
    – Carl Mummert
    Commented Mar 14, 2016 at 17:16
  • 2
    $\begingroup$ @Carl Mummert Could you elaborate? I assume the question is implicitly, "would you get some interesting insight or a different view of model theory in doing so?". $\endgroup$
    – Graffitics
    Commented Mar 15, 2016 at 9:47

1 Answer 1

Reset to default
3
$\begingroup$

Denoting $\mathcal{U}$ as a type universe, one usualy one writes $\mathsf{MagmaStr} : \mathcal{U} \to \mathcal{U}$ for the magma structure over some type. As allready noted the magma structure of $A$ is just a map $A \times A \to A$ so it should be $\mathsf{MagmaStr}(A) = A \times A \to A$.

For a type theoretical definition of $\mathsf{Magma} : \mathcal{U_1}$ itself I would write $\mathsf{Magma} = \sum_{A : \mathcal{U}} A \times A \to A$ note that this type, the magmas in a the universe $\mathcal{U}$, lives in a higher universe level. Then a member of $\mathsf{Magma}$ is a pair of of a type $A$ and a binary operator on $A$ living in $\mathcal{U}$. In that way the type $\mathsf{Magma}$ can be seen as a theory and the members of this type as its models.

Ofcourse the $\mathsf{Magma}$ answer is somewhat simplistic but the above readily generalizes to for example a $\mathsf{SemiGroup} = \sum_{G : \mathcal{U}} \sum_{* : G \times G \to G} \prod_{a b c : M} (a * b) * c = a * (b * c)$. Which is a bit more involved as you can see.

It think that within this framework a lot model theory can be done, at least if the type theory is rich enough.

$\endgroup$
1
  • $\begingroup$ Thank you. I think I can add to this now, that while I have yet to see any literature on type theory being used as an explicit alternative to model theory, the field of categorical semantics is essentially a categorical alternative to classical (set theoretic) model theory -- and category theory and type theory are of course closely related. $\endgroup$
    – Nathan BeDell
    Commented Feb 13, 2017 at 14:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .