digama

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 things to add or behaviors to tweak. That's why software engineering is a thing.

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, you can consider many "natural" classes of functions, such as computable functions, recursively enumerable functions, etc. and for each such enumeration there will be a "natural" function that escapes the class. Functions to do with definability or (in this case) 'interestingness' are especially susceptible to this. See also "Tarski's theorem on the undefinability of truth".

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 don't think we can exclude independence as an option for any currently open question without actually proving or disproving it. (Of course, most mathematicians don't really think that P=NP will turn out to be independent, any more than the Riemann hypothesis or Goldbach's conjecture, but we don't know for sure.)

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 doesn't change this; instead it effectively augments the system with certain "nonstandard" natural numbers (which are larger than any concretely describable term but "look" like regular natural numbers from within the system), and this mythical polynomial algorithm for 3SAT will have nonstandard length (meaning for pratical purposes that it is infinitely long).

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 size preserved by euclidean motions, unless you put points on top of each other.) Needless to say, gathering an infinite number of electrons or protons will cause black hole-themed "reality breakdown" problems long before you get there.

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 as better estimates of this real number. Using rational numbers or other countable sets in this position usually leads to undesirable biases and or circuity in the model. When you need a "continuum", the real numbers have the best properties for the job.

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 two-dimenional free group in just three-dimensional rotations. This is an infinite discrete set, a sort of analogue of the integers (which is the one-dimensional free group). In the integers it is no surprise (or maybe it is) that you can take the positive integers and shift them all to the right by one unit and then suddenly you have made a "hole" from apparently nothing (the Hilbert's hotel paradox). One worrisome part of this is that the "rooms" must get infinitely far away, but B-T exploits the fact that by using irrational rotations you an wrap the whole construction into the space taken up by a single sphere.

Add just a little more mathematical mumbo jumbo and you have a two-dimensional free group, which is a hotel such that every room is as big as all the rest of the rooms and you can set up the hotel so that each room is as big as all the rest of the rooms, and then you can do magic such that a move to the left actually leaves as much space as the whole hotel. And since it's all wrapped up in a ball it doesn't even run off to infinity to do this.

You do need the rooms to be points with zero volume, though; otherwise even with one-atom rooms you still need to shove the entire infinite hotel into a finite space and you will run out of room.

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 is known as a "counting measure" in measure theory.) It is the presence of infinities in the real numbers that causes this measure to fail (you will end up measuring the B-T sets, and regular objects like spheres as well, to have infinite "mass", so that 2*infinity = infinity is no longer as surprising a result).

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 formula or algorithm (which is connected to the fact that the axiom of choice is needed to even prove these sets exist).

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, in order to increase its proving capability, at the expense of tying it to its axiom set.

By contrast I can tell you that Metamath (http://us.metamath.org/mpegif/mmset.html), whose main library is also built on ZFC, does not at the most basic level assume any axioms at all (not even first order logic), so it is possible to do type theory or HoTT with no change to the verifier.

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 bijection with the natural numbers (and of course finitely many means in bijection with some natural number). A proof by contradiction will only give the weaker first statement in intuitionistic logic.

One explanation for why many people say that Euclid's proof is not a proof by contradiction is because you can actually get the second statement with only a little more care (i.e. n!+1 has a prime divisor, which is thus greater than n).

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 surprising. But it is impossible to truly overcome this, and it certainly goes a long way to improve confidence in the system.

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 programmer" who works with Metamath for much the same reasons as people use Coq (I just happen to prefer Metamath's set theory foundations to type theory). I find the article's claim "Set theory has sufficed as a foundation for more than a century, but it can’t readily be translated into a form that computers can use to check proofs" as outright false for this reason. Mizar is another set theory-based proof system.

If I wanted to prove x <= n -> x = 0 or x = 1 or ... or x = n, I would use http://us.metamath.org/mpegif/leloe.html to turn x <= n <-> x < n or x = n, and http://us.metamath.org/mpegif/zltlem1.html to prove x <= n-1 from x < n. Repeat until you get down to zero to get all n cases.