51 lines
2.3 KiB
Markdown
51 lines
2.3 KiB
Markdown
|
title: Omitting types
|
||
|
|
date: 2016-03-15 00:00
|
||
|
|
tags: logic
|
||
|
|
---
|
||
|
|
|
||
|
|
**Definition.** A *type* $p(x)$ for the theory $T$ is a collection of
|
||
|
|
formulas with a free variable $x$ consitent with $T$.
|
||
|
|
|
||
|
|
-- see Michael Weiss' [explanation of types](https://diagonalargument.com/2019/05/06/non-standard-models-of-arithmetic-1/).
|
||
|
|
|
||
|
|
**Definition.** A type $p(x)$ is *principal* if there is a
|
||
|
|
formula $\alpha(x)$ such that $p(x)=\\{ \psi(x) \mid \alpha \vdash \psi \\}$
|
||
|
|
|
||
|
|
**Definition.** A type $p(x)$ is *full* if for every
|
||
|
|
formula $\psi(x)$ either $\psi \in p(x)$ or $\neg \psi \in p(x)$.
|
||
|
|
|
||
|
|
A full type can be seen as a way of describing an a generic "element"
|
||
|
|
of a theory. For any model $M$ and an element $m \in M$ we can
|
||
|
|
consider the full type $p(m)$ generated by $m$. It contains all the formlas
|
||
|
|
$\psi(m)$ that are true about $m$.
|
||
|
|
|
||
|
|
[Omitting types theorem](https://en.wikipedia.org/wiki/Type_(model_theory)#The_omitting_types_theorem)
|
||
|
|
says that given a _complete_ countable theory $T$ in a countable
|
||
|
|
language, there is a model $M$ of $T$ which omits countably-many
|
||
|
|
non-principal full types.
|
||
|
|
|
||
|
|
Why is the non-principal condition needed?
|
||
|
|
|
||
|
|
If a theory $T$ is complete, then any model of $T$ realizes all the
|
||
|
|
full principal types. For if $p(x)$ is a complete principal isolated
|
||
|
|
by $\psi(x)$, then $T \not\vdash \not \exists x.\psi(x)$, for otherwise the
|
||
|
|
type $p(x)$ would be inconsistent with $T$. Because $T$ is complete it
|
||
|
|
must be the case that $T \vdash \exists x. \psi(x)$. Then such $x$
|
||
|
|
realizes $p(x)$.
|
||
|
|
|
||
|
|
What happens if the theory $T$ is not complete?
|
||
|
|
|
||
|
|
Then it is not the case that all
|
||
|
|
models of $T$ realize all the full principle types. For instance take
|
||
|
|
Peano arithmetic, and take $T_1 = PA + Con(PA)$ and $T_2 = PA + \neg
|
||
|
|
Con(PA)$. Both $T_1$ and $T_2$ are consistent, thus they have models
|
||
|
|
$M_1$ and $M_2$. Then denote by $q(x)$ the type generated by the
|
||
|
|
element $0$ in $M_1$, and by $p(x)$ the type generated by the element
|
||
|
|
$0$ in $M_2$. Both of those types are isolated by the formula $\phi(x)
|
||
|
|
:= \neg \exists y. y < x$, because $\phi$ completely determines $0$.
|
||
|
|
Albeit those types are types for different theories, they are both
|
||
|
|
types for a common theory $PA$. Furthemore, those types are complete
|
||
|
|
and isolated. However, one of the types states the consistency of $PA$
|
||
|
|
and the other one points out the inconsistency of $PA$. Thus both $q$
|
||
|
|
and $p$ cannot be realized in the same model.
|