Conjunction/disjunction of types

104 Views Asked by At

Let $T$ be a theory. A type $p(x)$ is a set of formulas in variable $x$ such that $T\cup p(x)$ is finitely satisfiable.

Question. What does disjunction (or conjunction) of types mean? More precisely, if $p(x)$ and $q(x)$ are types, then what do $p(x)\wedge q(x)$ and $p(x)\vee q(x)$ mean?

1

There are 1 best solutions below

0
On BEST ANSWER

Well, there is an obvious intended meaning of $p(x)\land q(x)$ and of $p(x)\lor q(x)$ in terms of satisfaction:

  • $a\in M$ satisfies $p(x)\land q(x)$ if $a$ satisfies $p(x)$ and $a$ satisfies $q(x)$.
  • $a\in M$ satisfies $p(x)\lor q(x)$ if $a$ satisfies $p(x)$ or $a$ satisfies $q(x)$.

Now the interesting thing is that these satisfaction conditions on $a$ are themselves definable by types.

  • $a$ satisfies $p(x)$ and $a$ satisfies $q(x)$ if and only if $a$ satisfies $p(x)\cup q(x)$. More generally, for a family of types $\{p_i(x)\mid i\in I\}$, we can use the notation $\bigwedge_{i\in I} p_i(x)$ for the type $\bigcup_{i\in I} p_i(x)$.
  • $a$ satisfies $p(x)$ or $a$ satisfies $q(x)$ if and only if $a$ satisfies $$\{\varphi(x)\lor \psi(x)\mid \varphi(x)\in p(x) \text{ and }\psi(x)\in q(x)\}.$$ More generally, for a finite family of types $\{p_1(x),\dots,p_n(x)\}$, we can use the notation $\bigvee_{i=1}^n p_i(x)$ for the type $$\{\bigvee_{i=1}^n \varphi_i(x)\mid \varphi_i(x)\in p_i(x)\text{ for all }1\leq i \leq n\}.$$

On the other hand, an infinite disjunction of types is typically not definable by a type.

The fact that types are closed under arbitrary conjunctions and finite disjunctions corresponds to the fact that closed sets are closed under arbitrary intersections and finite unions, since a (partial) type corresponds to a closed set in the Stone space of complete types.