On 21 Ago, 09:06, aatu.koskensi...@xortec.fi wrote:
> > I don't understand this statement. Are you saying that Gerhard > > Gentzen' proof of the consistency of Arithmetic is trivial? Or do you > > have something else in mind? > > Gentzen's proof is not at all trivial. What is trivial, by usual > mathematical standards, is the consistency of Peano arithmetic, > established by the following simple argument: > > The axioms of Peano arithmetic are true, no contradiction is true > and the rules of inference of first-order logic preserve truth; > hence no contradiction is provable in Peano arithmetic.
> Here we use the notion of truth, a mathematical property of sentences > in the language of arithmetic defined inductively. This notion, the > definition of which has the form "A is true iff for all sets X of > naturals ...", and the above argument, are not finitistically > meaningful. Gentzen's proof, on the other hand, is finitistically > meaningful, even though it contains an invocation of a principle, > "quantifier-free transfinite induction up to epsilon-0", that is not > finitistically justified.
Can you tell where can I find more details about this? I do not know enough Logic to understand why is it that the definition of truth that you mentioned is not finitistically meaningful.
>From such a proof we learn much more than > just that Peano arithmetic is consistent -- about which there never > were any real doubts -- e.g. a characterisation of the provably > recursive functions of Peano arithmetic.