Some properties of the -calculus
Karim Nour, Khelifa Saber · Journal of Applied Non-Classical Logics · 2012
In this paper, we present the -calculus which at the typed level corresponds to the full classical propositional natural deduction system. The Church–Rosser property of this system is proved using the standardisation and the finiteness developments theorem. We also define the leftmost reduction and prove that it is a winning strategy.