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 comma 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 finite 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.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 1st 2020

    Added a little to the Idea.

    diff, v7, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2020

    I have added references

    as well as those three articles by Montague. Then I touched the Idea-section. Now it reads as follows:


    The principle of compositionality asserts that the nature of complex structures is entirely determined by that of their simpler parts and the way these are composed.

    This is sometimes called Frege’s principle after Gottlob Frege, although it was arguably assumed in Boole 1854, decades before Frege’s work, and possibly not even embraced by Frege (see Pelletier 01).

    The concept became popular in linguistics with the formalization of semantics of formal and informal languages via Montague semantics (Montague 70a, Montague 70b, Montague 73), where the principle asserts that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them.

    diff, v8, current

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 1st 2020

    But you’ve removed my reference to Frege’s principle being relevant to semantics. Now it makes it sound like he had some general stance on the nature of complex structures. I’ll try to put something back.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 1st 2020

    I’ve added in Montague’s use of Tarski’s truth definitions. No doubt the entry could be a lot better.

    diff, v9, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2020
    • (edited Jan 1st 2020)

    Sorry, didn’t realize I had removed that connection. Thanks for fixing.

    Regarding your mentioning of “Alfred Tarski’s work on truth definitions”, hopefully this could go with a pointer to the relevant nLab entry. Is it propositional extensionality?

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 1st 2020

    Yes, we should have stuff on this. It’s what being described at Tarski’s theory of truth.

    Ah, I see we have correspondence theory of truth. But whether Tarski provides such a thing is debated.

    Whether Tarski’s own definition of truth can be regarded as a correspondence definition, even in this modified sense, is under debate (SEP: The Correspondence Theory of Truth)

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 1st 2020

    Thanks. But what Wikipedia mentions under Tarski’s theory of truth is essentially what we mention at propositional extensionality, no?

    As a first approximation, would it seem right to have “Tarski’s theory of truth” redirect to “propositional extensionality”, until some energetic logicians arrives who gives us a more comprehensive entry?

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 1st 2020

    Added a reference for Tarksi’s work.

    diff, v10, current

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 1st 2020

    But what Wikipedia mentions under Tarski’s theory of truth is essentially what we mention at propositional extensionality, no?

    I don’t agree with that. Propositional extensionality is an axiom that makes sense inside one particular language. Tarski’s theory of truth requires either a language and a metalanguage, or a self-referential language with a truth predicate (which immediately involves one in questions of inconsistency).

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 1st 2020

    But we currently claim the connection at propositional extensionality: history and that arose from our discussions.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJan 2nd 2020

    I agree that Boole’s quote at propositional extensionality#history could be interpreted to refer to a case of propositional extensionality, at least when taken out of context (and I haven’t looked up the context). But Tarski is explicitly talking about a “theory of truth”, and I have trouble viewing propositional extensionality as having anything to do with a “theory of truth”. (And if, for instance, by “secondary proposition” Boole meant a metatheoretic proposition, then his quote would also not refer to propositional extensionality.)

    • CommentRowNumber12.
    • CommentAuthoratmacen
    • CommentTimeJan 2nd 2020

    The quoting at propositional extensionality is (according to the article itself) referring to an element of a universe rather than the corresponding type. Even just restricting to propositions, this is different from the object/metalanguage distinction that quoting refers to with Tarskian semantics.

    I hope everyone here knows that Tarski-style universes are not really providing a Tarskian truth predicate, right?

    In any case, I agree with Mike that propositional extensionality is something different than a theory of truth, and it’s not clear which Boole was talking about from that quote. (But I would’ve guessed a theory of truth, not extensionality.)

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJan 2nd 2020

    It’s also possible that this dichotomy is an inappropriate anachronism to impose on the 19th-century mathematician Boole, who was after all still struggling with Aristotelian syllogistic. But I think it’s fair to impose it on the post-Frege 20th-century mathematician Tarski.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 2nd 2020

    I tried to add in that the Boole connection came from Voevodsky.

    (see Voevodsky 14, slide 8)

    But I receive the error message ’An unexpected error occurred when rendering the table of contents’.

    And we ought to take out the Tarski. What would we name the page to include his idea? Semantic theory of truth?

  1. Hi David, I was able to edit the page just now. What change were you trying to make?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 2nd 2020
    • (edited Jan 2nd 2020)

    It still doesn’t work. I was trying to add the reference mentioned in #14

    ’(see Voevodsky 14, slide 8)’ after ’can be thought’

    and the reference to his talk slides.

  2. Unfortunately I’m still not sure exactly what you were trying to do but I have added both the reference and the citation to the entry now. No idea whether they are where you intended them; please try to move them to where you intended them, and if it does not work, please paste here the exact fragment of source code (including some surrounding source) that you tried.

  3. Oh, it is a different page that you are referring to I guess!

    • CommentRowNumber19.
    • CommentAuthorRichard Williamson
    • CommentTimeJan 2nd 2020
    • (edited Jan 2nd 2020)

    I think I have fixed propositional extensionality now, the ’Idea section’ had the wrong header depth. I added the reference but not the citation.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 2nd 2020

    Oh, sorry. Yes, that page. Have added the citation.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJan 3rd 2020
    • (edited Jan 3rd 2020)

    I hope everyone here knows that Tarski-style universes are not really providing a Tarskian truth predicate, right?

    Let’s all hope for this, fingers crossed. What else could we possibly do on a wiki like this?!

    …until some energetic logician arrives who gives us a more comprehensive entry

    • CommentRowNumber22.
    • CommentAuthoratmacen
    • CommentTimeJan 3rd 2020

    Well the short version is that a truth predicate takes plain syntax as input, while type codes from a universe are hardly ever plain syntax. And if they are plain syntax then they don’t satisfy propositional extensionality.

    I think it’s easier to not try and explain the connection Voevodsky saw, which was awfully creative. Aside from the difference between syntax and semantics, the convention T still seems to be only a special case of propositional extensionality.

    • CommentRowNumber23.
    • CommentAuthorThomas Holder
    • CommentTimeOct 11th 2020

    Added a Spinoza quote and some references.

    diff, v12, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeOct 11th 2020

    added the English translation and a hyperlink to the footnote

    diff, v13, current

    • CommentRowNumber25.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 11th 2020
    • (edited Oct 11th 2020)

    Added an English translation of the Spinoza quote. We could maybe add some further details around this. Spinoza’s ’proof’ of this proposition is that it ’evidently’ follows from the axiom ’The knowledge of an effect depends on, and involves, the knowledge of the cause’ because ’The idea of what is caused depends on the knowledge of the cause of which it is the effect’. Thus, as far as it goes, compositionality seems to be implicit in the proof of Proposition 7, i.e. part of the ’meta-logic’ of Spinoza’s work.

    In particular, Spinoza does not seem to be making any point himself about composionality here, taking it as ’evident’; his purpose is to draw the following corollary: ’Whatever follows formally from the infinite nature of God follows from the idea of God as an object of thought in God according to the same order and composition’. In other words an equating, in any ultimate sense, of the idea of something and its actuality.

    diff, v14, current

    • CommentRowNumber26.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 11th 2020
    • (edited Oct 11th 2020)

    We cross-edited, Urs (which probably means you ignored the page lock ;-))! I guess my edit will have overwritten yours, feel free to edit again if anything was lost; have to dash now!

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeOct 11th 2020

    It happens fairly frequently that “Anonymous” locks a page for over 30 minutes. In most cases this just means that a hapless bypasser clicked randomly around the nLab and then left. In the early years of the nLab I used to wait for these ghost edits to appear, now I just go ahead editing. On the off chance that a serious editor is at work, it is just my edit that gets lost this way, as in this case.

    But we had the same idea here; I just took the liberty to stick to the formatting I had: Let’s have the translation in the footnote itself, not to break the aesthetic effect that the original quote has where it is, and so that we have room to add hyperlinks to sources.

  4. Yes, no problem!