User loginNavigation 
Inconsistency Robustness in FoundationsInconsistency Robustness requires repairing mathematical foundations in the face of contradictions that have arisen over and over again. In the Inconsistency Robustness paradigm, deriving contradictions are a progressive development and not â€œgame stoppers.â€ Contradictions can be helpful instead of being something to be â€œswept under the rugâ€ by denying their existence, which has been repeatedly attempted by the Establishment (beginning with some Pythagoreans). Such denial has delayed mathematical development. This article reports how Inconsistency Robustness has recently influenced the foundations of mathematics for Computer Science since the first International Symposium in 2011 continuing a tradition developing the sociological basis for foundations. That mathematics is thought to be consistent by an overwhelming consensus of working professional mathematicians justifies the use of Proof by Contradiction. In addition, Proof by Contradiction can be used to infer the consistency of mathematics by the following simple proof: The selfproof is a proof by contradiction. In order to obtain a contradiction, assume 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. Please note the following points: The above argument mathematically proves the theorem that mathematics is consistent and that it is not a premise of the theorem that mathematics is consistent. However, the proof does not intuitively increase our confidence in the consistency of mathematics because it does not rule out that there might be other proofs in mathematics that result in contradictions. The above theorem means that the assumption of consistency is deeply embedded in the architecture of classical mathematics. The above proof of consistency can be formalized in Direct Logic [Hewitt 2010] (a powerful inference system in which computer systems can reason about their own inferences). Having a powerful system like Direct Logic is important in computer science because computers must be able to carry out all inferences (including inferences about their own inference processes) without requiring recourse to human intervention. Selfproving consistency raises that possibility that mathematics could be inconsistent because of contradiction with the result of GÃ¶del et. al. that if mathematics is consistent, then it cannot infer its own consistency. The resolution is to provide a proper grammar of mathematical sentences so that a fixedpoint operator cannot be used to construct the kind of â€œselfreferentialâ€ proposition used by GÃ¶del in his results by exploiting an untyped grammar of sentences. Selfreferential propositions of the kind used by GÃ¶del do not seem to have any important practical applications. (There is a very weak theory called Provability Logic that has been used for selfreferential propositions coded as integers, but it is not strong enough for the purposes of computer science.) Direct Logic makes use of a typed grammar that prevents the construction of selfreferential sentences using unwanted fixed points. The bottom line is that selfreferential propositions are â€œmonstersâ€ (in the sense of Lakatos) that are ruled about by a proper grammar of sentences for the mathematical foundations of computer science. It is important to note that not having selfreferential propositions does not place restrictions on recursion in computation, e.g., the Actor Model, untyped lambda calculus, etc. A mathematical theory is an extension of mathematics whose proofs are computationally enumerable. For example, group theory is obtained by adding the axioms of groups to Direct Logic along with the requirement that proofs are computational enumerable. If a mathematical theory T is consistent, then it is inferentially undecidable (i.e. there is a proposition Î¨ such that âŠ¬_{T}Î¨ and âŠ¬_{T}Â¬Î¨ (which is sometimes called â€œincompletenessâ€ in classical terminology) because provability in T is computationally undecidable [Church 1936, Turing 1936]. Information Invariance is a fundamental technical goal of logic consisting of the following: This article has become highly controversial and the Establishment has censored (without substantive justification) its publication in electronic archives that are intended to record priority dates for scientific results. Consequently, this article is itself another episode in the ongoing saga of inconsistency robustness in foundations. The article for the above abstract can be found here: Inconsistency Robustness in Foundations By Hewitt at 20140218 21:15  LtU Forum  previous forum topic  next forum topic  other blogs  6077 reads

Browse archivesActive forum topics 
Recent comments
5 days 22 hours ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago