Maffezioli, Paolo2025-10-102025-10-102025Maffezioli, P. Proof Theory for Tight Apartness. Stud Logica (2025). https://doi.org/10.1007/s11225-025-10201-00039-321510.1007/s11225-025-10201-0https://hdl.handle.net/20.500.14352/1247772025 Acuerdos transformativos CRUE-CSIC con Springer Nature.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.engAttribution 4.0 Internationalhttp://creativecommons.org/licenses/by/4.0/journal article1572-8730https://doi.org/10.1007/s11225-025-10201-0https://produccioncientifica.ucm.es/documentos/6880a3da3871d04c4eb4a2afopen access164ApartnessProof theoryCut eliminationLógica simbólica y matemática (Filosofía)1102.08 Lógica Matemática1102.03 Lógica Formal1102.11 Teoría de Pruebas