Timeline for How Would an Intuitionist Prove This?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 28, 2016 at 14:57 | history | edited | Carl Mummert | CC BY-SA 3.0 |
added 655 characters in body
|
| Sep 28, 2016 at 14:45 | comment | added | Carl Mummert | @cody: I see what you're saying. I will try to find a better way to phrase what I had in mind. | |
| Sep 28, 2016 at 12:49 | comment | added | cody | I'm confused about your first statement: it's obviously false if you take, say $P=R\vee Q$. | |
| Sep 27, 2016 at 12:22 | comment | added | Ingo Blechschmidt | I wholeheartedly with your answer. Two small additions: Firstly, one can prove "$\forall n,m \in \mathbb{N}: n = m \vee n \neq m" by induction. Secondly, a rather large and nice field which has decidable equality is the field of algebraic numbers. The extra information coming with an algebraic number, that is a polynomial with rational coefficient which has the given number as a zero, is enough to intuitionistically verify whether the number is zero or not zero. | |
| Sep 27, 2016 at 10:44 | comment | added | Carl Mummert | The constructive proof that each number is composite or not composite, in the systems I am thinking of, is easier if we define some helper functions. Let $f(a,b,k)$ equal 1 if $bk = a$ and let it be $0$ otherwise. Decidable equality of naturals shows that this is a function. Let $g(a)$ be the sum of $f(a,b,k)$ over all $b,k$ in the interval $(1,a)$. It can be shown in these systems that $g$ is a function. Then a natural number $a$ is composite if and only if $g(a) \not = 0$. By making more complicated inductive arguments, it should be possible to eliminate the use of the functions. | |
| Sep 27, 2016 at 10:35 | comment | added | J126 | Thanks. While it is probably outside the scope to describe this to the students, I don't feel morally opposed to including the proof in my notes. | |
| Sep 27, 2016 at 10:34 | vote | accept | J126 | ||
| Sep 27, 2016 at 10:30 | history | answered | Carl Mummert | CC BY-SA 3.0 |