I've not read ProfHewitt's argument, so I'm just looking at your summary.
If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them), then I don't understand what ◻◻UNP means, because ◻UNP is not a proposition of the implicit formal system.
If we were doing this in Peano Arithmetic using Gödel numberings, then ◻P would be expression by taking the Gödel number encoding P and applying a predicate that expresses provability to that number.
This might be written as like, Provable«P» with the quotes indicating taking the Gödel number of the proposition P, in order to encode it in a way that Peano arithmetic can talk about. (Usually one uses the right angle brackets on the upper corners for the quoting, but my phone doesn’t have that on the keyboard, which is why I’m using “«“ and “»”). Statements like this are statements in the same formal system as P.
The modal logic known as “provability logic” is a nice abstracted system which captures how these things work, and allows for dealing with them in a general case.
◻◻P is perfectly sensible, and if the system is able to describe itself sufficiently well (which is not a high bar; Peano arithmetic satisfies this requirement.) then if you can derive P within the system (without additional assumptions), then, simply by including a proof that the proof of P is a proof of P, one can produce a proof in the system of ◻P,
And so, if one can derive ◻P, so too can one derive ◻◻P .
(ProfHewitt’s post also uses basically the same thing as ◻◻P , though he writes it using the turnstile symbol rather than the square symbol, and I prefer the square symbol for it, and the turnstile for something slightly different. Not saying the use of the turnstile for it is wrong though.)
You’re free to use a system that has orders of propositions, and I’m sure there are interesting things to be said about systems with such orders. (The set theory of NFU seems rather appealing, and stratified formulas seem somewhat analogous.)
(And yes, if you restrict what a system can do, it is possible to produce a system which can, in a sense, prove its own consistency. Dan Willard produced one such system. It has subtraction and division as fundamental rather than addition and multiplication.)
However, a theory is not required to have orders of propositions (Or, perhaps you might prefer saying this as “A theory can have all of its propositions be if the same order”?).
Furthermore, in a formal system modeling the mathematical properties of a syntactical system (as in, a set of rules describing allowed transformations on some strings), this also does not require having multiple orders of propositions.
And modeling what things are provable in a given formal system, is just that same kind of thing.
So, when describing in a formal system which well-formed-formulas can be derived within that system, it is not necessary (in the sense of “you don’t have to do it.”) to use multiple orders of propositions.
(Of course, in any formal proof of a wff which we interpret as having a meaning, there is perhaps a kind of gap between the string of characters which is provable within the system, and the thing which we interpret it to mean. However, if the system is sound with respect to our interpretation of it, then the things it proves will, under that interpretation of the system, correspond to a meaning which is true.
As such, it is usually safe to elide the distinction between “the string corresponding to this proposition is derivable in this formal system” and “this system proves this proposition” (where “this proposition” is taken to refer to some meaning).
When interpreting statements made in a system “about” that system, there are kind of two levels of interpretation, kinda-sorta. First, when we interpret a proof within the system that some statement(s) is(are) (not) provable in the system, we first have to interpret the string we have derived as corresponding to the meaning of a claim about the system, namely, a claim about what strings can be derived in the system. At that point, we also interpret what those strings that we interpret the first string as referring to, would mean.
This can perhaps sometimes be a little confusing.
Keeping this distinction in mind should make it clear why there is no need for orders of propositions when dealing with a system referring to what it can and can’t prove.)
Are you claiming that (e.g.) ZFC (which does not have orders for propositions) is not "foundations", or that it isn't consistent?
Or by "foundations" are you referring to a particular system you are proposing as a foundational system, and which you have named "foundations"?
You appear to justify the argument on the basis of the idea of a liar sentence.
As exemplified in NFU , it is not necessary to give strict orders to things, as long as you put restrictions on how things are constructed. TST has linearly ordered types, but NFU has no need to introduce these types and orders, as just requiring that formulas be stratified is sufficient.
There is no liar sentence in Peano Arithmetic. It isn't a well-formed-formula. Partitioning propositions into orders is not needed in order to prevent it being a well-formed-formula. Just, don't include anything in your rules for what counts as a wff which would let you define it.
(you may object that, what if one just does the Godel numbering thing to do some quine-ing, and uses that to produce a liar sentence, but you can't express "The proposition [some number] encodes, is false" in PA (see Tarski's undefinability theorem) .)
It isn't like UNK is defined in PA as "a statement UNK such that UNK iff not(provable('UNK'))". That wouldn't be a wff in PA. Rather, it is some long expression involving a bunch of quantifiers over natural numbers, and also a bunch of large numbers, and a bunch of arithmetical relations, and happens to be such that one can prove (in PA) that [UNK iff not(provable('UNK')] .
> If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them)
It doesn't mean that. The formal system is explicit: it's the system we're using to write statements like `◻P` (it's a form of modal logic https://en.wikipedia.org/wiki/Modal_logic ).
If ◻P means "P is a proposition that is formally provable within some implicit formal system" (perhaps there should be a subscripted letter to show which formal system because there are an infinite number of them), then I don't understand what ◻◻UNP means, because ◻UNP is not a proposition of the implicit formal system.