When do two descriptions
behave the same?
Explore contextual certification through the finite propositional model accompanying Gödelian Recursive Incompleteness. Choose two presentations, challenge them with every logical context, and follow their evolution through repeated successor operations.
01 · Choose the presentations
Select a preset or any of the 153 finite presentationsPresentation α
Left systemPresentation β
Right system02 · Follow the transformations
Click a stage to inspect its stateSuccessor trajectory
Aₙ₊₁ = Aₙ ∪ {first non-theorem}03 · Challenge every context
16 truth-table contexts · click one to examine itContextual consistency tests at the selected stage
agreement disagreementFor each formula φ, test whether the presentation admits a model where ¬φ holds. In this finite classical model, “no such model” is equivalent to entailment of φ.
04 · Execute the full audit
Reproduce the Mac Python experiment in your browserExhaustive finite-model verification
Tests the deduction/consistency relationship, contextual equivalence, and five-step successor preservation for all 23,409 ordered pairs.
05 · What this does—and what it doesn't
Finite semantic behavior
The model exhausts all Boolean formulas on two atoms (16 truth tables) and all presentations containing zero, one or two axioms (153 presentations). Its contextual tests characterize equality of model sets in this small classical universe.
Because the chosen successor is determined only by the model set, equal presentations stay equivalent here. This toy system cannot display genuine delayed Gödelian divergence.
Actual Gödelian verification
The manuscript concerns arithmetized provability, uniform PA-internal proof certificates, diagonalization and inherited-axiom Gödelian successors.
Those require explicit proof encodings and Lean-checked arithmetic theorems. The companion Lean project tracks the outstanding proof obligations; the browser model does not discharge them.