RT Journal Article
T1 Proof theory for tight apartness
A1 Maffezioli, Paolo
AB The paper provides a cut-free sequent calculus for the theory of tight apartness in a language where both apartness and equality are primitive notions. The result is obtained by aptly modifying the underlying logical calculus for intuitionistic logic and adding rules of inference corresponding to the axioms of apartness and the principles governing the mutual deductive relationships between apartness and equality. While the rules for apartness are found directly from the axioms by applying standard proof-theoretic methods, the others, especially the rule corresponding to the principle of tight apartness, are found by exploiting the logical law of consequentia mirabilis. Along the way, we also provide a cut-free sequent calculus for the theory of weak tight apartness, also known as the theory of negated equality, thus answering in the positive to an open problem in the existing literature on the subject.
PB Institute of Philosophy and Sociology Polish Academy of Sciences
SN 0039-3215
YR 2025
FD 2025
LK https://hdl.handle.net/20.500.14352/124777
UL https://hdl.handle.net/20.500.14352/124777
LA eng
NO Maffezioli, P. Proof Theory for Tight Apartness. Stud Logica (2025). https://doi.org/10.1007/s11225-025-10201-0
NO 2025 Acuerdos transformativos CRUE-CSIC con Springer Nature.
NO Universidad Complutense de Madrid
DS Docta Complutense
RD 10 nov 2025