Summary: \(\lambda^{\text{Sym}}_{\text{PA}}\) is a natural deduction system for Peano Arithmetic that was developed in order to provide a basis for the programming-with-proofs paradigm in a classical logic setting. In the paper, we analyze one of its main features: non-confluence. After looking at which rules can cause non-confluence, we develop in the system a formal proof for a formula that can be seen as a simple but meaningful program specification. The computational behaviour of the corresponding term will be analyzed by interpreting it is a (higher-order communicating) process formed by distinct subprocesses which co-operate in different ways, producing different results, according to the reduction strategy used. We also show how to restrict the system in order to get confluence without loosing its computational features. The restricted system enables us to argue for the expressive power of symmetric and non-deterministic calculi like \(\lambda^{\text{Sym}}_{\text{PA}}\).
For the entire collection see [Zbl 0871.00032].