Consistency of Heyting arithmetic in natural deduction
Annika Kanckos · Mathematical logic quarterly · 2010
Abstract A proof of the consistency of Heyting arithmetic formulated in natural deduction is given. The proof is a reduction procedure for derivations of falsity and a vector assignment, such that each reduction reduces the vector. By an interpretation of the expressions of the vectors as ordinals each derivation of falsity is assigned an ordinal less than ε 0, thus proving termination of the procedure (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)