According to https://www.inc.com/bill-murphy-jr/science-says-were-sending-our-kids-to-school-much-too-early-and-that-can-hurt-th.html, when students get taught a concept when they're so young, they're less likely to be able to learn it properly. For example, some students really struggle to learn what fractions are and some people also can't understand how it's possible that irrational numbers exist after they learned how to represent all rational numbers and make calculations on them. Maybe if they avoid teaching that so early, they can use the time to teach the students stuff they actually can understand such as number theory and go quite far with it and then later, they can teach about real numbers so much more easily as a result of the knowledge about number theory they learned earlier. For example, they could completely avoid teaching them about the concept of cardinality of a finite set and teach only the definition of a natural number as an ordinal number because some of them might not have yet thought of their own proof that distinct finite ordinal numbers always correspond to different cardinal numbers.
Maybe they could teach them how to write a formal proof in a certain weak system of number theory after giving them the resources from which they can form an intuition that everything it proves is true where that system only talks about natural numbers. They might later test them on their ability to write a formal proof of the statement they're asked to write a formal proof of. If the student writes an intuitive reason why a certain statement is obviously true, the teacher will not progress with the material until after the student learns that the task was to write a formal proof the way they were asked to to show that they're able to figure out how to write a formal proof of it and masters the skill of figuring how how to write formal proofs of different statements when they're asked to write formal proofs of them. By waiting until all the students in the class master the skill of figuring how how to write a formal proof of a new statement when they're asked on a test to write a formal proof of that statement before moving on, they might gain the ability to think and figure stuff out really well and understand other material they're getting taught later.
Without being told ahead that these are some of the statements they're going to be asked to write a formal proof of so that they won't collaborate with another student to figure out the formal proofs of those statements ahead of time, here are some of the statements they could be asked to write a formal proof of except that those statements in their current form aren't actually describable in the system so they will be given strings of characters that represent a different but similar statement. They could be told on the test that by definition
- $\forall x \in \mathbb{N} x + 0 = x$
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N} x + S(y) = S(x + y)$
- $\forall x \in \mathbb{N} x \times 0 = 0$
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N} x \times S(y) = (x \times y) + x$
without any prior being introduced to the concept of addition and multiplication and then asked to write a formal proof of the following statements.
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N}\forall z \in \mathbb{N} (x + y) + z = x + (y + z)$
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N} x + y = y + x$
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N}\forall z \in \mathbb{N} (x \times y) \times z = x \times (y \times z)$
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N} x \times y = y \times x$
- $\forall x \in \mathbb{N}\forall y \in \mathbb{N}\forall z \in \mathbb{N} x \times (y + z) = (x \times y) + (x \times z)$
It could be even later that they're taught the inductive definition of the decimal notation for each natural number which goes as follows
To get to the successor follow the following rules
- If the last digit is not 9, increase that digit by 1
- If the sting of characters is 9, change it to 10
- If the last digit is 9 but is not the only digit, change that digit to a 0 and change the string of all digits before it to the string that represents the successor of that string
They can also be left to figure out on their own how to multiply numbers in decimal notation mentally and to know how to divide two numbers when ever the division problem is defined as well as learning how to check whether it actually is defined and write undefined when it's not defined instead of only knowing how to form a division strategy that always works when the given problem is defined and being the type of person who would write 8 as the answer to 14 $\div$ 3.
They might not get a feel that real numbers other than natural numbers actually exist but later, they could be taught how to become a savant at number theory who can discover results without reliance on a calculator, pencil and paper, a computer program, or the internet. They might later work in stronger systems of number theory dealing with more complex properties of the natural numbers the stronger system describes and when they read a book that uses the phrase real number, they might not understand what it's saying but will be so good at noticing patterns that they notice a certain connection between the text in the book and what they discovered about number theory and decide that when they talk about the real number $\sqrt{2}$, they're really informally describing a certain property of the natural numbers.
One down side of that is that not all real numbers correspond to a property of the natural numbers the system describes so the person might say that the real numbers it does describe are the only real numbers. They might later create their own version of type theory which is weaker than the already existing type theory to only extend number theory and not be at all an extension of ZF where Godel's first incompleteness theorem on proof systems of number theory is a meaningful statement and they don't assume unrestricted comprehension on all properties of the natural numbers anymore than normal type theory assumes unrestricted comprehension on all sets and will treat $\mathbb{R}$ like a proper class and not get along with mathematicans who work in Zermelo-Frankel set theory which does assert that there is a set of all subsets of the set of all finite ordinals and write formal proofs in it. Also, we can informally define ordinal numbers in terms of proof systems of pure number theory where stronger systems can define larger ordinal numbers. However, in that version of type theory, if we include the Church-Turing theris in the type theory, we could probably also derive that the ordinal numbers at and above the Church-Kleene ordinal don't exist at all. See https://mathoverflow.net/questions/133597/what-would-remain-of-current-mathematics-without-axiom-of-power-set/133598#133598