Talk:Type (model theory)

Please add {{WikiProject banner shell}} to this page and add the quality rating to that template instead of this project banner. See WP:PIQA for details.

Mathematics B‑class Mid‑priority

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
B	This article has been rated as B-class on Wikipedia's content assessment scale.
Mid	This article has been rated as Mid-priority on the project's priority scale.

Example of a type

The example about ${\sqrt {2}}$ confuses me. I have corrected the obvious problem: If $x={\sqrt {2}}$ (say, in reals) then for y smaller than $-{\sqrt {2}}$ it is not true that $y^{2}>2\implies y>x$ (there is nothing about considering just positive reals in the article).

The definition of type that I know requests that if $\phi (x)$ and $\psi (x)$ belong to the type in a certain model, then also $\exists x(\phi (x)\wedge \psi (x))$ holds in the model (that is, $\phi \wedge \psi$ is consistent with the model). Thus, if the example statements about ${\sqrt {2}}$ are meant as a type in model of rationals then we would need examples of two conditions that are also met by some rational number. Or maybe what is meant by the example is a type in the theory of arithmetics, because being consistent with a model of a theory and being consistent with a theory are differnt things?

I am not an expert on this, so a second opinion would be helpful.82.208.2.227 15:23, 25 September 2006 (UTC)[reply]

Two replies to the above. 1. As regards the example, it now reads $y>0\land y^{2}>2\implies$ . 2. In general a (partial) type is not required to be a filter. Any (partial) type has however its set of concequences which is a filter of the set of formulae. I prefer to use (partial) types this way, it is not however totally standard. Something else: The word type is often used to mean complete type, and partial type is used for the general notion. Unfortunately there is not widespread agreement on this, different papers have a different convention. In my experience, the latter view of types being complete is more widespread, as in many areas one need only consider complete types. Comments? Thehalfone 10:25, 3 October 2006 (UTC)[reply]

1. Yes, I have corrected the example and noted it on the discussion page because I felt that a little explanation is in order. Sorry, if it confused anyone. I still think that the definitions could be cleared up a bit (preferably by an expert). 2. The lecture on logic that we have had (at Charles University, Prague) used the opposite convention. 82.208.2.227 20:07, 12 October 2006 (UTC)[reply]

I appreciate a lot the content of this article, but the language looks pretty obscure and at times just awkward. I wonder if somebody could improve it. Not being a specialist in type theory, I'd rather abstain from doing it myself. --Vlad Patryshev 16:06, 12 April 2007 (UTC)[reply]

lede needs help

I agree that the article as it stands lacks sufficient context, and I've tried to add a better lede, but what I'm missing is _why_ types are significant, or some kind of analogy as to what they're _like_ -- for example it was explained to me that the diagram of a structure is 'analogous' to the multiplication table for a group -- I cannot find any similar useful and correct analogy for types that would provide motivation for why we study them. The rest of the article does (I think) a good job explaining what types are and what you can do with them. Help! Zero sharp (talk) 18:33, 15 August 2008 (UTC)[reply]

saturated structures

There should also be a link/mention of saturation since that concept is defined in terms of types Zero sharp (talk) 18:36, 15 August 2008 (UTC)[reply]

Omitting Types

Given a complete n-type p one can ask if there is a model of the theory that omits p, in other words there is no n-tuple in the model which realizes p. If p is an isolated point in the Stone space, i.e., if {p} is an open set. It is easy to see that every model realizes p (at least if the theory is complete). The omitting types theorem says that conversely if p is not isolated then there is a countable model omitting p (provided that the language is countable).

This is really unhelpful to me and I know at least basic model theory. There needs to be an explanation of the relationship between topology and model theory - the link to the topological notion of an open point doesn't help me to understand how an element of a model's domain can be isolated. What exactly are the conditions under which a type is omitted? —Preceding unsigned comment added by Dr satsuma (talk • contribs) 12:10, 12 March 2010 (UTC)[reply]

Incorrect example of elementary extension

The example where one constructs the elementary extension of the natural numbers with order is not actually elementary, as the model satisfies the sentence there are two elements with no immediate predecessor, which the naturals do not satisfy. — Preceding unsigned comment added by 84.248.64.88 (talk) 23:11, 12 February 2012 (UTC)[reply]

I'm not sure why you think the other model satisfies that sentence. If you're correct about that, then of course you're also correct that it's not an elementary extension, but I don't think you are. Nonstandard models of arithmetic all have the property that there is only one element that does not have an immediate predecessor. --Trovatore (talk) 23:17, 12 February 2012 (UTC)[reply]

As far as I can tell, there is no example where an elementary extension is constructed. Just one that says "Here's a type, if we could realize this in some elementary extension this is what we'd end up with." And then a warning that this isn't the same as just adding one element to realize the type because that element would be definable and so the extension would not be elementary. In reality, by compactness, we can realize the type in some elementary extension. As the property "There exists a unique element x such that for all y we have x not equal to s(y)" is first order and true in true arithemetic (or PA if you want), it will be true in the elementary extension given by compactness. So, I'm guessing your confusion was just with you thinking the non-example was an example. 24.131.192.199 (talk) —Preceding undated comment added 22:47, 13 February 2012 (UTC).[reply]

I'm quite confident that the example given is not an elementary extension. If the language only contains the ordering, then adding the integers on top of the naturals would make it an elementary extension, as no new element without immediate predecessors would be added. If the language contains addition, multiplication and so forth, then constructing an elementary extension would not be so easy.

Anyway, the statement that ${\mathcal {N}}$ and ${\mathcal {N'}}$ are elementarily equivalent is not true. Now for example the formula $\exists x\exists y(x\neq y\wedge \forall z(x\leq z)\wedge \forall w<y\exists w'(w<w'<y))$ is true in ${\mathcal {N}}'$ but not in ${\mathcal {N}}$ .