Would it be possible to concoct a "harmful" axiom?

Question

Suppose I run an automated theorem prover. It begins with the axioms of ZFC, and using a random number generator, it proves more theorems, and it runs for two days. At the end of the second day, it halts.

The program then considers all the theorems it proved on the second day (but not the first), and outputs the shortest of these.

Finally, I write a paper proposing the negation of the proved statement as a new axiom of ZFC, based on some "deep intuition" I've had.

People spend lots of time working out the "profound consequences" of this new axiom. I spend lots of time laughing, and it ends up taking 100 years for people to work out that the axiom is inconsistent with ZFC.

Could this ever happen? Do the principles of computational complexity allow it to happen? And if so, what can be done about it? I don't want mathematics infected with harmful axioms.

Edit: The point is, it may be reasonably easy to use a computer to come up with a harmful axiom, but very difficult to use a computer to refute such an axiom.

Answer 1

There are a few problems with this scenario:

1. I doubt there will be much acceptance of a new axiom without useful consequences (e.g. Martin's Axiom has wonderful consequences, so it was accepted). So before people will accept this as a new axiom, you would have to show why this will be a fruitful addition to the current set of axioms of mathematics.

2. I am certain that people will be reluctant to accept axioms from a stranger. There is a lot to work out with the current axioms, and you would probably have to establish a name before a new axiom that you suggest will be accepted.

3. If you are not a stranger to set theorists, and you are in the status where you could propose some new axiom and people will find it interesting immediately, then it is most likely that you have spent the last decade or more working hard on set theory, and proposing a false axiom on purpose would put your life's work into question. Despite mathematicians (and logicians) having a reputation for being crazy, they are not that kind of crazy.

4. Some of the brightest people I know are set theorists. The fact that you used an automated prover does not mean that people won't be able to see right through that and within a few days, or weeks, or months, point out the contradictions.

But sure, you can always suggest anything that you want. The question is whether or not it is going to stick with set theory. And taking the negation of some randomly proved theorem does not seem like a very fruitful proposition. If it won't be useful to begin with (and you would have to supply the first round of usefulness, and it would have to be good), then people won't bother with it.

Answer 2

Perhaps a longish comment, but we do not know if ZFC is itself consistent to begin with. Most set-theorists (if not mathematicians in general) have a strong belief that ZFC is consistent — in part due to the fact that many brilliant mathematicians have not found a contradiction yet — but a belief is all it is.

Could an automated theorem prover come up with a theorem whose negation could not easily be refuted by humans? Most likely, since automated theorem provers can make connections that are not immediately obvious to humans (consider the Robbins Problem which stood open for more than 60 years until William McCune used an automated theorem prover to solve it). Might it take decades of research to discover the inconsistency? Perhaps. Unless, of course, if someone decided to input this all into an automated theorem prover.