User talk:Prof. Carl Hewitt

Please leave any suggestions and comments for me here. Thanks! Carl

Proposals for article on Incompleteness theorem

Criticisms of Gödel's approach to incompleteness theorems

Over the years, sharper and sharper critiques have been developed of Gödel's 1931 incompleteness results to the point that today that they are under very serious doubt by many computer scientists.

Carl (talk) 01:42, 15 August 2016 (UTC)

Wittgenstein

Early on, Wittgenstein correctly noted that Gödel's proposition I'm unprovable. makes mathematics inconsistent:

"Let us suppose [Gödel's writings are correct and therefore] I prove the improvability (in Russell’s system) of [Gödel's proposition I'm unprovable.] P; [i.e., ⊢⊬P where P⇔⊬P] then by this proof I have proved P [i.e., ⊢P]. Now if this proof were one in Russell’s system [i.e., ⊢⊢P] —I should in this case have proved at once that it belonged [i.e., ⊢P] and did not belong [i.e., ⊢¬P because ¬P⇔⊢P] to Russell’s system. But there is a contradiction here! [i.e., ⊢P and ⊢¬P]"

Wittgenstein's criticism pertained to obtaining a contradiction in Russell's system Principia Mathematica which was the system used for Gödel's original article on the incompleteness theorem. Unfortunately, the type system of Principia Mathematica was not up to modern standards. Subsequently, to save his results from Wittgenstein's devastating criticism, Gödel retreated to first-order provability logic, which is inadequate as a mathematical foundation for computer science.

Carl (talk) 02:25, 12 September 2016 (UTC)

Wittgenstein's criticism is objectively wrong, (or, at least recognized as wrong by experts of the field.) "P⇔⊬P" is self-referential, but is not part of the statement of the theorem, nor is that statement in the language discussed, but in the meta-language. If we discuss proofs in theories and languages where "⊬" is in the language, Wittgenstein may have a point. I do not believe that Gödel's proof relates to Russell's system. I have not studied the history of Gödel's proofs ... it's possible that Gödel's original proof really did relate to a system where "⊢" is part of the language, in which case Wittgenstein's note might be valid as to the early proofs, but not as to the later proofs which were more formal. — Arthur Rubin (talk) 03:56, 16 May 2016 (UTC)

Gödel's original proof was indeed for Russell's system Principia Mathematica. Wittgenstein's criticism is not objectively wrong, and it certainly is troublesome that such a simple correct proof leads to contradiction in Principia Mathematica. The problem with the proposition P⇔⊬P is that the type system of Principia Mathematica is insufficient. In proper Mathematics, the proposition P⇔⊬P is not type correct because ⊬P in the definition P⇔⊬P is a proposition of order one greater than the order of P.

Gödel's response to Wittgenstein's criticism was twofold:

1. To insinuate that Wittgenstein was crazy.
2. To retreat into first-order Provability Logic, thereby attempting to save his results. However, Provability Logic is very weak because it is first-order and therefore cannot properly automatize the natural numbers.

All of this is currently a matter of active research. Carl (talk) 13:25, 16 May 2016 (UTC)

It's still probably not mainstream, but if that is correct, it just shows directly that (untyped) PM is inconsistent, not that there is anything wrong with Gödel's approach.

I haven't seen successful attempts to formalize proofs in second-order theories, with something resembling $\vDash \psi \leftrightarrow \vdash \psi$ holding (in the metalanguage). If there is such an approach, Wittgenstein's criticism still not a criticism of Gödel's theorems or proofs, but of the systems in which they are contained.

Some of this is WP:OR on my part, but it seems that Wittgenstein's and Church's criticism is not of Gödel's work, but of the logical systems which allowed his proofs to work. — Arthur Rubin (talk) 17:55, 10 June 2016 (UTC)

Wittgenstein's proof (above) shows that Principia Mathematica is inconsistent if its type theory allows (as Gödel claimed) that Gödel's proposition I'm unprovable. is valid. Consequently, Wittgenstein's criticism directly applies to Gödel's results.

Of course, it is well known that (⊢_$Nat$Ψ)⇒⊨_ℕΨ because the axioms of $Nat$ hold in ℕ. Of course, the converse does not hold.

Carl (talk) 01:32, 15 August 2016 (UTC)

Church

Church critiqued the foundations of logic as follows:

"in the case of any system of symbolic logic, the set of all provable theorems is [computationally] enumerable... any system of symbolic logic not hopelessly inadequate ... would contain the formal theorem that this same system ... was either insufficient [theorems are not computationally enumerable] or over-sufficient [that theorems are computationally enumerable means that the system is inconsistent]...

This, of course, is a deplorable state of affairs...

