# Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi

## TL;DR

This paper provides an arithmetical proof of strong normalization for lambda-Sym-Prop and establishes a translation to lambda-bar-mu-mu-tilde-star-calculus, introducing the concept of zoom-in sequences of redexes.

## Contribution

It offers a new arithmetical proof of strong normalization for lambda-Sym-Prop and connects it to lambda-bar-mu-mu-tilde-star-calculus using a novel method involving zoom-in sequences.

## Key findings

- Proved strong normalization of lambda-Sym-Prop
- Established translation to lambda-bar-mu-mu-tilde-star-calculus
- Introduced the concept of zoom-in sequences of redexes

## Abstract

In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.