I feel like I'm just reinventing Tarski's wheel with this idea, or maybe I'm even remembering what I've looked over with respect to Tarski's undefinability thesis and phrasing it in a way that resonates with me. Anyway, this is what I'm curious about:
- Let ℒ(S) be a function that takes a sentence S and outputs which ath-order logic that S "belongs" to. For example, "A is an element of B," would (presumably) be first-order, so ℒ(A is an element of B) = 1. Then (I suppose) ℒ(A is an element of an element of B) = 2, and so on.
- What happens, then, if we take S schematically and have ℒ(ℒ(S))? But this seems ill-formed, or deficient, or something along that line. Perhaps it would be better to write ℒ(ℒ(S) = a); then a (Lawverean?) fixed point of this is such that ℒ(ℒ(S) = a) = a.
- The Tarskian maneuver: but alternatively, maybe it's not possible to use ℒ(S) so schematically, but we must always defer to ℒ(ℒ(S) = a) specifically and get ℒ(ℒ(S) = a) = a + 1 (I suppose this is of a piece with how Russell had type indexes increase).
Is the above a way to formulate Tarski's reasoning, or does it apply to a separate (if similar/related) issue in metalogic?