Indeed, if there is no formalization of logic as a whole, then there is no exact description of what logic is, for it in the very nature of an exact description that it implies a formalization. And if there no exact description of logic, then there is no sound basis for supposing that there is such a thing as logic."

The above critique foreshadowed a new understanding of true but unprovable propositions in the Dedekind/Peano theory of natural numbers. The proposition that "theorems of the theory are computationally enumerable" is unprovable in the Dedekind/Peano theory, but it is true in the standard model.

Carl (talk) 16:29, 4 June 2016 (UTC)

I'm not sure I understand what you quote Church as saying. It seems to me that his thesis is that the fact that the recursion theory incompleteness proof (not, the incompleteness theorem, itself) means that logic is not formalizable. That's not a critique of Gödel's work, but of what Wikipedia might (but apparently does not) call formal logic. It may have a place in another article, but it doesn't seem to me to be a critique of Gödel's incompleteness theorems. — Arthur Rubin (talk) 13:25, 10 June 2016 (UTC)

The Church quotation is relevant to Incompleteness theorems because it led to the discovery of a proposition of the theory $Nat$ that is true in the model ℕ but unprovable in the theory $Nat$, namely, "the proofs of $Nat$ are computationally enumerable." Carl (talk) 05:39, 11 June 2016 (UTC)

I think there there may be a map-territory problem here. Your comment (not attributed to Church) that $\mathbb {N} \Vdash \operatorname {Th} (PA){\text{ is r.e.}}$, but $PA\nvdash \operatorname {Th} (PA){\text{ is r.e.}}$ is not incorrect; PA cannot state $\operatorname {Th} (PA){\text{ is r.e.}}$. I think you'll find that if you formalize Th(PA) in PA, you'll find that there is a specific partial recursive function f such that $PA\vdash \operatorname {Th} (PA)=\operatorname {Domain} (f)$ (or, to be precise, that statement from second-order PA corresponds to a statement in first-order PA which is provable in PA.) — Arthur Rubin (talk) 14:05, 10 June 2016 (UTC)

Church was dealing with the classical mathematics of his day, namely, the Dedekind categorical theory of the natural numbers $Nat$, which can state (but cannot prove) that the proofs of $Nat$ are computationally enumerable. Carl (talk) 23:39, 14 August 2016 (UTC)

Chaitin

Gregory Chaitin criticized Gödel's approach to the incompleteness theorem for being superficial and lacking insight. For example in the BBC scientific documentary “Dangerous Knowledge”, Chaitin said that in his considered judgment,

"[Gödel’s argument for incompleteness] was too superficial. It didn't get at the real heart of what was going on. It was more tantalizing than anything else. It was not a good reason for something so devastating and fundamental. It was too clever by half. It was too superficial. [It was based on the clever construction] I'm unprovable. So what? This doesn't give any insight how serious the problem is."

The thesis of Chaitin's criticism above is that incompleteness is a fundamental issue for formal systems that is not adequately addressed by Gödel’s proof based on his proposition I'm unprovable. In his 2007 book Chaitin wrote: "You see, the real problem with Gödel's proof is that it gives no idea how serious incompleteness is."

Chaitin's criticism is supported in that important properties of the natural numbers (such as Goodstein's theorem, Paris–Harrington theorem, etc.) cannot be proved in the first-order version of the Dedekind/Peano axioms for natural numbers. These undecidable theorems are more intuitive than Gödel’s proposition I'm unprovable. Chaitin's criticism was also supported by the fact that even Gödel himself agreed that the subsequent proof of incompleteness by Church/Turing based on computational undecidability was fundamental in proving that there is no total recursive procedure that can decide provability of a proposition of the Peano/Dedekind theory $Nat$ of natural numbers. There must be an inferentially undecidable proposition for $Nat$ because otherwise provability of any proposition could be computationally decided by enumerating all theorems until the proposition or its negation occurs. However, Gödel, Church, and Turing continued to believe in the importance of Gödel’s proof based on his proposition I'm unprovable.

