3 Tableau calculus, certified
Strict signs \(T,F\) and weak signs \(P=\{ T,Z\} \), \(N=\{ F,Z\} \); weak signs occur only in refutation polarity.
Fuel-indexed structural tableau engine over the generating basis \(\{ \neg ,\wedge ,\vee \} \); heavy connectives reduce by the living identities.
The tableau closes iff the signed nodes are unsatisfiable — for all formulas, by induction on weighted size. Zero axioms.
\(\Gamma \vdash \varphi \) by the engine iff every valuation making all premises \(T\) makes \(\varphi \) \(T\).
The engine with native signed rules for \(\to ,\oplus ,\leftrightarrow \) is certified by the same induction and returns identical verdicts.