Language: bi-sorted first order logic with equality ==, set membership ∈∈, and a total one place function symbol NN from sets to numbers, signifying "is the number elements in". First sort objects are the numbers symbolized by lower cases, second sort objects are sets symbolized in upper case. We impose a syntactical restriction on formulas so that the atomic membership formulas can only have a lower case symbol on the left and a upper case symbol on the right; also the symbol N is only take upper cases as arguments.
The idea of this theory is to simply formalize natural numbers as cardinality function on finite sets, which is a common conception of numbers being differential indices of quantities of elements in sets. This can be done in first order logic without much use of schemata! Unlike the theory presented here, which relies extensively on use of schemata.
Extensionality: ∀z(z∈X↔z∈Y)⟹X=Y
Definition:
a<b⟺∃X,Y,Z(X⊊Y∧N(Z)=N(Y)∧a=N(X)∧b=N(Z))
Comprehension: ∀n∃X∀y(y∈X↔y≤n∧ϕ(y))
Well foundedness: ∃x∈A⟹∃x∈A∀y∈A(x≤y)
Define:S(y)=x⟺y<x∧∄z (y<z<x)
Define: X 1:1 Y⟺X,Y are empty
∨ [X,Y are nonempty ∧∃K:∃min {min X,min Y}∈K∧∀a∈X ∀b∈Y(∃min{a,b}∈K∧∃S(a)∈X→
∃S(b)∈Y(min{S(a),S(b)}∈K))]
Equinumerousity: N(X)=N(Y)⟺X1:1Y∧Y1:1X
Finiteness: X⊊Y⟹¬ Y1:1X
Question:
Is the above theory equi-interpretable with PA? or is it slightly stronger?