Lambda the Ultimate

"Preface" Carl Hewitt

Part 1. Mathematical Foundations

1. "Formalizing common sense reasoning for scalable inconsistency-robust information coordination using Direct Logic Reasoning and the Actor Model" Carl Hewitt

2. "Inconsistency robustness in foundations: Mathematics self proves its own consistency and other matters" Carl Hewitt

3. "Inconsistency: Its preset impacts and future prospects" John Woods

4. "Two sources of explosion" Eric Kao

Part 2. Software Foundations

1. "Actor Model of computation: Scalable robust information systems" Carl Hewitt

2. "Inconsistency robustness for logic programs" Carl Hewitt

3. "ActorScript extension of C#, C++, Java, Objective C, JavaScript, and SystemVerilog using iAdaptive concurrency for antiCloud privacy and security" Carl Hewitt

Part 3. Applications

1. "Some types of inconsistency in legal reasoning" Anne Gardner

2. "Rules versus standards: Competing notions of inconsistency: Robustness in the Supreme Court and Federal Circuit" Stefania Fusco and David Olson

3. "Politics and pragmatism in scientific ontology construction" Mike Travers

4. "Modelling ungrammaticality in a precise grammar of English" Dan Flickinger

5. "The singularity is here" Fanya S. Montalvo

6. "Biological responses to chemical exposure: Case studies in how to manage ostensible inconsistencies using the Claim Framework" Catherine Blake

7. "From inter-annotation to intra-publication inconsistency" Alaa Abi Haidar, Mihnea Tufi, and Jean-Gabriel Ganascia

Index

It is good that there's more voices we can study around this. If anybody ends up having the money and time to read through it, do please summarize here, in particular: how useful the book is at explicating the Hewitt's koans. It does seem like there are other people out there who Get It so hopefully their writing can transmit it.

I've recently been following Dr. Hewitt's posts on arithmetic proving its consistency, Gödel not having a proper (typed) means of constructing sentences, and therefore the admission of fixpoints essentially smuggling inconsistency into arithmetic. I'm in the process of preparing a formal logic workshop for Scala World as a kind of "pre-Curry-Howard" effort, I came across this section in Logical Labyrinths:

FIXED POINTS

Underlying the proofs of Theorem GT (Gödel, With Shades of Tarski) and Theorem T (Tarski) is a principle that is very important in its own right. First, a definition. A sentence S is called a fixed point of a predicate H iff the following condition holds: S is true if and only if H(n) is true, where n is the Gödel number of S. Thus a fixed point of H is a sentence S_n such that H(n) is true iff S_n is true.

THEOREM F₁ (FIXED POINT THEOREM). In any system satisfying condition G₁, each predicate of the system has a fixed point.

PROBLEM 27.11. Prove the Fixed Point Theorem.

PROBLEM 27.12. Next, show how the Fixed Point Theorem greatly facilitates the proofs of Theorems T and GT.

Fixed points, diagonalization and self-reference all play key roles not only in the works of Gödel and Tarski, but also in the field of recursion theory (a fascinating subject!) and in the field known as combinatory logic (an equally fascinating field).

So it would seem that Dr. Smullyan, at least, is sounding some of the same notes as Dr. Hewitt, albeit not claiming the reasoning is unsound. In my opinion, this requires more investigation, which is why I'm prioritizing reading Dr. Hewitt's paper highly.

Raould,

LtU archives have extensive discussions of the invalidity of the Gödel/Smullyan writings on incompleteness because types mean the nonexistence of the Y fixed point operator.

There is extensive discussion here.