Arithmetical Proofs of Strong Normalization Results for Symmetric λ-calculi

摘要: We give arithmetical proofs of the strong normalization two symmetric λ-calculi corresponding to classical logic. The first one is λ¯μμe-calculus introduced by Curien & Herbelin. It derived via Curry-Howard correspondence from Gentzen's sequent calculus LK in order have a symmetry on side between "program" and "context" other "call-by-name" "callby-value". The second λμ-calculus. λμ-calculus Parigot which reduction rule μ', μ, added. These results were already known but previous use candidates reducibility where interpretation type defined as fix point some increasing operator thus, are highly non arithmetical.