User loginNavigation 
Continuation of Discussion: "Mathematics selfproves its own Consistency (contra GÃ¶del et. al.)"DRUPL limitations truncated previous ongoing discussion. So I have reposted here. BTW, I would like to thank LtU for previous discussion that was very helpful in improving the current version. Some readers might be interested in the following abstract from Mathematics selfproves its own Consistency: Mathematics selfproves its own Consistency (contra GÃ¶del et. al.) Carl Hewitt http://carlhewitt.info That mathematics is thought to be consistent 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. Suppose to obtain a contradiction, 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. The above theorem means that the assumption of consistency is deeply embedded in the structure of classical mathematics. The above proof of consistency is carried out in Direct Logic [Hewitt 2010] (a powerful inference system in which theories 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 not to allow selfreferential propositions that are used in the proof by GÃ¶del et. al. that mathematics cannot selfprove its own consistency. This restriction can be achieved by using type theory in the rules for propositions so that selfreferential propositions cannot be constructed because fixed points do not exist. Fortunately, selfreferential propositions 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.) It is important to note that disallowing selfreferential propositions does not place restrictions on recursion in computation, e.g., the Actor Model, untyped lambda calculus, etc. The selfproof of consistency in this paper does not intuitively increase our confidence in the consistency of mathematics. In order to have an intuitively satisfactory proof of consistency, it may be necessary to use Inconsistency Robust Logic (which rules out the use of proof by contradiction, excluded middle, etc.). Existing proofs of consistency of substantial fragments of mathematics (e.g. [Gentzen 1936], etc.) are not Inconsistency Robust. 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. 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â€) because provability in T is computationally undecidable [Church 1936, Turing 1936]. Information Invariance is a fundamental technical goal of logic consisting of the following: 1. Soundness of inference: information is not increased by inference 2. Completeness of inference: all information that necessarily holds can be inferred Direct Logic aims to achieve information invariance even when information is inconsistent using inconsistency robust inference. But that mathematics is inferentially undecidable (â€œincompleteâ€) with respect to Î¨ above does not mean â€œincompletenessâ€ with respect to the information that can be inferred because it is provable in mathematics that âŠ¬_{T}Î¨ and âŠ¬_{T}Â¬Î¨.
The full paper is published at the following location: By Hewitt at 20131015 23:45  LtU Forum  previous forum topic  next forum topic  other blogs  6786 reads

Browse archivesActive forum topics 
Recent comments
49 min 11 sec ago
14 hours 32 min ago
15 hours 45 min ago
15 hours 56 min ago
16 hours 10 min ago
16 hours 38 min ago
1 day 2 hours ago
1 day 5 hours ago
2 days 3 hours ago
4 days 1 hour ago