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.)

I'm trying to wrap my head around how P=NP could not have an answer, and I am not having much success. It could be that I am not educated enough to understand.

Notwithstanding that, I don't see how any of this relates to my original question.

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).

> If P=NP is independent, then we already know that a complete search for a polynomial algorithm for 3SAT will fail

A search for a provably polynomial algorithm will fail, but that doesn't mean that an unprovably polynomial time algorithm couldn't exist. We might come up with strong arguments for why a particular algorithm would be polynomial in practice. Still, I'd say "independent but false" is more likely than "independent but true."

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.