Timeline for Direct construction of the integers
Current License: CC BY-SA 3.0
38 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 28, 2017 at 11:17 | comment | added | Carl Mummert | In the case of the integers (and this is well known) we can avoid a quotient by just redefining the operations to always produce a value in a particular set of representatives. For example we could define an integer to be a pair $(m,n)$ of naturals in which $m = 0$ or $n = 0$ - the set of such pairs is a selector for the usual equivalence relation used to define integers. Then we define the operations to always produce a result in our set. So the issue of having a quotient seems like it is a chimera. The same thing happens for the construction of $\mathbb{Q}$ from $\mathbb{Z}$, etc. | |
| Nov 28, 2017 at 10:45 | answer | added | CopyPasteIt | timeline score: 0 | |
| Apr 13, 2017 at 12:58 | history | edited | CommunityBot |
replaced http://mathoverflow.net/ with https://mathoverflow.net/
|
|
| Dec 22, 2016 at 17:57 | comment | added | Jonathan Beardsley | Wanted to use the fundamental group of the circle, but then realized this required quotienting by homotopy equivalence. | |
| Dec 22, 2016 at 14:57 | history | edited | Francesco Polizzi | CC BY-SA 3.0 |
added 25 characters in body
|
| Sep 19, 2016 at 12:43 | vote | accept | Jacques Carette | ||
| Sep 19, 2016 at 12:41 | comment | added | Jacques Carette | @HeinrichD that is covered in the question: I would like something like an inductive type for $\mathbb{Z}$, which is constructed directly. Yours is an indirect construction. And I really should have asked about the ring of integers. | |
| Sep 16, 2016 at 18:46 | comment | added | HeinrichD | Since the question is only about the set of integers: What's wrong with $\mathbb{Z} := \{0\} \cup \mathbb{N}^+ \times \{0,1\}$? Here $(n,0)$ means $+n$ and $(n,1)$ means $-n$. | |
| Aug 18, 2013 at 18:54 | answer | added | Gerald Edgar | timeline score: 3 | |
| Aug 18, 2013 at 17:14 | comment | added | Włodzimierz Holsztyński | @Gerald Edgar, you may insert your $(-1\ 0\ 1)$ construction into a separate answer. Then I will remove my copy. | |
| Aug 18, 2013 at 1:14 | comment | added | Mariano Suárez-Álvarez | Maybe god gave us the natural numbers and forced us to do some work to get the integers? | |
| Aug 18, 2013 at 1:10 | answer | added | Włodzimierz Holsztyński | timeline score: 1 | |
| Aug 16, 2013 at 14:38 | answer | added | Chandan Singh Dalawat | timeline score: 3 | |
| Nov 8, 2011 at 12:27 | comment | added | Jacques Carette | I don't disagree! I just wanted to "explore the design space" a bit more, to see what is possible. | |
| Nov 8, 2011 at 10:49 | comment | added | Andrej Bauer | In that case, I would go for two-level inductive definition, followed by lemmas that show the thing has the correct universal property. Then you just keep proving everything from the universal property. Which leads to teh natural conclusion that you shouldn't really worry about how the integers are constructed, but rahter than what they are. Your proofs should not rely on any particular construction of the integers. That's my opinion. | |
| Nov 7, 2011 at 21:27 | comment | added | Jacques Carette | @Andrej: a combination of the last two. I want a quotient-free construction of the integers, as this is easiest to handle in all existing proof assistants, and is at the same time 'more elegant'. It really does not feel like something as fundamental as the integers should require a 'complicated' construction. A good representation should allow for proofs about properties of the integers which are 'structural', in the same way one easily gets structural proofs for most properties of the naturals, but without reference to the naturals. | |
| Nov 7, 2011 at 17:16 | answer | added | David Milovich | timeline score: 15 | |
| Nov 7, 2011 at 14:17 | comment | added | Andrej Bauer | Could you explain your motivation? Are you trying to get an efficient implementation of the integers, or something that works well in a proof assistant, or something that is mathematically elegant, or what? | |
| Nov 7, 2011 at 11:38 | answer | added | Leo Alonso | timeline score: 2 | |
| Nov 7, 2011 at 11:27 | answer | added | S. Carnahan♦ | timeline score: 13 | |
| Nov 6, 2011 at 16:18 | answer | added | Valerio Capraro | timeline score: 2 | |
| Nov 6, 2011 at 13:39 | vote | accept | Jacques Carette | ||
| Nov 6, 2011 at 13:43 | |||||
| Nov 6, 2011 at 13:28 | answer | added | Lii | timeline score: 3 | |
| Aug 3, 2010 at 4:32 | comment | added | Kaveh | How about using two types? One for non-negative integers and one for negative ones, each having one function and one constant. | |
| Aug 1, 2010 at 12:36 | comment | added | Jacques Carette | @Kaveh: those axioms induce a quotient. | |
| Aug 1, 2010 at 7:33 | comment | added | Kaveh | 0 (zero), S (successor) , P (predecessor) Add the axioms PS(x)=SP(x)=x. | |
| Jun 28, 2010 at 11:49 | comment | added | Jacques Carette | @Russell: indeed. Seems unfortunate that there is not obvious, straightforwardly irredundant, elegant and direct construction of the integers. [The initial object in the category of unital rings is certainly an elegant characterization!] | |
| Jun 28, 2010 at 9:57 | comment | added | Russell O'Connor | @Jacques: Defining Integers to be Maybe (Either Positive Positive) is also a 2-level definition (well it is once you combine Maybe (Either x x) into one level). | |
| Jun 22, 2010 at 21:23 | comment | added | Daniel Litt | Ah sorry, leading indeed. | |
| Jun 22, 2010 at 16:39 | comment | added | Jacques Carette | I take my 'redundant' comment back - this seems to be a good answer. The only remaining difficulty are the leading zeroes (rather than the trailing zeroes) which would exist in a naive inductive definition of strings of symbols. A 2-level definition can take care of that, though that is somewhat inelegant. | |
| Jun 22, 2010 at 16:06 | comment | added | Daniel Litt | You're fine as long as you eliminate trailing zeros, which I suspect is the objection. | |
| Jun 22, 2010 at 15:57 | comment | added | rgrig | Balanced ternary doesn't seem redundant. en.wikipedia.org/wiki/Balanced_ternary Do you have a (counter)example? | |
| Jun 22, 2010 at 14:33 | comment | added | Jacques Carette | @Gerald: isn't your second construction 'redundant' (some numbers are multiply represented) so that you would need to take a quotient? Yes, that is direct enough. | |
| Jun 22, 2010 at 14:31 | history | edited | Jacques Carette | CC BY-SA 2.5 |
more clarification
|
| Jun 22, 2010 at 14:24 | history | edited | Jacques Carette | CC BY-SA 2.5 |
clarify
|
| Jun 22, 2010 at 14:18 | comment | added | Gerald Edgar | Strings of symbols, from a three-letter alphabet (representing digits 0, 1, -1; thought of as base 3 expansions). All but finitely many digits must be zero. Define operations essentially as in grade-school. Is that what you want for "direct"? I took balanced ternary, since you don't want to start with positive integers... | |
| Jun 22, 2010 at 14:13 | comment | added | Gerald Edgar | The free group on one generator? Or do you want to define multiplication, as well? Maybe you should provide an example of a "direct" construction of something else to show what you have in mind. | |
| Jun 22, 2010 at 14:01 | history | asked | Jacques Carette | CC BY-SA 2.5 |