Of course, there are are important properties of the natural numbers (such as Goodstein's theorem, Paris–Harrington theorem, etc.) that cannot be proved in the first-order version of the Dedekind/Peano axioms for natural numbers.

Carl (talk) 17:00, 1 July 2016 (UTC)

Hewitt

Hewitt noted that since Godel's I'm unprovable is not a valid proposition of strongly typed mathematics, the challenge became to find other propositions that are true but unprovable.

The theory $Nat$ was first categorically automatized by Richard Dedekind, which means that up to a unique isomorphism there is just one mathematical model of $Nat$ which is denoted by ℕ. The following proposition is true in the model ℕ, but unprovable in $Nat$ by an argument due to Alonzo Church:

       Proofs of $Nat$ are computationally enumerable. 

In other words, both of the following hold

• ⊨_ℕ ProofsComputationallyEnumerable_$Nat$
• ⊬_$Nat$ ProofsComputationallyEnumerable_$Nat$

Note that the above theorem is much stronger than the one claimed by Gödel because the theory $Nat$ is much stronger than any first-order logic axiomatization of the natural numbers.

Furthermore, Hewitt pointed out that the current common understanding is incorrect that Gödel proved “Mathematics cannot prove its own consistency, if it is consistent.” However, the formal consistency of mathematics can be proved by a simple argument using standard rules of Mathematics including the following:

• rule of Proof by Contradiction, i.e., (¬Φ⇒(Θ∧¬Θ))├Φ
• rule of Theorem Use (a theorem can be used in a proof), i.e., (├Φ)├Φ [Theorem Use is a fundamental rule used in mathematical proofs going back at least to Euclid.]

Formal Proof. By definition, Consistent⇔¬∃[Ψ]→├(Ψ∧¬Ψ). By Existential Elimination, there is some proposition Ψ₀ such that ¬Consistent⇒├(Ψ₀∧¬Ψ₀) which by Theorem Use and transitivity of implication means ¬Consistent⇒(Ψ₀∧¬Ψ₀). Substituting for Φ and Θ, in the rule for Proof by Contradiction, it follows that (¬Consistent⇒(Ψ₀∧¬Ψ₀))├Consistent. Thus, ├Consistent.

The above theorem means that consistency is deeply embedded in the architecture of classical mathematics. Please note the following points: The above argument formally mathematically proves the theorem that mathematics is consistent and that it is not a premise of the theorem that mathematics is consistent. Classical mathematics was designed for consistent axioms and consequently the rules of classical mathematics can be used to prove consistency regardless of the axioms, e.g., Euclidean geometry.

By formally consistent, it is meant that a consistency is not inferred. The proof is remarkably tiny consisting of only using proof by contradiction and soundness. In fact, it is so easy that one wonders why this was overlooked by so many great logicians in the past. The proof is also remarkable that it does not use knowledge about the content of mathematical theories (plane geometry, integers, etc.). The proof serves to formalize that consistency is built into the very architecture of classical mathematics. However, the proof of formal consistency does not prove constructive consistency, which is defined to be that the rules of Classical Direct Logic themselves do not derive a contradiction. Proof of constructive consistency requires a separate inductive proof using the axioms and rules of inference of Classical Direct Logic. The upshot is that, contra Gödel, there seems to be no inherent reason that mathematics cannot prove constructive consistency of Classical Direct Logic (which formalizes classical mathematical theories). However, such a proof is far beyond the current state of the art.

The consistency theorem contradicts [Raatikainen 2015] which states: “For any consistent system [formal system] F within which a certain amount of elementary arithmetic can be carried out [for example, the formal system $Nat$], the consistency of F cannot be proved in F itself.” where “Roughly, a formal system is a system of axioms equipped with rules of inference, which allow one to generate new theorems. The set of axioms is required to be finite or at least decidable, i.e., there must be an algorithm (an effective method) which enables one to mechanically decide whether a given statement is an axiom or not. If this condition is satisfied, the theory is called 'recursively axiomatizable', or, simply, 'axiomatizable'. The rules of inference (of a formal system) are also effective operations, such that it can always be mechanically decided whether one has a legitimate application of a rule of inference at hand. Consequently, it is also possible to decide for any given finite sequence of formulas, whether it constitutes a genuine derivation, or a proof, in the system—given the axioms and the rules of inference of the system.” and “A formal system is consistent if there is no statement such that the statement itself and its negation are both derivable in the system.” The reason for the contradiction is that [Raatikainen 2015] implicitly assumed that a formal system must be untyped and consequently have Y fixed points for propositions that can be used to construct Gödel's proposition “I'm unprovable.”

A bone of contention between some philosophers and computer scientists is strong typing of propositions. Computer scientists want strong typing for clarity, efficiency, groundedness, and blocking known mathematical paradoxes including those resulting from allowing I'm unprovable. Conservative philosophers want to stick to untyped first-order propositions allowing use of the Y fixed point construction to create the proposition I'm unprovable. Many computer scientists do not see an practical benefit of allowing propositions like I'm unprovable.

Carl (talk) 01:02, 15 August 2016 (UTC)

We all know that, if a theory is inconsistent, then it is not sound. (There may be even shorter proofs than the one you gave above, but not by much.) In classical logic, that is used to note that we cannot guarantee a theory is sound. In your interpretation, it's the other way around: you seem to assume soundness, and use it to prove consistency. — Arthur Rubin (talk) 05:25, 10 June 2016 (UTC)

Soundness is a fundamental assumption used in proofs going back at least to Euclid. In proof theory, soundness, i.e., (├Φ)⇒Φ, says that a theorem can be used in a proof. In model theory, soundness for the theory $Nat$ (first categorically automatized by Richard Dedekind) says (⊢_$Nat$Ψ)⇒⊨_ℕΨ, i.e., if a proposition is provable in the theory $Nat$, then it is true in the model ℕ.

Carl (talk) 23:25, 14 August 2016 (UTC)

In "traditional" logic, you have stated soundness correctly, but it is nothing like "a theorem can be used in a proof"; that would be more like ( T, φ |- ψ) and ( T |- φ) implies ( T |- ψ) . As for Nat, you have stated N is the only model of Nat, but N |= φ does not imply Nat |- φ. If so, this is a clear failure of the completeness theorem, which is an even more essential part of proof theory than soundness. — Arthur Rubin (talk) 21:45, 10 September 2016 (UTC)

In the above I have clarified, that the rule of Theorem Use (which goes back at least to Euclid) is sufficient for mathematics to prove its own consistency, that is, (├Φ)├Φ.

Unfortunately, you got it wrong in your statement above by confusing the hypothesis and conclusion of my correct statement: (⊢_$Nat$Ψ)⇒⊨_ℕΨ. Of course, the converse of the correct statement does not hold, which was first validly proved by Church. (Gödel's proof is invalid because his proposition I'm unprovable. cannot be validly formalized in mathematics on pain of contradiction in mathematics.)

Categoricity is something else again: all models that satisfy the Dedekind axioms for the natural numbers $Nat$ are isomorphic to ℕ.

Carl (talk) 15:08, 12 September 2016 (UTC)

To be precise, incompleteness theorems are uninteresting without a completeness theorem. (I'll adjust wording and links sometime tomorrow.) — Arthur Rubin (talk) 01:33, 11 September 2016 (UTC)

It would be even better if you state a correct version of the incompleteness theorem for $Nat$:

• ⊨_ℕ ProofsComputationallyEnumerable_$Nat$
• ⊬_$Nat$ ProofsComputationallyEnumerable_$Nat$

Note that the above incompleteness theorem is much more powerful than the first-order result (incorrectly claimed) in the current Wikipedia article because ⊬_$Nat$ is much stronger than

⊬_{$FirstOrderNaturalNumbers$}

Carl (talk) 02:30, 12 September 2016 (UTC)

Proposals for article on Ordinal numbers

The article on Ordinal numbers is significantly obsolete and inaccurate.

More up to date information can be found here: Inconsistency Robustness in Foundations: Mathematics self proves its own formal consistency and other matters

Carl (talk) 23:45, 21 October 2016 (UTC)

Proposals for articles on Actor Model

The articles on the Actor Model are significantly obsolete and inaccurate.

More up to date information can be found here:

• Actor Model of Computation for Scalable Robust Information Systems: One computer is no computer in IoT
• ActorScript™ extension of C#®, Java®, Objective C®, JavaScript®, and SystemVerilog using iAdaptive™ concurrency for antiCloud™ privacy and security: One computer is no computer in IoT

Carl (talk) 23:45, 21 October 2016 (UTC)

Proposals for article on Logic Programs

The article on Logic programs is significantly obsolete and inaccurate.

More up to date information can be found here: Inconsistency Robustness for Logic Programs

Carl (talk) 23:58, 21 October 2016 (UTC)

ANI notice

There is currently a discussion at Wikipedia:Administrators' noticeboard/Incidents regarding an issue with which you may have been involved. Thank you. Binksternet (talk) 05:56, 13 November 2016 (UTC)

November 2016

You have been blocked indefinitely from editing for abuse of editing privileges, per [1]. If you think there are good reasons why you should be unblocked, you may request an unblock by first reading the guide to appealing blocks, then adding the following text to the bottom of your talk page: {{unblock|reason=Your reason here ~~~~}}.

I think it is clear that you are reverting to the behaviours that led to your original sanctions. I do not think you are actually able to work productively with people who do not accept you as arbiter and authority in your field. You may even be right about the content matters, but Wikipedia works by collaboration and credentialled expertise is explicitly not recognised as permitting anybody to "win" in any dispute. Guy (Help!) 09:11, 13 November 2016 (UTC)

It seems unfortunate that Wikipedia is not more devoted to truth. Instead, it seems to be governed by the The Cult of the Amateur. 50.0.72.20 (talk) 22:57, 1 May 2017 (UTC)