@PaulTaylor Some proofs really are proofs by contradiction under that definition. (For example, a student may start with "Assume that $\sqrt{2}$ is not irrational. That means it is rational. So...") Thus, a more correct statement is: "A proof exists that avoids a certain logical non-intuitionistic axiom." But this is about teaching high school students beautiful proofs. Are you really going to tell such a student "it is not a proof by contradiction"? If so, why stop there? One could say: "It is not a proof of a negation, it is a fill in the blank, weaker fragment proof."

@JoshuaZ I agree with your quibble, and will edit accordingly.

@Joe I think it really boils down to this. Given a specific Turing machine, is there an objective answer to whether or not it halts. My current answer is no. For all I know, even if we had the ability to create a new universe where we could build a Turing machine and run it forever in that universe, but in finite time in ours, we might get different answers depending on the universe we build.

Reread my post, with "we" not understood as an abstract "mathematical community", but with "we" read as "you and me and others reading along". (Anyway, we can agree to disagree whether learning mathematics for ourselves is a process of discovery.)

@TimothyChow I did. I know many others who were flabbergasted that there are these nonstandard models. But, if you were never surprised by this fact during your education, you can certainly modify my "we" to "many of us". (In hindsight, I see how naïve it was to have this belief. And yet, it is a common one among the uneducated. And it isn't so surprising since there are no computable nonstandard models.)

"L is a minimal model with a universal property, and so monism dictates that V must equal L..." It does not minimally model ZFC-Union. Nor of ZFC-Infinity. To argue that L is a minimal model, you need to first have accepted a list of axioms. That occurs before you can appeal to monism.

"Which operations would you like to add to Godel's collection?" Personally, none right now. But philosophically, I have no reason to think that transfinite combinations of them yield every conceivable operation on collections. That said, others have put forward lots of options! Really, take any property you can do with finite sets, generalize to an operation on infinite sets, and see what happens. What makes union and powerset so special that they get to work for infinite collections, but others don't? Finite sets are measurable, why shouldn't all collections be measurable?

Now, likewise apply it to the axiom of powerset, without which we wouldn't even have the reals...

@JesseElliott Good questions. Now change AC to the axiom of unions Why not allow a collection of collections where it has no union? Answer that question, and then translate back to AC. (My answer is: We accept the axiom of union, because we are familiar with unions in the context of finite sets, and we imagine it should similarly work for any collection of sets. Likewise, we accept AC, because we are familiar with fixing elements from finitely many nonempty sets, and we imagine it should work for any collection. Yes, both of these axioms limit the types of collections available.)

Regarding accepting V=L, the MO question mathoverflow.net/questions/331956/… raises that very question, and has some interesting answers. However, if you can persuade mathematicians that the only true operations mathematicians will ever have access to---in both deed and thought---are the Godelian operations, then you might make headway in getting V=L accepted. However, do you truly believe that the Godelian operations are really all that one can do with infinite collections?

Jesse, for a non-artificial connection between large cardinals and number theory, there is the conjecture that the first row of a Laver table has unbounded period. en.wikipedia.org/wiki/Laver_table

As for advocating pluralism, I'd say my position is a bit more nuanced than that. The business with comprehension failing and On being an uncompleted infinity, lead me to believe (on the level of mathematical abstraction) that set theory is inherently limited to certain contexts (or types, if you will). So, yes, there are many possible universes, for the many possible types of sets.

@JesseElliott Many set theorists admit that the axiom of foundation is just an axiom of convenience for simplicity, limiting one's focus to the well-founded (hereditarily set-like) sets. AC is something different. It is similar to the axioms of union and power set, allowing one a power to construct new sets from old ones by pure assertion; and yet it is somewhat different in its impredicativity. AC is like comprehension in that it asserts an ability to accomplish tasks in the realm of Platonic collections.