Although [Gödel 1931] failed to proved inferential undecidability of Russell's Principia Mathematica, there is a fairly simple undecidable proposition namely, the proposition *Undecidable*≡Halt >[RunOne.[]] where RunOne.[]≡Eval.[SelectOne.[0]] such that SelectOne.[i:Natural]≡ExpressionFromString .[i] *finishesFirst* SelectOne.[i+1] Eval.[anExpression] evaluates anExpression and where the expression (expression1 *fini…
There is a small typo in the above:
Undecidable ≡ Halt>[⦅RunOne.[]⦆] is
inferentially undecidable in the theory Actors, that is,
⊬Undecidable and ⊬¬Undecidable where
RunOne.[]≡Eval.[SelectOne.[0]] and ⦅RunOne.[]⦆ is the
expression for the procedure application RunOne.[]