Premium
Consistency of Heyting arithmetic in natural deduction
Author(s) -
Kanckos Annika
Publication year - 2010
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200910118
Subject(s) - falsity , mathematics , consistency (knowledge bases) , natural deduction , reduction (mathematics) , interpretation (philosophy) , natural number , discrete mathematics , arithmetic , algebra over a field , pure mathematics , computer science , programming language , epistemology , philosophy , geometry
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)