# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeSep 27th 2016

I started a page logicality and invariance. In Bristol the other day, Steve Awodey was promoting the thought that HoTT is a realisation of that thrust to understand logic as maximally invariant.

What would it be to take that seriously? If invariants are picked up by dependent product in some $\mathbf{B} Aut$ context, could there be a useful context $\mathbf{B} Aut(\mathcal{U})$ for the universe $\mathcal{U}$?

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeSep 27th 2016

An attempt to work things out for a form of type theory:

• Johan van Benthem, Logical constants across varying types, Notre Dame J. Formal Logic 30 (1989), no. 3, 315–342, (pdf)
• CommentRowNumber3.
• CommentAuthorAnthony Durity
• CommentTimeOct 17th 2016
• (edited Oct 17th 2016)

Maybe include this quotation from that Tarski paper? [bottom of page 8]

Now suppose we continue this idea, and consider still wider classes of transformations. In the extreme case, we would consider the class of all one-one transformations of the space, or universe of discourse, or ’world’, onto itself. What will be the science which deals with the notions invariant under this widest class of transformations? Here we will have very few notions, all of a very general character. I suggest that they are the logical notions, that we call a notion ’logical’ if it is invariant under all possible one-one transformations of the world onto itself.

It is quite succinct and as Corcoran says in footnote 5, “Apart from Mautner 1946, which Tarski seems not to have known, this is, I believe, the first attempted application in English of Klein’s Erlanger Programm to logic.”

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeOct 17th 2016

Yes, by all means include that quote.

Slightly odd wording by Corcoran. Why not say

Apart from Hillary and Tenzing 1953, Ernst Reiss and Fritz Luchsinger were the first men to climb Everest?

I don’t see what Tarski’s ignorance of Mautner has to do with it. The latter hardly hid his intentions:

F. I. Mautner, An Extension of Klein’s Erlanger Program: Logic as Invariant-Theory

Apart from a billion or so people, I’m the fastest man alive.

• CommentRowNumber5.
• CommentAuthorAnthony Durity
• CommentTimeOct 17th 2016
• (edited Oct 17th 2016)

Regarding Corcoran’s wording. Noted.

I’ve made the edit. As it’s my first on this site can you check it to make sure that it is alright? Thanks! Should I add the DOI http://dx.doi.org/10.1080/01445348608837096 of Tarski’s paper? I have a copy of the PDF but it is copyrighted so I ought not link to it I guess.

• CommentRowNumber6.
• CommentAuthorDavidRoberts
• CommentTimeOct 17th 2016

Looks fine to me, but David C is more of an expert in the subject matter. I went ahead and took the liberty of adding the doi myself.

• CommentRowNumber7.
• CommentAuthorDavid_Corfield
• CommentTimeOct 17th 2016

Another factor in Mautner’s favour for you, Anthony, is that he was working in Dublin at the time.

Let’s give him a page Friederich Mautner.

• CommentRowNumber8.
• CommentAuthorAnthony Durity
• CommentTimeOct 17th 2016

Thank you David R! Interesting factoid David C! I must get to know a bit about Mautner.

• CommentRowNumber9.
• CommentAuthorDavid_Corfield
• CommentTimeAug 24th 2020

• CommentRowNumber10.
• CommentAuthorDavid_Corfield
• CommentTimeAug 24th 2020

Mentioned what he calls there the Tarski-Grothendieck Thesis

If a statement, concept, or construction is purely logical, then it should be invariant under all equivalences of the structures involved. A statement that is not invariant must involve some non-logical specifics, pertaining not to general logical form but to some particular aspects of the objects bearing the structure. If it is the hallmark of a logical concept that it should pertain only to general, formal structure and not to any specific features of the objects bearing that structure, then this formal character may be witnessed by the fact that the concept is invariant under all equivalence transformations.

• CommentRowNumber11.
• CommentAuthorDavid_Corfield
• CommentTimeAug 15th 2021

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeAug 16th 2021
• (edited Aug 16th 2021)

Reading through the entry, I find myself left thinking that probably this means to be about what elsewhere we called the “principle of equivalence”? In any case, I have added pointer to that page after the first occurrence of the word “equivalence” and also under “Related concepts”.

Otherwise I have hyperlinked more keywords, throughout, such as invariant and transformation group.

I feel there should be a hyperlink also on the first occurrence of the term “language”. Though I am not sure if our entry “language” is what wants to be referenced here? This would be good to clarify.

• CommentRowNumber13.
• CommentAuthorDavid_Corfield
• CommentTimeAug 16th 2021

There’s probably much to this that’s more of concern to philosophers. The separation of the analytic and synthetic components of a theory was of great concern to Carnap, and something famously deemed impossible by Quine. Maybe I’ll add some such context.

There are plenty of people still working on the logic as invariance idea, so to them it’s perhaps a way into HoTT that it involves a new form of invariance.

Something perhaps more interesting: Mautner was looking to classify all $Sym(X)$ invariants of $X^k$. Can we know that we haven’t missed some important type formation operation?

• CommentRowNumber14.
• CommentAuthorDavid_Corfield
• CommentTimeAug 16th 2021

• CommentRowNumber15.
• CommentAuthorUrs
• CommentTimeAug 16th 2021

What do you mean by “language” in the first line? Do you mean “natural language”? Do you mean what the $n$Lab has under “theory”? Best to add a hyperlink to whatever is meant.

• CommentRowNumber16.
• CommentAuthorDavid_Corfield
• CommentTimeAug 16th 2021

Yes, theory is better, thanks. I’ve changed it.

• CommentRowNumber17.
• CommentAuthorUrs
• CommentTimeAug 16th 2021

Thanks! Just to clarify that I didn’t mean to necessarily suggest that the word “language” needs to be replaced – if that is the term under which those active in this invariance debate will recognize their subject? Also, our entry theory says right away that “a theory is a formal language”. So maybe the reader might best be served if this entry here says

…components of a formal language (a “theory” in the sense of mathematical logic and model theory)…

?

• CommentRowNumber18.
• CommentAuthorDavid_Corfield
• CommentTimeAug 16th 2021

Hmm, been fiddling about. The trouble is that terms such as ’language’ and ’theory’ are used with varying degrees of precision. It can’t be that we’ve already got the logical language in which the theory is expressed resolved, because the whole point is to isolate what counts as logical.

I’ll have another think.

• CommentRowNumber19.
• CommentAuthorDavid_Corfield
• CommentTimeAug 16th 2021

I rewrote this somewhat. I came to think it’s more about the boundary of the logical and the mathematical, if anything.