Abstract

The aim of the paper is to present two natural deduction systems for Intuitionistic Sentential Calculus with Identity ( ISCI ); a syntactically motivated \(\mathsf {ND}^1_{\mathsf {ISCI}}\) and a semantically motivated \(\mathsf {ND}^2_{\mathsf {ISCI}}\). The formulation of \(\mathsf {ND}^1_{\mathsf {ISCI}}\) is based on the axiomatic formulation of ISCI. Its rules cannot be straightforwardly classified as introduction or elimination rules; ISCI -specific rules are based on axioms characterizing the identity connective. The system does not enjoy the standard subformula property, but due to the normalization procedure non-subformulas can label only leaves of proofs. In \(\mathsf {ND}^2_{\mathsf {ISCI}}\), we propose only two general identity-related rules, in reference to the treatment of the identity connective in First-Order Logic.