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 beauty book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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).
    • CommentRowNumber1.
    • CommentAuthorThomas Holder
    • CommentTimeJun 26th 2014

    I have added some sketchy remarks on Lindström’s theorem on first-order logic and a reference to predicate logic. Expert logicians hopefully can live with this or improve on it.

    • CommentRowNumber2.
    • CommentAuthorThomas Holder
    • CommentTimeJun 29th 2014

    I have revised and expanded the entry on the Löwenheim-Skolem theorem a bit. Hope the slight rewriting is ok!

    • CommentRowNumber3.
    • CommentAuthorThomas Holder
    • CommentTimeJul 2nd 2014

    Following the suggestions in the thread on geometric logic here, I’ve tried to be more explicit in predicate logic that the remarks on Lindström’s theorem there talk only about the standard fragment of first-order logic.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeJul 4th 2014

    Thomas, I have made some of your references to ‘standard [finitary] first-order logic’ say ‘classical untyped first-order logic’, since this is the standard (going back at least to Hilbert), the one relevant to Lindström’s Theorem, and more precise. But change that if you don't think that it says what needs to be said.

    • CommentRowNumber5.
    • CommentAuthorThomas Holder
    • CommentTimeJul 4th 2014

    I guess you have much better feel for what terms to use in order to get the message through to the nlab’s intended readership. So if by any chance you happen to pass at Lindström’s theorem you might find other occasions to check or harmonize the terminology.

    Concerning ’untyped’, (the reason why I absorbed it into the vague term ’standard’ is probably that) I somewhat fancy the idea that the equivalence of coherent logic to classical first-order logic over the class of Boolean toposes (a point that Lawvere likes to stress) could actually be subsumed under a typed version of the Lindström theorem with a categorical (well-pointed?) Boolean semantics which then of course is going to be interpreted as a characterization of coherent logic namely that there is no logical system that is more expressive than coherent logic and satisfies compactness and the Löwenheim-Skolem theorem.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeJul 4th 2014

    Well, that would be pretty cool if true!

    • CommentRowNumber7.
    • CommentAuthorThomas Holder
    • CommentTimeJul 6th 2014

    I am rather optimistic that a Lindstöm type theorem holds over a sufficiently tame class of Boolean toposes (let’s say with enough points and an NNO). E.g. Väänänen suggests that the Craig interpolation theorem entails Lindström type results; and interpolation should already be established for coherent logic by Pitts and Makkai. I am rather afraid that the resulting Lindström theorem is straightforwardly just the classical result and would not offer anything new besides the possibility to spread the rumor that coherent logic is the only logic (well, probably I am naive, seen how much work Makkai has to invest in his monograph to get definability for Boolean pretoposes!). But to look seriously into this would take me too far afield: I was only trying to get my monadic SOL together for the Jonsson-Tarski-topos before Todd talked me into this.

    • CommentRowNumber8.
    • CommentAuthorzskoda
    • CommentTimeNov 2nd 2022

    predicate logic with equality. That means that one predicate symbol with two arguments =(x,y)=(x,y) (also written x=yx=y) is distinguished, and has to satisfy reflexivity, symmetry, transitivity and the rule of substitution: (x=yϕ(x))ϕ(y)(x = y \wedge \phi(x))\implies \phi(y) for any predicate ϕ\phi with one argument.

    Also added a link to future entry rule C.

    diff, v24, current

  1. adding redirects for variants of “predicate logic with equality” or “first-order logic with equality”, as well as a paragraph about first-order logic with apartness


    diff, v25, current