Proposal: levels of strict sorts

[srghma]

strict sort wff means wff cannot be used in binders {...}. This is why mm0 is metalanguage for first order logic.

So, its like "level 0" type.

Why not make mm0 more general: allow levels of provable sorts.

e.g.
instead of

strict provable sort wff
sort nat

we write

strict(0) provable sort wff
strict(inf) sort nat

-- and also can

strict(1) provable sort wff2

-- Second-Order Logic quantifier:
-- We can bind `wff` (level 0) inside `wff2` (level 1) because 1 > 0.
term al2 {p: wff} (Q: wff2 wff): wff2;

-- then can something like this, dunno
theorem double_negation_law: $ al2 p (not2 (not2 p) <->2 p) $;

or even better the graph of sorts instead of levels.

Does it make sense? Is it already equal to first-order logic? I dont know type theory enough