 Investigations into the Predicate Calculus
Oiva Ketonen. Edited by Sara Negri and Jan von Plato
Oiva Ketonen (19132000) was the closest to a student the creator of modern proof theory Gerhard Gentzen ever had. Their encounter took place in 193839 in GĂ¶ttingen, with Ketonen hoping to receive a suitable topic for a doctoral dissertation and Gentzen instead deeply immersed in attempts at proving the consistency of analysis. Ketonenâ€™s thesis of 1944, his only work in logic, introduced what is today called the G3sequent calculus. It is his bestknown discovery, a sequent calculus for classical propositional logic the logical rules of which are all invertible. Few read his thesis, the results of which were instead made available through a long review by Paul Bernays. Ketonen's calculus is the basis of Evert Beth's tableau method and of the sequent calculi in Stephen Kleene's influential {it Introduction to Metamathematics}. A second result was a sharpening of the midsequent theorem, by which the number of quantifier inferences with eigenvariables could be minimized. The existence of a weakest possible midsequent followed, in the sense that if any midsequent is derivable, a weakest one is. Turning this into a contrapositive, Ketonen found a purely syntactic method for proofs of underivability that he applied to affine plane geometry. His result, in modern terms, was a positive solution to the word problem for the universal fragment of plane affine geometry, with a syntactic proof of underivability of the parallel postulate from the rest of the affine axioms as a corollary.
See inside
1 December 2022
9781848904071
Buy from Amazon: UK US
