digama

5 ms·

1.
by digama 11y ago
No software ever does exactly what we want it to do, because we are all different and have different demands on our programs. Even the author of a program is usually never truly "finished" with their program, and always find new
2.
by digama 11y ago
You just defined a subset of the natural numbers, and asserted it has a Godel number. Sorry, there are uncountably many subsets of natural numbers and countably many Godel numbers, so there is no guarantee that this is possible. More subtly
3.
by digama 11y ago
Just because a question is well-posed doesn't mean it must be provable or disprovable. Consistency of ZFC is also a perfectly well-posed question with a finite answer (if one exists), but we know it is impossible to prove regardless. I
4.
by digama 11y ago
If P=NP is independent, then we already know that a complete search for a polynomial algorithm for 3SAT will fail (because if there were such an algorithm it would prove P=NP, so it wouldn't be independent). Adding P=NP as an axiom doe
5.
by digama 11y ago
It's not just that the particles have to be zero size. There also have to be infinitely many. Otherwise, you could just count before and after and apply conservation of mass. (This also applies in mathematics: any finite set has its si
6.
by digama 11y ago
Oh but they do. When taking measurements in a scientific setting, it usually gives the most accurate and simple model to assume that your measurement is an approximation of a certain real number, and understand more accurate measurements
7.
by digama 11y ago
Short answer, yes that's a good way to think about it. The Hilbert Hotel paradox is closely related to the B-T paradox, it only adds a few more complications to make a stronger statement. The key step in the B-T paradox is setting up a
8.
by digama 11y ago
Conservation of mass is a consequence of the fact that matter is not infinitely divisible. The math on this works out too: there is an easy "measure" on three dimensional objects in the real world - just count the atoms. (This i
9.
by digama 11y ago
Fractals generally have a formula describing them, i.e. they are computable. Nonmeasurable sets are necessarily non-computable. This is why you will never see an accurate picture of the B-T sets, because they are not defined uniquely by any
10.
by digama 11y ago
I don't believe you could vary Mizar to the extent that it mimics HoTT. Much of the basic properties that follow from the axioms Mizar uses (roughly ZFC + the Tarski-Grothendieck axiom) are built in to the internals of the Mizar prover
11.
by digama 11y ago
I believe that in the context of the infinitude of primes, this is the difference between "NOT (finitely many primes)" and "infinitely many primes", where "infinitely many" means that the primes are in bijectio
12.
by digama 11y ago
It's already in this state. See Coq-in-Coq, where Coq formalizes its own foundations. Note that this is not entirely convincing, because if Coq was in fact inconsistent then the fact that it could prove its consistency is not surpris
13.
by digama 11y ago
For what it's worth, here's a proof that the primes are unbounded (and hence infinite) in the proof language Metamath: http://us.metamath.org/mpegif/prmunb.html . I would classify myself as a "proof prog