Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab: definition of geometric theory

Bottom of Page

1 to 20 of 20

  1.  
    • CommentRowNumber1.
    • CommentAuthorbezem
    • CommentTimeJun 18th 2014
    • (edited Jun 18th 2014)
    Why is a geometric theory on http://ncatlab.org/nlab/show/geometric+theory defined as a _first-order_ theory with _possibly infinitary_ disjunction? The latter would render compactness false, and compactness is one main characteristic of first-order logic (see http://en.wikipedia.org/wiki/Lindstr%C3%B6m%27s_theorem). I think this definition is self-contradicting, or in any case not in accordance with (classical) abstract model theory.

    Marc
    • CommentRowNumber2.
    • CommentAuthorZhen Lin
    • CommentTimeJun 18th 2014

    It is “first order” in the sense of not quantifying over subsets/predicates/relations. Nothing more than that is meant.

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 18th 2014

    It’s a very standard and well-established notion. See Johnstone’s “Elephant” book on topos theory for more information.

    • CommentRowNumber4.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeJun 18th 2014
    • (edited Jun 18th 2014)

    Also note that the class of geometric formulas is extremely interesting for reasons concerning base change: The truth of geometric formulas is preserved under pullback by geometric morphisms; this is detailed in the article you linked to.

    If you don’t care about topos theory, here is a more explicit way to state a related result. Recall that any modal operator □\Box gives rise to a translation φ↦φ □\varphi \mapsto \varphi^\Box of formulas. For instance, the well-known modal operator □=¬¬\Box = \neg\neg gives rise to the double-negation translation, and the operator □φ=((φ⇒F)⇒F)\Box\varphi = ((\varphi \Rightarrow F) \Rightarrow F) gives rise to Friedman’s FF-translation. (Here, a model operator should satisfy the following axioms: φ⇒□φ\varphi \Rightarrow \Box\varphi, □□φ⇒□φ\Box\Box\varphi \Rightarrow \Box\varphi, and □(φ∧ψ)⇔□φ∧□ψ\Box(\varphi \wedge \psi) \Leftrightarrow \Box\varphi \wedge \Box\psi. This is, in a somewhat different language, detailed at Lawvere-Tierney topology.)

    The result is the following: If φ\varphi is a geometric formula, then φ □⇒□φ\varphi^\Box \Rightarrow \Box\varphi, i.e. all □\Box’s appearing in the □\Box-translation may be pulled to the front.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2014
    • (edited Jun 18th 2014)

    If this terminology, standard and well-established in topos theory and related schools of thought, is not recognized in some parts of the community such as, I gather from #1, classical abstract model theory, then it would still be good to have a warning remark in the entry saying just this, for clarification. Something like

    Remark: While this terminology is standard in … beware that there is another convention in …

    Might any of the experts here have the energy to briefly add something like this to entry? That would be nice.

    • CommentRowNumber6.
    • CommentAuthorbezem
    • CommentTimeJun 18th 2014
    • (edited Jun 18th 2014)
    My point is not about different terminology in different communities: click on http://ncatlab.org/nlab/show/Elephant, scroll to D1.1, see under theories, and there are two subcategories: first-order and infinitary first-order. The way I understand it: "geometric" should use the latter (infinitary only for disjunction), "coherent" the former.
    • CommentRowNumber7.
    • CommentAuthorbezem
    • CommentTimeJun 18th 2014
    #4: Is the result still true for infinitary disjunctions? (I mean, pulling boxes to the front)
    • CommentRowNumber8.
    • CommentAuthorZhen Lin
    • CommentTimeJun 18th 2014

    What exactly is your objection? The red herring principle perhaps?

    • CommentRowNumber9.
    • CommentAuthorbezem
    • CommentTimeJun 18th 2014
    After what I read on http://ncatlab.org/nlab/show/Elephant (see #6 above), I would be most happy with the following parenthesis added: "A geometric theory is a (possibly infinitary) first order theory ..." (twice). An internal link to "infinitary first order theory" would be valuable (but there is no chapter on that). I'm not particularly fond of red herrings, but what I propose is actually a red herring: an infinitary first order theory is not a first order theory. The standard counterexample is \bigvee_n \phi_n, with \phi_n the formula \exists x_1,\ldots,x_n.~\forall y.~(y=x_1 \lor \cdots y=x_n). This infinite disjunction expresses finiteness, which is not first-order definable (because of compactness).
    • CommentRowNumber10.
    • CommentAuthorZhen Lin
    • CommentTimeJun 18th 2014

    OK. I have edited the article, in part also to clarify that axioms are sequents rather than just formulae.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2014
    • (edited Jun 18th 2014)

    Thanks to you two, for improving on the nLab entry!

    For bystanders: the edits are at geometic theory in the Idea section.

    • CommentRowNumber12.
    • CommentAuthorbezem
    • CommentTimeJun 19th 2014
    Thanks to Zhen for the editing. Maybe a last remark: it seems that there is a typo in the example concerning torsion: n>1 should be n>0 to include the disjunct x=0 written as 1*x=0.

  13. 4: Is the result still true for infinitary disjunctions? (I mean, pulling boxes to the front)

    Yes, it is. And it is false for infinitary conjuctions.

    In more detail, (⋁ iφ i) □≡□⋁ iφ i □⇒□⋁ iφ i(\bigvee_i \varphi_i)^\Box \equiv \Box \bigvee_i \varphi_i^\Box \Rightarrow \Box \bigvee_i \varphi_i is valid (assuming φ i □⇒□φ i\varphi_i^\Box \Rightarrow \Box\varphi_i for each ii), and (⋀ iφ i) □≡⋀ iφ i □⇒□⋀ iφ i(\bigwedge_i \varphi_i)^\Box \equiv \bigwedge_i \varphi_i^\Box \Rightarrow \Box \bigwedge_i \varphi_i is not.

    • CommentRowNumber14.
    • CommentAuthorThomas Holder
    • CommentTimeJun 29th 2014

    In the references for geometric theory I have added the Makkai-Reyes monograph and a pointer to some Lawvere remarks, and taken the ’elephant’ out of the scope of ’textbook’. I have also added ’geometric’ to ’positive’ as name for ’positive formula’ and fixed the formula for torsion groups as pointed out in the above remark #12 where I’ve changed the index to start with n=1 (it would presumably have been possible as well to simply delete the remark, that the formula asserts ’x=0’ as a disjunct).

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeJul 2nd 2014

    While I don't object to writing ‘possibly infinitary’ as a clarifying remark where Zhen put it, I do object to the idea that infinitary first-order theories are not really first-order theories. Logic is a very broad topic; finitary logic is a special case. It is an important special case (as can be seen by such results as Lindström's Theorem), but there is far too much assumption in the literature that it is the only case. (I blame Hilbert.)

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeJul 2nd 2014

    Actually, if I understand correctly what I've found online about Lindström's Theorem, the issue there is not even whether we are allowing infinitary language but whether we are allowing any variation from untyped first-order classical logic. It is that particular logic that is singled out by this theorem, if I understand it correctly.

    • CommentRowNumber17.
    • CommentAuthorThomas Holder
    • CommentTimeJul 2nd 2014
    I perfectly agree that geometric logic should count as a respectable infinitary first-order logic in the primary sense of indicating the types of variables and quantifiers. Nevertheless, there is a wide spread usage that identifies 'first-order logic' with classical finitary unsorted first-order logic and even the elephant makes a concession to this when it defines many sorted 'first-order theories' with the consequence that later on it has to add 'finitary' for clarification in the examples.

    It is 'first-order logic' in this narrow sense that the Lindström theorems talk about. Now, they don't justify a narrow first-order chauvinism but shed some light on the question why (relative to some classical background assumptions) early 20th century logicians hit upon this particular fragment: Löwenheim's 'theorem' (+compactness) carve it out of higher-order logic (As far as I can see, even the term 'first-order' originated with Löwenheim's 1912 paper) and the second theorem of Lindström shows that it has good proof theoretic properties in order to accomodate Hilbert's program.

    The classical background assumptions enter Lindström's theorems as 'regularity conditions' on the logical systems considered, among one finds a restriction to set-theoretic structures and the existence of semantic negation in the sense that, for every 'sentence' $\varphi$ there is a $\psi$ such that $A\models\varphi$ iff not $A\models\psi$.

    I felt that the entries on first-order logic and Löwenheim-Skolem theorem should at least point to Lindström's important results. My remarks are admittedly sketchy and can certainly be expanded and improved upon. I also think that the Lindström theorems deserve a proper entry but that would demand some familiarity with abstract model theory from the author.
    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 2nd 2014

    Why not create an entry on Lindström’s theorems to which one could link?

    • CommentRowNumber19.
    • CommentAuthorThomas Holder
    • CommentTimeJul 2nd 2014

    In my personal view, such an entry should contain a precise statement of the result, which is technically rather involved and should be done by somebody with some exposure to the state of art in abstract model theory. For instance I don’t have a good intuition how essential all the specific assumptions that enter really are i.e. can you relax these assumptions and still get similar results etc. ? after all, Lindström in 1969 extracted his concept of logical system by generalizing about the then common classical systems. A glimpse over the Väänänen paper suggests that the result transfers.

    All in all, I can live with the remarks as they are as side remarks, but wouldn’t like to have an entry containing only a side remark on its subject on my conscience. Though you are probably right that even a rudimentary entry on Lindström could be heplful and would hopefully recruit more easily some expert for further improvements. Anyway I wouldn’t object to some copy and paste on the remarks concerning Lindström in predicate logic.

    Funnily, the elephant has a definition of geometric theory in B4.2 that is very much in the spirit of abstract model theory and probably should deserve some mention in the nlab-entry.

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 3rd 2014

    Thomas: may I direct you to this? :-)

    Seriously, anything you do to get the ball rolling is appreciated. Not being an expert on something shouldn’t stop anyone from contributing in some small way.

1 to 20 of 20

  1.