Synthetic Tableaux with Unrestricted Cut for First-Order Theories
Dorota Leszczyńska-Jasion, Szymon Chlebowski · Axioms · 2019
The method of synthetic tableaux is a cut-based tableau system with synthesizing rules introducing complex formulas. In this paper, we present the method of synthetic tableaux for Classical First-Order Logic, and we propose a strategy of extending the system to first-order theories axiomatized by universal axioms. The strategy was inspired by the works of Negri and von Plato. We illustrate the strategy with two examples: synthetic tableaux systems for identity and for partial order.