My discovery about mathematics

                           1

You cannot write the proposition "x is a finite set." by a logical formula.
It's easy to prove it. If you are a strict formalist,you must remove this
proposition in the mathematics. You lose theorems about Noetherian rings
and compact sets. You cannot use direct sums and tensor products of modules.
You cannot write the proposition "x is an intuitional natural number." by
a logical formula. I prove it too. You cannot define N and the countable
set by formalism. It seems impossible to evolve mathematics by forlmalism.

                           2

Let's think a language including individual symbols N and d.
Let's write 1=Ø∪{Ø},2=1∪{1},…,n+1=n∪{n}….
And N={1,2,…n…}.
Let A be a countable axiom system of the standard mathematics. Assume that
(1∈N)∧∀x((x∈N)→(x+1∈N))∈A　(x+1=x∪{x})
∀x((1∈x)∧∀y((y∈x)→(y+1∈x))→(N⊂x))∈A.
N is an individual symbol expressing the set of the natural numbers for the
standard model.
d is a free individual symbol. The axioms except the axioms about equality
and the logical axioms don't include d.
If A∪{d=m} (m∈N) isn't consistent, A |- d≠m.
A |- ∀x(x≠m) A |- m≠m So A∪{d=m} is consistent.
A∪{P(d)} has a model M for which M |= d=m and is consistent
if A∪{P(m)} is consistent.
Let's think the next proposition.
(P1) There is a logical formula Fini(x) for which
∀c(M |= Fini(c) ⇔ ∃n∃c₁…∃c_n(∀c"((M |= c"∈c) ⇔
((M |= c"=c₁)∨…∨(M |= c"=c_n))))
M is an arbitrary countable model of A.
Fini(x) means that x is a finite set.
Theorem 1.If the standard mathematics is consistent, (P1) isn't formed.
Proof. Assume (P1) and consistency of A.
Put B_m=A∪{m∈d, Fini(d)} (m∈N).
If n≤m, B_n has a model M_m for which M_m |= d=m+1.

∪ Bn has a model Mm and is consistent.

n≤m

∪ Bm is consistent and has a countable model M for which

m∈N

M |= m∈d for ∀m∈N. M is a countable model of A.
M |= ¬Fini(d) then. But M |= Fini(d). This is contradiction. ♦
Let's think the next proposition.
(P2) There is a logical formula Num(x) for which
∀c(M |= Num(c) ⇔ ∃m((m∈N)∧(M |= c=m))).
M is an arbitrary countable model of A.

Theorem 2. If the standard mathematics is consistent,(P2) isn't formed.
Proof. Assume (P2) and consistency of A.
Put C_m=A∪{m∈d, Num(d)}.
Like the proof of theorem 1,

∪ Cm is consistent and has a countable model M for which

m∈N

M |= m∈d for ∀m∈N
M |= Num(d) ∴ ∃n((n∈N)∧(M |= d=n)).
M |= n∈d M |= n∈n This is contradiction.♦
Let M be a model of A.
If N is a set for M, M |= N⊂N and M |= N⊂N.
∀c(M |= c∈N ⇔ ∃m((m∈N)∧(M |= c=m)))
If N is a set for every countable model of A, you can set up that
Num(x)=(x∈N).
So there is a countable model of A for which N isn't a set.
The countable sets aren't sets for the model by the axiom of replacement.
You cannot treat the countable sets by formalism.
(To be continued.)