9
$\begingroup$

In discussion about the consistency of large cardinals, a justification which occasionally appears is that despite years of work, no inconsistency has currently been discovered. For example, here are two occurrences of this argument:

"My belief in their consistency is based on the fact that very smart people, like Jack Silver, have looked seriously for inconsistencies and haven't found any.)" - Andreas Blass, in a MathOverflow answer to question "Reasons to believe Vopenka's principle/huge cardinals are consistent".

"But is $\mathrm{ZFM}$ [$\mathrm{ZF}$ plus 'there exists a measurable cardinal'] consistent? ... It seems to be consistent in the sense that the set theorist's use of $\mathrm{ZFM}$ has not led to any inconsistencies." - Harvey Friedman, in "The Incompleteness Phenomena", in Proceedings of the AMS Centennial Symposium (1988, p. 67).

My question is, has there ever been a computer search run for an inconsistency in some set theory (whether with or without choice) with large cardinals. If not, is there a generally accepted reason for why such a search is not worth the effort of implementing it?

I know such projects have been later proposed by Friedman, e.g. in his manuscript "Computational Confirmation of Consistency" (2018), although these computer searches would be on graph-theoretic propositions he has proven equivalent to consistency of large cardinals, and not on proofs from $\text{ZF(C)+large cardinals}$ themselves.

Randall Dougherty's paper "Critical points in an algebra of elementary embeddings, II" (1995) contains the claim "this may be the first serious example of computer-aided research in the theory of large cardinals", but as far as I know this computer experimentation was not a search for an inconsistency.

Improve this question
$\endgroup$
5
  • 9
    $\begingroup$ The conventional wisdom is that the space of proofs is so vast that an open-ended computer search for a proof of any particular theorem is totally infeasible (a proof of inconsistency is a proof of the theorem "false"). So people are unlikely to have attempted such a search, for the same reason they are not searching for proofs of (say) the Riemann Hypothesis. $\endgroup$
    – Alex Kruckman
    Commented Sep 7 at 22:41
  • 12
    $\begingroup$ It seems to me that any proposal for such a search should first be checked on a known inconsistency, for example Reinhardt cardinals with ZFC. $\endgroup$
    – Andreas Blass
    Commented Sep 7 at 23:48
  • 4
    $\begingroup$ The situation could change if someone could come up with an idea for a targeted search for a proof of "false". There have been a few successes in automated theorem proving, when the search space is carefully designed. In today's era of machine learning, one could imagine training a learning algorithm on a corpus of inconsistent systems. The difficulty here might be coming up with a sufficiently large and rich corpus of inconsistent systems for the machine learning system to sink its teeth into. $\endgroup$
    – Timothy Chow
    Commented Sep 8 at 3:35
  • 7
    $\begingroup$ There’s a rumor that some top set theorists have actually found inconsistencies, but the arguments are so intricate that they can be mined for proofs of other results enough to make a long successful academic career. $\endgroup$
    – Monroe Eskew
    Commented Sep 8 at 5:04
  • 1
    $\begingroup$ @MonroeEskew Obligatory xkcd comic. $\endgroup$
    – Timothy Chow
    Commented Sep 8 at 12:59

0

Reset to default

You must log in to answer this question.