User talk:Prof. Carl Hewitt

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

Suggestion for Wikipedia Policy on Authoritative (sometimes called "Reliable") Sources

What you might mean by "Authoritative" does not seem similar to what we mean by "Reliable". — Arthur Rubin (talk) 03:58, 16 May 2016 (UTC)

"Authoritative" is not as apriori judgmental of content as "reliable" which has intimations of being "true". "Authoritative" may be more suitable for Wikipedia because it does not as strongly take sides in content disputes. Carl (talk) 13:35, 16 May 2016 (UTC)

Coming back to this, "authoritative" may be a better word choice than "reliable". A problem, is that, although "reliable" has the connotation of "truth", "authoritative" seems to have the connotation that it assets its importance/significance, rather than it actually being important or significant. — Arthur Rubin (talk) 21:58, 28 June 2016 (UTC)

You have a good point! Being "authoritative" must be determined on a case by case basis.

As I have said elsewhere on Wikipedia, Being authoritative means having authority. Dijkstra's letter the editor "Go-to statement considered harmful" proved to be extremely authoritative because of subsequent discussion and reaction in CACM and subsequent authoritative publications. There is general consensus in computer science that Dijkstra's letter proved to be "authoritative" but it would be incorrect to say that the letter is "reliable."

Carl (talk) 19:16, 2 July 2016 (UTC)

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)

archiving content

you shouldn't particularly be erasing comments (yours or others) from your talk page; it's against policy...it's not about not liking how a conversation goes and wanting to start afresh...the reason being it could be of note to other editors who interact with you in the future for the purpose of improving Wikipedia articles...you also shouldn't be renaming other people's thread titles...this isn't a facebook or myspace page; it's all in place solely for working on Wikipedia articles....I may revert back some of what you erased..68.48.241.158 (talk) 02:05, 8 May 2016 (UTC)

Content should be archived that is not on point with specific suggestions for improving the proposals on this page. Editors are welcome to assist in archiving content that is not specifically on point. Carl (talk) 14:15, 8 May 2016 (UTC)

everything was substantive/on point...you can erase personal attacks or collapse off point discussion...you can also archive old discussion...which I don't think you've actually done...where is the archive you created? I think you've just erased things...68.48.241.158 (talk) 14:47, 8 May 2016 (UTC)

Being on point in this case is means making specific suggestions for improving a proposal for a change in a Wikipedia article. The archive is in the usual place as a subpage of this page. Of course, I may have made errors in archiving, which editors are free to correct. Carl (talk) 14:55, 8 May 2016 (UTC)

I was substantively discussing your proposal for additional content, of course..68.48.241.158 (talk) 01:26, 9 May 2016 (UTC)

You need to make specific suggestions for improving the proposals together with arguments for your specific suggestions. Carl (talk) 01:56, 9 May 2016 (UTC)

it is perfectly acceptable to substantively propose only that your proposals aren't yet proper for the article..(ie I'm not required to try to make your proposals better)68.48.241.158 (talk) 02:14, 9 May 2016 (UTC)

The purpose on this talk page is to improve proposals for correcting articles. You can object to the proposals (without making constructive suggestions) on the talk page of the article when a proposal is actually on the talk page of an article. Carl (talk) 02:26, 9 May 2016 (UTC

that's not really what the purpose of this talk page is (or any talk page is)...you can learn what the purpose of a talk page is by reading the policy articles about it...(you can't unilaterally declare what the purpose of your talk page is)...however, I don't mind only engaging you on the article talk page...all I was doing was taking the time to pay attention to your thoughts..68.48.241.158 (talk) 02:38, 9 May 2016 (UTC)

Editors are perfectly welcome to make constructive suggestions for improving the proposals on this talk page so that the proposals can be improved. Carl (talk) 02:42, 9 May 2016 (UTC)

For what it's worth, the anon is not exactly correct. You are allowed to remove material from your talk page (provided you also remove all later replies, including your own), but it is not encouraged, even if you (correctly or incorrectly) think the comments are not on point. The only entries you are encouraged to remove from your, or any, talk page are violations of WP:BLP, WP:COPYVIO, and perhaps WP:NPA.

However, you are also incorrect: the purpose of the talk page includes discussion of whether the material on the talk page is proper. This is not a strongly typed environment. We don't have [[Talk:User talk:Prof Carl Hewitt]] (except in rare situations, where a talk page is protected, such as Talk:Carl Hewitt, we might have an unprotected Talk:Carl Hewitt/Talk). In general, though, proposals should be made on pages such as User:Prof. Carl Hewitt/Incompleteness, with discussion of the proposal (including comments that it is not ready for implementation) in User talk:Prof. Carl Hewitt/Incompleteness. — Arthur Rubin (talk) 13:42, 10 June 2016 (UTC)

It would be great if we could keep discussions of proposals on this page on how to improve articles organized in some fashion. To do this, it is necessary to archive old and irrelevant comments so that discussion can proceed in an organized way. I am creating User talk:Prof. Carl Hewitt/archive/incompleteness as a place where editors can archive old and irrelevant discussion. Of course, none of the proposals on this page are ready for implementation. When a proposal is ready for consideration for implementation, it should be placed on the talk page of the article. Carl (talk) 17:56, 10 June 2016 (UTC)

Edit requests for article Carl Hewitt

Hi Mr. Hewitt, I've moved your edit request into your sandbox User:Prof. Carl Hewitt/sandbox, which is outside the article namespace, and which you can freely edit. If you have a working draft in the sandbox, you can consider re-posting an edit request with a link to your sandbox for an editor to look into. I hope this helps! Thanks. — Andy W. (talk · ctb) 01:25, 14 June 2016 (UTC)

Thanks! I moved to requests to User:Prof. Carl Hewitt/EditRequestsForArticleCarlHewitt to avoid confusion about "sandbox". Others are welcome to improve the edit requests and to coordinate with other edit requests for the the article Carl Hewitt. Carl (talk) 20:58, 14 June 2016 (UTC)

Paraconsistent Logic

Dear Prof. Hewitt,

In the interest of the encyclopedia, I am ordering Hewitt & Woods 2015 for myself. My personal interest is in discovering the relationship of your work to that of Norman Foo 1994 "Convex Predicates and Induction". Foo lived 1943-2015. Foo cites Gardenfors 1990. If no one beats me to it, I could be another non-COI editor for the article on paraconsistent logic. If I turn out to be the only other editor for this effort, please be patient while I work through your material. Or, if others pop up, we could all work together.

Ancheta Wis   (talk | contribs) 13:04, 27 August 2016 (UTC)

Thanks for ordering the book and the link to Foo's article.

You should also note that CBM has recently constructively contributed to this article.

Carl (talk) 14:46, 27 August 2016 (UTC)