Strong Types for Direct Logic

Hi Carl, it's me, mathematics. I'm sure you recall that Turing machines (TMs) can be enumerated. ActorScript programs can also be enumerated, as can Direct Logic statements. I'm sure that you also have no problem with the basic concept of arithmetic encoding, nor with diagonalization widgets.

So, I'd like you to demonstrate that Direct Logic is, in fact, strictly more powerful than TMs, by constructing a DL program which cannot be computed by any TM.

Alternatively, I'd like you to prove the claim, "In Direct Logic, categorical theories of the Natural Numbers, Real Numbers, Ordinal Numbers, Set Theory, the Lambda Calculus, and Actors are inferentially decidable, meaning that every true proposition is provable and every proposition is either provable or disprovable," from your abstract. Specifically, I'd like you to construct the Direct Logic program which proves or disproves any given theorem. If that is too difficult, it will suffice to demonstrate a use of Direct Logic to answer a tough question about numbers; I humbly invite you to consider Goldbach's conjecture.

Thanks and good luck.