Philosophers have sought a means to isolate the properly logical components of a language from the remainder. A prominent idea here has been to use invariance under arbitrary permutations of the domain of objects. Some, e.g., Friederich Mautner and Alfred Tarski, have seen this as an extension of the Erlangen program of Felix Klein, which looked to distinguish geometries by their invariance under different transformation groups.
Tarski’s informal definition (Ln) is reproduced here,
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.
Logic is now to be seen as the maximally invariant theory.
In the propositional case, consider the symmetric group, $S_n$, acting on a set, $X$, of cardinality $n$. Then it also acts on all cartesian powers, $X^k$. Subsets of $X^k$ are $k$-ary relations, and those invariant under $S_n$ are unions of the orbits of its action. The idea then is that such relations are invariant if and only if they are definable using only logical constants.
Johan van Benthem proposed (JvB) such a treatment for a certain type theory. Steve Awodey (ULL) has argued that homotopy type theory should be seen in a similar light as expressing invariance under the broader notion of equivalence. In (UPL) he speaks of what he calls 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.
John MacFarlane, Logical Constants:Permutation invariance, SEP
F. I. Mautner, An Extension of Klein’s Erlanger Program: Logic as Invariant-Theory, American Journal of Mathematics, Vol. 68, No. 3 (Jul., 1946), pp. 345-384 (based on Hermann Weyl‘s formulation of the program in Classical Groups, pp. 13-18)
Alfred Tarski, 1986, What are Logical Notions?, History and Philosophy of Logic, 7: 143–154. (Transcript of a 1966 talk, ed. J. Corcoran.) doi:10.1080/01445348608837096
V. McGee, 1996, Logical Operations, Journal of Philosophical Logic, 25: 567–580
Denis Bonnay, Logicality and Invariance, lecture series (under ‘Enseignement’)
Denis Bonnay, Logicality and Invariance, Bulletin of Symbolic Logic 14 (1):29-68 (2006), pdf
Johan van Benthem, Logical constants across varying types, Notre Dame J. Formal Logic 30 (1989), no. 3, 315–342, (pdf)
Steve Awodey, Univalence as a logical law, talk at conference, Bristol 15 Sept 2016.
Steve Awodey, Univalence as a Principle of Logic, (preprint)
Last revised on August 24, 2020 at 09:01:49. See the history of this page for a list of all contributions to it.