Continuation of Discussion: "Mathematics self-proves its own Consistency (contra Gödel et. al.)"

DRUPL limitations truncated previous ongoing discussion. So I have re-posted 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 self-proves its own Consistency:

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

                             Carl Hewitt

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 self-proof 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.

Self-proving 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 self-referential propositions
that are used in the proof by Gödel et. al.
that mathematics cannot self-prove its own consistency.
This restriction can be achieved by using type theory
in the rules for propositions
so that self-referential propositions cannot be constructed
because fixed points do not exist. 
Fortunately, self-referential propositions
do not seem to have any important practical applications.
(There is a very weak theory called Provability Logic
that has been used for self-referential propositions coded as integers,
but it is not strong enough for the purposes of computer science.) 
It is important to note that disallowing self-referential propositions
does not place restrictions on recursion in computation,
e.g., the Actor Model, untyped lambda calculus, etc.

The self-proof 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:
Mathematics self-proves its own Consistency

Interactive Parsing Theory


I've posted here in the past and just had a few questions about the basics of parsing and perhaps wanted a bit of insight on parsing theory.

I'm currently writing a parser compiler, to better understand the formal side of parsing, and into that I hand-wrote the grammar description language's parser. One of the major things I've learned through this is how very little I really know now and knew when I started.

In the general case, when parsing the full file you begin from the start rule, and go from there, that much is pretty basic. The parts I get a bit hazy on are how to handle partial parses when faced with interactive environments, such as the user typing the text into Visual Studio and integrating your parser infrastructure into the Visual Studio Extensibility. The current method I use involves parsing the entire thing every time, with a asynchronous delay kicked off to pause each time a key is pressed, so it's not parsing everything literally every key press. The major question I have is how to merge the parse trees and isolate the impact of a change to the concrete/abstract tree that results from the user's text.

Is there research based off of interactive parsing I could look at to get an idea?

In the future I want to understand this concept well enough to automate its integration into the project I'm writing now, even if it's in the second or third iteration. I have a feeling it's complicated, perhaps more than I'm thinking now.

Insight is very welcome.

Also note to people posting links to published documents: I don't have any subscriptions to any journals/publication websites, so it might be difficult to follow if such sources are referenced since they usually request a monetary fee for retrieving their data.