A formal system of negationless arithmetic that is conservative with respect to Heyting arithmetic (Q1064322)

A system of natural deduction for a negationless arithmetic is presented. A deduction in \(HA^ N\) is defined as a pair of deductions \(<\Sigma_ 1,\Sigma_ 2>\), where \(\Sigma_ 1\) is a proof of nonemptiness of the conjunction of all open hypotheses of \(\Sigma_ 2\) and \(\Sigma_ 2\) is a deduction in a classical sense. Natural interpretations of HA in \(HA^ N\) and \(HA^ N\) in HA are introduced. Appropriate interpretation results are proven showing in particular that HA is a conservative extension of \(HA^ N\) with respect to the interpretation.