Sequent-style tableaux for intuitionistic propositional logic
Sequent-style tableaux are a refutation calculus in which each node of the refutation tree carries a finite block of formulae and the structural rules are absorbed into the data structure and the closure criterion. In their original, classical form they rest on an involutive De Morgan negation and on closure upon a complementary pair. We show that both may be dispensed with. Replacing unsigned formulae by signed ones, we obtain a block calculus $\mathbf{B}_{ti}$ for intuitionistic propositional logic in which the whole of intuitionism is carried by one rule, the rule decomposing…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2608.21143
curl -X POST /api/v1/records/arxiv/2608.21143/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.21143/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'