Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

AIC Seminar Series

Mathematics self-proves its own Consistency (contra Gödel et. al.)

Carl HewittInternational Society for Inconsistency Robustness[Home Page]

Notice:  Hosted by Richard Waldinger

Date:  Tuesday, April 24th 2012 at 4:00pm

Location:  EJ228 (SRI E building)  (Directions)


The consistency of mathematics has long been of concern. Using self-referential propositions, Gödel et. al. proved that if mathematics is consistent, it does not prove its own consistency. Regardless, this paper presents a simple non-constructive self-proof of consistency: The self-proof is a proof by contradiction. Suppose to obtain an inconsistency that mathematics is inconsistent. Then there is some proposition Φ such that ⊢Φ and ⊢¬Φ. Consequently, both Φ and ¬Φ are theorems that can be used in the proof to produce an immediate contradiction. Therefore mathematics is consistent.

Of course, the above proof does not show that mathematics is really consistent, i.e., that is impossible to infer an inconsistency using the inference rules because the proof is valid even if mathematics is inconsistent. In fact, self-proving consistency raises that possibility that mathematics could be inconsistent because of contradiction with the result of Gödel et. al. One resolution is not to have self-referential propositions. This can be achieved by carefully arranging the rules for propositions so that self-referential propositions cannot be constructed. Fortunately, self-referential propositions do not seem to have any important practical applications.

The above proof of consistency is carried out in Direct Logic [Hewitt 2011] that is a powerful inconsistency-robust inference system that is its own metasystem. Having such a system is important in computer science because computers must be able to carry out all inferences (including inferences about their own inference processes) without always relying on humans. A tradeoff is that in return for having such a powerful inference system, self-referential propositions are not allowed.

   Note for Visitors to SRI

Please arrive at least 10 minutes early as you will need to sign in by following instructions by the lobby phone at Building E (or call Wilma Lenz at 650 859 4904, or Eunice Tseng at 650 859 2799). SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the parking lots off Fourth Street. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page. There are two entrances to SRI International located on Ravenswood Ave. Please check the Building E entrance signage.

SRI International
©2018 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy