What I get on direct logic

gistfile1.md

Disclaimer: don't read this unless you are already interested in Carl Hewitt's direct logic.

Carl Hewitt's Direct Logic is a strange thing, if it is a thing at all. However, part of the mystery stems only from communication problems. It is hard to understand because it violates the following standard assumptions without sufficient mention or discussion --- though (some of) the violations might have a point in software engineering. However, it's still not clear whether (a) these problems can all be solved satisfactorily (b) .

• A conventional logic has a syntax in the usual sense, so that the set of judgements is countable. Direct Logic's judgements can refer to an uncountable set of actors. Therefore, Direct Logic's judgements cannot be encoded through Gödel's natural numbers.
• Conventionally, proof checking is decidable. It's unclear to me how Direct Logic's proof checking can be decidable; but maybe it only looks at a finite part of each actor. But if proof-checking is decidable, why can't you turn an execution trace of the proof-checker into a certificate c part of a countable set C of... proofs? Why can't you use that to produce Gödel's proofs? I guess such "proofs" would not be very compositional, so that it would be hard to construct larger proofs from smaller ones (as required for Gödel's theorems) — for instance, because a larger proof might get more info out of an actor. But it would be important to see a detailed discussion.
• Many conventional logics avoid reflective principles, which are part of direct logic; in particular, it includes the rule (⊦ T) ⇒ T. Reflective principles destroy several properties of a logic. This might be fine for some applications, but should be discussed.
• A conventional logic has the principle of explosion, while direct logic is paraconsistent. I agree this could be useful for software engineering, though this application has not been explored enough.

Overall, what is missing is a presentation of direct logic where the "assumed background knowledge" is at most first-order logic, and which follows standards for mathematical writing. Overall, it'd have to be a more "conformist" presentation.

Acknowledgements: a lot of the points above were figured out by many patient LtU readers.