Construct discrete mathematical structures from non-discrete ones

>>8664819
Very good question!

HoTT would suggest that continuous space-like structures are actually more fundamental than discrete ones. But as far as I know you still have to explicitly define a natural numbers type, which is not exactly what you're asking. You could also define Z as the fundamental group of the circle.

N can also be defined as the least subset of R containing 1 and closed under adding 1, assuming that you already have R (e.g. in the second order theory of R). There is probably more to say on the question though.

Consider the x intercepts of sin(x). Sin(x) is itself a function existing in continuous space but it's x intercepts can be used to count discretely.

>>8664877
HoTT? sorry, i´m still new to mathematical analysis, could you give me sources where i can get more information about my question?

>>8664887
Google

>>8664887
homotopy type theory

you can define the reals like this

https://en.wikipedia.org/wiki/Tarski's_axiomatization_of_the_reals

and then generate the other structures

>>8665190
this guy gets it

>>8664819
>non-discrete ones
ones are all discrete, prove me wrong
1 1 1 1 1 1 1 1 1 1 = ten discrete ones

>>8664819
Set of all binary sequences, it's "made of" countable set of naturals and finite set {0, 1} and has continuum cardinality

>>8664819
Since we're talking about mathematical foundations and thus skirting the edge of mathematical philosophy then we should be careful to distinguish between discrete structures, the integers, and the naturals.

While it may be possible to produce discrete structures and the integers I argue that producing the naturals may expose some difficulties depending on your philosophical perspective of them.

I prefer Bertrand Russell's perspective. Here is a quote from his Introduction to Mathematical Philosophy.
>The use of mathematical induction in demonstrations was, in the past, something of a mystery. There seemed no reasonable doubt that it was a valid method of proof, but no one quite knew why it was valid. Some believed it to be really a case of induction, in the sense in which that word is used in logic. Poincare considered it to be a principle of the utmost importance, by means of which an infinite number of syllogisms could be condensed into one argument. We now know that all such views are mistaken, and that mathematical induction is a definition, not a principle. There are some numbers to which it can be applied, and there are others (as we shall see in Chapter VIII.) to which it cannot be applied. We define the "natural numbers" as those to which proofs by mathematical induction can be applied, i.e. as those that possess all inductive properties. It follows that such proofs can be applied to the natural numbers, not in virtue of any mysterious intuition or axiom or principle, but as a purely verbal proposition. If "quadrapeds" are defined as animals having four legs, it will follow that animals that have four legs are quadrapeds; and the case of numbers that obey mathematical induction is exactly similar.

Note that in this context, when we perform induction on subsets of the integers or reals (or even subsets of the naturals) we are actually invoking the axioms and stating that the set we're performing induction on is the naturals themselves.

(cont.)

>>8666283
(cont.)

>>8665190
Doesn't work for defining the natural numbers precisely because those axioms do not give us induction. There are some forms of real induction out there but if my memory serves they all rely on some variation of connectedness (formalized in a topological sense). So such induction wouldn't extend to discrete subsets.

>>8664877
For the same reasons as above I think the fundamental group of a circle would fail. I mean we could argue that algebraically similar but it doesn't have induction. At best we could argue that there exists an embedding of said group into the actual naturals that exist elsewhere.

With regards to your real number argument:
1) As above it only gives something that can be embedded into the naturals but not the naturals themselves.
2) It doesn't actually matter if you start with 1. You could start with any non-zero real number and add it to itself and the structure you would gain would be isomorphic to the one generated by 1.

All that said, there are methods of formalizing induction in type theory that I'm sure extend to HOTT. I'm not entirely unconvinced by your approach in this sense. Perhaps it is the case that structural induction is more fundamental than mathematical induction and thereby a type theoretic definition of the naturals with structural induction would be the naturals themselves (unfortunately type theory has nothing inherently to do with continuous mathematical structures so this may not help OP but I at least still think it's interesting).

>>8664887
HoTT is a pretty advanced subject anon.

It is a relatively new field where people are using comp sci's programming language + type theory + category theory approach to programming languages in order to formalize Homotopy Theory in a corresponding type theory which can then be formalized in a theorem prover (a special type of programming language) or be studied from a theoretical perspective (to produce mathematical results by applying category theory in more interesting ways). It sits at the intersection between pure mathematics and theoretical computer science.

The mathematical analysis you're doing is a much more old-school (but still important) way of formalizing mathematics that's built directly on axiomatic set theory and classical logic.

HoTT is a very popular field that is believed to have a lot of potential for the future of mathematics though personally I think the idea of using type theories to study mathematics as one does in HoTT is much more interesting.

All that said, nothing that anon said is specific to HoTT (except that HoTT likes continuous structures). The first statement is some basic algebraic topology and only needs some basic group theory and topology to understand, and the second statement is pretty much the real analysis approach you're doing now.

Keep on keeping on, anon. You asked an interesting question and I don't know if there exists an answer to it.