Contraction-free sequent calculi for intuitionistic theories of apartness and order are given and cut-elimination for the calculi proved. Among the consequences of the result is the disjunction property for these theories. Through methods of proof analysis and permutation of rules, we establish conservativity of the theory of apartness over the theory of equality defined as the negation of apartness, for sequents in which all atomic formulas appear negated. The proof extends to conservativity results for the theories of constructive order over (...) the usual theories of order. (shrink)

Both at the propositional and the predicate level, in tableau systems of intuitionistic logic as well as in the corresponding sequent and natural calculi, the problem arises of reducing as much as possible the duplication of formulas, i.e., the reuse of formulas already used in a proof, in order to single out efficient proof search techniques. This problem has been analyzed in a paper by Dyckhoff, where a nearly optimal solution is given for intuitionistic propositional sequent and natural calculi, and (...) in previous papers by the authors, where an improvement is proposed of Fitting's tableau system for intuitionistic predicate logic. In the present paper we reanalyze the ideas of our previous works in the light of Dyckhoff's results. This gives rise to a tableau system for intuitionistic predicate logic which provides a good improvement of the previous tableau systems with respect to the problem of duplication. The formal setting of the paper seems to be promising to treat further intermediate logics. In this line, we analyze Kuroda logic and provide for it a tableau system involving a smaller amount of duplication than the one involved in the intuitionistic tableau system presented in the paper. (shrink)