Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorjesse
   • CommentTimeMay 4th 2017
   • PermaLink
   Author: jesse
   Format: MarkdownItexI've started filling out [[elimination of quantifiers]], adding some initial remarks and sketching the usual proof that algebraically closed fields eliminate quantifiers.

   I’ve started filling out elimination of quantifiers, adding some initial remarks and sketching the usual proof that algebraically closed fields eliminate quantifiers.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 8th 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThat's great -- keep those model theory articles coming! This is one area that could use beefing up within the nLab.

   That’s great – keep those model theory articles coming! This is one area that could use beefing up within the nLab.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeMay 8th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks, Jesse. I have added a pointer to the entry from _[Quantifiers -- Related concepts](https://ncatlab.org/nlab/show/quantification#RelatedConcepts)_. With every entry you create, it is good practice to think about which entries should link to it. This increases the chance that the entry will be found by people who, necessarily, don't a priori know that it exists.

   Thanks, Jesse.

   I have added a pointer to the entry from Quantifiers – Related concepts.

   With every entry you create, it is good practice to think about which entries should link to it. This increases the chance that the entry will be found by people who, necessarily, don’t a priori know that it exists.

4. • CommentRowNumber4.
   • CommentAuthorjesse
   • CommentTimeMay 8th 2017
   • PermaLink
   Author: jesse
   Format: MarkdownItexThat's a good idea (case in point, I didn't even know that general page on quantification existed). In keeping with your suggestion, I added a brief remark to the Idea section about how QE helps prove [[decidability]] (mentioning Tarski's theorem that real closed fields are decidable), and cross-linked [[quantifier elimination]] with [[decidability]] via their Related Concepts sections.

   That’s a good idea (case in point, I didn’t even know that general page on quantification existed).

   In keeping with your suggestion, I added a brief remark to the Idea section about how QE helps prove decidability (mentioning Tarski’s theorem that real closed fields are decidable), and cross-linked quantifier elimination with decidability via their Related Concepts sections.

5. • CommentRowNumber5.
   • CommentAuthorjesse
   • CommentTimeMay 26th 2017
   • (edited May 27th 2017)
   • PermaLink
   Author: jesse
   Format: MarkdownItexTowards proving the useful QE-criterion (currently Theorem 4.2 at [[quantifier elimination]]), I created [[substructure complete theory]] and proved there the [[semantic]] equivalent characterization of quantifier elimination that "T eliminates quantifiers iff T is substructure complete". The remaining thing to do is show that if you weaken "substructure complete" to "model complete", then to recover the above equivalence you need to additionally assume that $\mathbf{Mod}(T)$ has certain kinds of weak pushouts. After that the QE-criterion follows easily.

   Towards proving the useful QE-criterion (currently Theorem 4.2 at quantifier elimination), I created substructure complete theory and proved there the semantic equivalent characterization of quantifier elimination that “T eliminates quantifiers iff T is substructure complete”.

   The remaining thing to do is show that if you weaken “substructure complete” to “model complete”, then to recover the above equivalence you need to additionally assume that $\mathbf{Mod}(T)$ has certain kinds of weak pushouts. After that the QE-criterion follows easily.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 26th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhat does "infinite vector space" mean there? Just that the field is infinite? It doesn't sound like you mean infinite-dimensional.

   What does “infinite vector space” mean there? Just that the field is infinite? It doesn’t sound like you mean infinite-dimensional.

7. • CommentRowNumber7.
   • CommentAuthorjesse
   • CommentTimeMay 26th 2017
   • PermaLink
   Author: jesse
   Format: MarkdownItex@David_Corfield, it means "infinite dimensional if the field is finite, any dimension if the field is infinite." (Equivalently, just that the underlying set is infinite.) Strictly speaking, finite-dimensional vector spaces over finite fields also have quantifier elimination, but---I should have written this somewhere---all the theory that's being developed on the page only applies to infinite models. It turns out that [[substructure completeness]] is still an equivalent characterization for quantifier elimination in finite structures, but combined with the fact that [[elementary equivalence|elementarily equivalent]] finite structures are isomorphic, this usually appears as the statement "finite structures eliminate quantifiers iff they are ultrahomogeneous" (i.e. any isomorphism of substructures extends to an automorphism, which is one of the defining properties of a [[Fraisse limit]], which tend to eliminate quantifiers.)

   @David_Corfield, it means “infinite dimensional if the field is finite, any dimension if the field is infinite.” (Equivalently, just that the underlying set is infinite.)

   Strictly speaking, finite-dimensional vector spaces over finite fields also have quantifier elimination, but—I should have written this somewhere—all the theory that’s being developed on the page only applies to infinite models.

   It turns out that substructure completeness is still an equivalent characterization for quantifier elimination in finite structures, but combined with the fact that elementarily equivalent finite structures are isomorphic, this usually appears as the statement “finite structures eliminate quantifiers iff they are ultrahomogeneous” (i.e. any isomorphism of substructures extends to an automorphism, which is one of the defining properties of a Fraisse limit, which tend to eliminate quantifiers.)

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 27th 2017
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThanks, but I'm still missing something. Say we take $\mathbb{F}$ as finite. What does it mean to be "working with the theory of an infinite vector space" when considering vector spaces of the form $\mathbb{F}^n$? >For example, suppose we're working with the theory of an infinite [[vector space]] over a fixed field $\mathbb{F}$. Let $A$ be a linear transformation $\mathbb{F}^{n+1} \to \mathbb{F}^m$... Oh, are you allowing $n$ and $m$ to be infinite ordinals?

   Thanks, but I’m still missing something. Say we take $\mathbb{F}$ as finite. What does it mean to be “working with the theory of an infinite vector space” when considering vector spaces of the form $\mathbb{F}^n$?

   For example, suppose we’re working with the theory of an infinite vector space over a fixed field $\mathbb{F}$. Let $A$ be a linear transformation $\mathbb{F}^{n+1} \to \mathbb{F}^m$…

   Oh, are you allowing $n$ and $m$ to be infinite ordinals?

9. • CommentRowNumber9.
   • CommentAuthorjesse
   • CommentTimeMay 27th 2017
   • (edited May 27th 2017)
   • PermaLink
   Author: jesse
   Format: MarkdownItexOh, I see. There I meant to consider $\mathbb{F}$ as a vector space over itself and for $n$ and $m$ to be integers, so for the entire statement to be consistent (and to still be working in ordinary finitary first-order logic), $\mathbb{F}$ would have to infinite. Now that you've pointed this out, I think it might be best to remove the instances of "infinite" from the Idea section and then incorporate the comments from #7 into the Remarks.

   Oh, I see. There I meant to consider $\mathbb{F}$ as a vector space over itself and for $n$ and $m$ to be integers, so for the entire statement to be consistent (and to still be working in ordinary finitary first-order logic), $\mathbb{F}$ would have to infinite.

   Now that you’ve pointed this out, I think it might be best to remove the instances of “infinite” from the Idea section and then incorporate the comments from #7 into the Remarks.

10. • CommentRowNumber10.
    • CommentAuthorjesse
    • CommentTimeMay 27th 2017
    • (edited May 27th 2017)
    • PermaLink
    Author: jesse
    Format: MarkdownItexDone! This wouldn't be the same as just replacing $n$ and $m$ above with infinite ordinals, but you're right that we could also circumvent this by starting off with the vector space $\mathbb{F}^{\omega}$ and then working with a definable linear transformation $A : \left(\mathbb{F}^{\omega}\right)^{n+1} \to \left(\mathbb{F}^{\omega}\right)^{m}$. Since to do this you end up (after specifying a basis) specifying an $ m \times (n + 1)$ matrix $A$ over $\mathbb{F}$ anyways, this is an "[[interpretation]]" of the case where we started with $\mathbb{F}$ over itself, all inside $\mathbb{F}^\omega.$ (Scare quotes because we can only nail down an actual interpretation up to symmetries given by moving bases around, which are all indistiguishable to the model.) Which is neat, because it's like an $\mathbb{F}$-linear version of the usual trick of studying finite structures by interpreting them as finite [[imaginary element|imaginary sorts]] inside infinite structures (e.g. the theory of an equivalence relation with $N$ infinite classes on an infinite set).

    Done!

    This wouldn’t be the same as just replacing $n$ and $m$ above with infinite ordinals, but you’re right that we could also circumvent this by starting off with the vector space $\mathbb{F}^{\omega}$ and then working with a definable linear transformation $A : \left(\mathbb{F}^{\omega}\right)^{n+1} \to \left(\mathbb{F}^{\omega}\right)^{m}$. Since to do this you end up (after specifying a basis) specifying an $m \times (n + 1)$ matrix $A$ over $\mathbb{F}$ anyways, this is an “interpretation” of the case where we started with $\mathbb{F}$ over itself, all inside $\mathbb{F}^\omega.$ (Scare quotes because we can only nail down an actual interpretation up to symmetries given by moving bases around, which are all indistiguishable to the model.)

    Which is neat, because it’s like an $\mathbb{F}$-linear version of the usual trick of studying finite structures by interpreting them as finite imaginary sorts inside infinite structures (e.g. the theory of an equivalence relation with $N$ infinite classes on an infinite set).

11. • CommentRowNumber11.
    • CommentAuthorjesse
    • CommentTimeMay 27th 2017
    • PermaLink
    Author: jesse
    Format: MarkdownItexI wrote down the proof that [[model completeness#substructureconverse|model completeness + amalgamation implies substructure completeness]] and then (finally) sketched the proof of the QE-criterion at [[quantifier elimination]].

    I wrote down the proof that model completeness + amalgamation implies substructure completeness and then (finally) sketched the proof of the QE-criterion at quantifier elimination.

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 27th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexGreat. Thanks, Jesse. I don't know what it is about model theory, but I never feel quite at home there.

    Great. Thanks, Jesse. I don’t know what it is about model theory, but I never feel quite at home there.

13. • CommentRowNumber13.
    • CommentAuthorjesse
    • CommentTimeMay 27th 2017
    • PermaLink
    Author: jesse
    Format: MarkdownItexI still feel that way sometimes! (Conversely, many model theorists are allergic to the $n$POV, and more broadly to categories in general.)

    I still feel that way sometimes!

    (Conversely, many model theorists are allergic to the $n$POV, and more broadly to categories in general.)