Tableaux

In one of Langan’s extraneous posts somewhere he mentions the CTMU being originally based on a hierarchical nesting of universal computers he called Nested Simulation Tableau or NeST. I figured it would be good to look into tableau to try and get inside his head more. I am drawing from Open Logic Project.

Tableau is a derivation system that allows you to potentially prove or disprove formulas in some logic. Let’s start with propositional logic. Unlike other derivation systems like natural deduction or the sequent calculus, a tableau uses signed formulas. A signed formula is notated Tf or Ff where T or F is the truth sign of the formula and f is the formula itself. A tableau consists of joined branches with formula “in series” on the branch. If a branch contains the same formula signed both T and F then that branch is closed. If all branches of a tableau are closed then the tableau itself is closed and the assumptions on the “start branch” of the tableau cannot all be true at the same time. To prove a formula f true, we take Ff as an assumption and attempt to close the tableau. This shows that, at least in light of any other assumption we may be using, the formula f cannot be false. For each operator: AND, OR, NOT, IMPLIES (IF/THEN), there are two rules: one for T formulas and one for F formulas. In the following rules “->” means given the formula on the left, add the formula on the right to the branch. The symbol “|” means the branch now splits into two branches at that point. “,” simply means two formulas are added to the branch.

Rules:

NOT T: T NOT(f) -> Ff

NOT F: F NOT(f) -> Tf

AND T: T AND(f, g) -> Tf, Tg

AND F: F AND(f, g) -> Ff | Fg

OR T: T OR(f, g) -> Tf | Tg

OR F: F OR(f, g) -> Ff , Fg

IMPLIES T: T IMPLIES(f, g) -> Ff | Tg

IMPLIES F: F IMPLIES(f, g) -> Tf , Fg

Here is a visualization of a tableaux, it’s kinda hard without the visual aid:

Fig of a tableau from chapter 11.4 of Open Logic Project’s complete build

The robot suggested that nested simulation tableau would be closer to tableau in a modal logic. So far we’ve only done propositional logic. Let’s keep going. In predicate logic we have all the previous rules, plus four more. We have two new rules for ∀ and two new rules for ∃.

New rules:

∀ T: T∀x f(x) -> Tf(t) (where t is a closed term)

∀ F: F∀x F(x) -> Ff(a) (where a is some constant symbol not occurring anywhere in the branch above the rule application.)

∃ T: T∃x f(x) -> Tf(a) (where a is some constant symbol not occurring anywhere in the branch above the rule application.)
∃ F: F∃x f(x) -> Ff(t) (where t is a closed term)

By the way, the Open Logic Project complete build linked above gives these rules in a way nicer format. I’d recommend looking there if you’re interested. But let’s continue. The Langan was using hierarchical universal computers and called it NeST for Nested Simulation Tableau. He generally is quite straight forward with his naming (at least if you know what he’s talking about), so we can make a few guesses. First, tableau is important to understand how he had these nested computers configured in some way. Second, I think model theory has some comments on simulation itself so we’ll want to look into that. Third, the robot suggested modal logic and Langan seems to have a grasp of the advanced knowledge in the domains he’s working in so to the extent he’s using tableau, he’s probably starting there. So let’s go look at modal tableau.

…

Oh. Oh god… I do not feel even remotely prepared to tackle this, let alone try to overview it for anyone else. It looks like it starts by prefixing the signs with sets of integers. There are also symbols in there I don’t recognize, and I’ve done a fair bit of math. Fuck that, I’m taking the long way up. Wish me luck. Good god, some people and their brains…