The idea of *internal stratification* is not to bother ourselves in determining whether a function is stratified or not, the system would run it for us, because it is an internal notion! And the system controls its properties, in the way we demand!
To avoid any confusion beforehand, the typing function T (mentioned below) is among the signature of our language, so it runs over objects in the universe of discourse of our theory, and not like the usual external stratification function which works on the syntax of our language.
Its pretty much simple, take ANY formula \phi in first order logic with identity and membership, simply obtain another formula \phi^Ti that is a conjunctive formula of all *i_typed renderings* of atomic subformulas of \phi, defined as:
the i_type rendering of x=y is the formula Ti(x)=Ti(y)
the i_type rendering of x E y is the formula Ti(y)=Ti(x) + 1
Then the formula (\phi \land \phi^Ti) is called an i_typed formula.
Example: (x = y \land x E y \land Ti(x)=Ti(y) \land Ti(y)=Ti(x) + 1), is an i_typed formula.
So formation of i_typed formulas is very easy, its nothing but a set theory formula in conjunction with a conjuctive tail of all i_typed renderings of its atomic subformulas.
Now ISF (Internal stratified comprehension) is the schema:
for all i Exists x for all y (y E x <-> phi \land \phi^Ti)
for any formula \phi in the language of set theory that doesn't have x free.
That's it, as simple as such.
Of course we need to add AXIOMS to this theory about the T function, and about +,1,=. So in nutshell our theory in written in FOL (=, N, 1, +, T, E)
the axioms about = are those of identity theory;
the axioms about N, 1, + are those of PA about them (replace "S(x)" in PA by "x+1")
axioms about T are what needs to be specified, those are simple.
T is a partial two place function symbol. With the only three axiom that are:
1. T(i,x)=j \implies N(i) \land N(j)
2. \forall x Exists i,j (T(i,x)=j)
3. \forall naturals i_1,...,i_n \forall x_1,..,x_n \exists j
(T(j,x_1)=i_1 \land .. \land T(j,x_n)= i_n)
I like to write "T(i,x)" as "Ti(x)".
axiom 3 above is called the axiom of permutations.
Simply RUN this theory, and you'll interpret SF.
Aug 29, 2020