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 r

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')] .