FIRST ORDER LOGICISM
Here I'll show that we don't need second order as the logic for logicism (the use of Hum's principle + logic to derive axioms of arithmetic), we can directly use a first order base! This also proves that Atomic General Extensional Mereology + Multiple atoms exist + Hum's principle + cardinals are atoms. Would also interpret second order arithmetic!
Language: bi-sorted first order logic with equality =, set membership ∈, and a total one place function symbol N from sets to numbers, signifying "is the number of elements in". First sort objects are the natural 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 an upper case symbol on the right; also the symbol N can only take upper cases as arguments.
Sorts: ∀X∀x:x≠X
Numbers: ∀X ∃n:N(X)=n
Extensionality: ∀z(z∈X↔z∈Y)⟹X=Y
Definition: a<b⟺∃X∃Y:X⊊Y∧a=N(X)∧b=N(Y)
Comprehension: ∀n∃X∀y(y∈X↔y≤n∧ϕ(y)) for every formula ϕ in which X is not free.
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