Conceptions of Proof from Aristotle to Gentzen’s Calculi

The present paper aims to show how some key ideas at the basis of the normalization results in proof theory have their deep grounds in a number of fundamental questions that are posed always anew within the philosophical reflection on mathematics. Two different paradigms of proofs, synthetic and analytic, are contrasted and their origin is traced back to Aristotle as well as to Bernard Bolzano’s idea of a better grounded presentation of mathematics at the beginnings of the 19th century. Two different proofs of the cut-elimination theorem are then sketched with the aim of showing, on the one hand, what happens when one tries to implement formally the traditional idea of rigorous scientific proof and, on the other hand, how high are “the costs” in terms of complexity of the proofs when one avoids the use of transitivity, that is, in traditional terms, the use of fortuitous alien intermediate concepts in the proofs.