We address two questions: • what is the use of formal proofs? • how do we proceed from a formal proof to a computation? Indeed, the latter is subsidiary to the former and is briefly dealt with by means of concrete examples in the final section. We shall argue that formal proofs yield in many cases genuine methods for ideal experiments with problematic principles and rules, and for gaining semantical and computational information. The points are briefly illustrated by cases taken from proof theory; we emphasize the fact that even within proof theory, the variety (vs. purity) of methods is common practice and it is justified by theoretical results. The main motivation is to contrast the claim that there would be a standard thesis among logically oriented philosophers of mathematics, tending to reduce the essence of usual proofs of mathematical statements to their formal counterparts within a given axiomatic theory. This tenet is not justified today; actual genuine uses of formal proofs are peculiar and technical, and they do not aim at certainty or formalistic foundations.

On formal proofs / A. Cantini. - STAMPA. - (2008), pp. 29-48.

On formal proofs

CANTINI, ANDREA
2008

Abstract

We address two questions: • what is the use of formal proofs? • how do we proceed from a formal proof to a computation? Indeed, the latter is subsidiary to the former and is briefly dealt with by means of concrete examples in the final section. We shall argue that formal proofs yield in many cases genuine methods for ideal experiments with problematic principles and rules, and for gaining semantical and computational information. The points are briefly illustrated by cases taken from proof theory; we emphasize the fact that even within proof theory, the variety (vs. purity) of methods is common practice and it is justified by theoretical results. The main motivation is to contrast the claim that there would be a standard thesis among logically oriented philosophers of mathematics, tending to reduce the essence of usual proofs of mathematical statements to their formal counterparts within a given axiomatic theory. This tenet is not justified today; actual genuine uses of formal proofs are peculiar and technical, and they do not aim at certainty or formalistic foundations.
2008
9788847007840
Deduction, Computation, Experiment
29
48
A. Cantini
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/318527
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 1
social impact