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)

An open letter 📨 to Prof. Carl Hewitt

Dear Prof. Carl Hewitt,

Well let me start off my saying that I genuinely do believe that Wikipedia can benefit from having your expertise around and as no-one bothered to tell you how to appeal I would like to leave this rough concept of an idea here and you can see yourself which one applies to you and should read it prior to appealing.

It appears that you have been blocked.
Please read the guide to appealing blocks.
* If you are currently unable to access your talk page you may request an unblock via the Unblock Ticket Request System or the #wikipedia-en-unblock connect chat channel.
* Checkuser and Oversight blocks may be appealed to the Arbitration Committee.
* If you were blocked by Jimbo Wales then you may appeal directly to him or the Arbitration Committee.
* If this is a Sockpuppet then you should confess your main account (or IP) now so you may receive a reduced penalty.
* If you have been blocked for a username violation then you can simply create or request a new account or request to be renamed here or at #wikimedia-rename connect, if however the username was made in bad faith then first request a rename and then you may appeal the block; further reading Wikipedia:Changing username.
* If you have been blocked for adding promotional material or spam then please read about our policy on this before requesting an unblock.
* If your options are currently still unclear then please read how to appeal a block.

That aside however I would also like to note that just because you have been blocked on English Wikipedia and if you feel that this community is less open to experts then I would like to point you to German Wikipedia where they have whole panels for people who are experts in their fields and take the opinion of experienced and trusted experts such as yourself in high regard, you may contact the German Wikipedia at their embassy here if you’re interested in sharing your ideas with the German-speaking community, I must however state that all ideas are open to scrutiny. I would advise you to check your options out there are German-speaking Wikipedians take people such as yourself in high regard and any sources and knowledge you are willing to provide tends to be welcomed with open arms there. (the “embassy” of German Wikipedia accepts English)

Concerning this comment you left here:

“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)”

Well, this is simply not true, Wikipedia takes high account of good educational resources and is in no way a playground for “amateurs”, however a requirement is that when you improve the encyclopedia that you are willing to collaborate and are open to criticism, if this criticism is well founded or not should be debated.

I hope that after reading this that you would be willing to appeal your block (after familiarising yourself with all the policies and guidelines, of course), and I hope that the reviewing administrators can see the benefits of having someone like you return to contributing to this community as I can.

P.S.

This letter was drafted on August 18th, 2017 but as you can see I’ve been blocked for quite a long time (just look at my signature ✍🏻 why), by the way if you're interested in sharing pictures 📷 of yourself and things that interest you as well as sharing your written works, concepts, and drafts for the whole world to see then I would advise to go tự Wikimedia Commons and upload everything you want to publicise there, this community (and many others) could greatly benefit from people like you and I hope that you have not given up on it.

P.P.S.

The above “Blockbox” is just a (rough) draft which I am planning to propose in the future, if (or when) you would get unblocked and the box helped you in any way then please tell me so on my talk page. 😉

Sent from my Microsoft Lumia 950 XL with Microsoft Windows 10 Mobile 📱. --Donald Trung (Talk 💬) (Sockpuppets 🎭) (Articles 📚) 20:06, 6 February 2018 (UTC)

This user's unblock request has been reviewed by an administrator, who declined the request. Other administrators may also review this block, but should not override the decision without good reason (see the blocking policy).

Prof. Carl Hewitt (block log • active blocks • global blocks • contribs • deleted contribs • filter log • creation log • change block settings • unblock • checkuser (log))

---

Request reason:

Your reason here "Restore edits to this talk page that were deleted so that other editors may discuss them."

Decline reason:

I am declining your unblock request because it does not address the reason for your block, or because it is inadequate for other reasons. To be unblocked, you must convince the reviewing administrator(s) that

• the block is not necessary to prevent damage or disruption to Wikipedia, or
• the block is no longer necessary because you
  1. understand what you have been blocked for,
  2. will not continue to cause damage or disruption, and
  3. will make useful contributions instead.

Please read the guide to appealing blocks for more information. Yamla (talk) 20:15, 13 February 2018 (UTC)

---

If you want to make any further unblock requests, please read the guide to appealing blocks first, then use the {{unblock}} template again. If you make too many unconvincing or disruptive unblock requests, you may be prevented from editing this page until your block has expired. Do not remove this unblock review while you are blocked.

If you are unclear why I declined your unblock, please ask and I'll be happy to clarify. You are welcome to make a new request, addressing the reason for your block, and another admin will be happy to review. --Yamla (talk) 20:18, 13 February 2018 (UTC)

No problem. Anyone interested in the issues involved in the material that was censored from this page can go to my website which is here: Homepage of Prof. Carl Hewitt

With respect to your questions:

1. I was blocked because I fell into a trap into getting into a conflict. Sorry that I didn't understand the protocol. Wikipedia newbies should be warned against falling for this trap.
2. I did not intend to cause damage or disruption. My purpose in contributing to Wikipedia is to further the spread of knowledge.
3. I have made many useful contributions including being the primary author of the article Actor Model as well as other articles. Unfortunately, the article on the Actor Model has now become seriously obsolete. Also, several articles on mathematical logic are also obsolete including the following: First-order logic, Higher-order logic, Incompleteness theorems, Lambda calculus, Ordinal number, and Set theory. See the following article: Strong Types in Direct Logic.

Carl (talk) 19:18, 14 February 2018 (UTC)