Bernays' lost truth table

Stream: general

[Mario Carneiro]

The recent arXiv short note On the independence of Robinson's set of axioms for propositional calculus by Benoît Jubin reconstructs a five-valued truth table to show the independence of axiom (S) in Robinson's axioms for classical propositional logic. Formalizing this result looks like it could be a fun little project.