more from this thinker     |     more from this text


Single Idea 13824

[filed under theme 5. Theory of Logic / H. Proof Systems / 1. Proof Systems ]

Full Idea

Frege's formal definition of derivability is perhaps the first investigation in general proof theory.

Gist of Idea

Proof theory began with Frege's definition of derivability

Source

report of Gottlob Frege (Begriffsschrift [1879]) by Dag Prawitz - Gentzen's Analysis of First-Order Proofs 2 n2

Book Ref

'A Philosophical Companion to First-Order Logic', ed/tr. Hughes,R.I.G. [Hackett 1993], p.207


A Reaction

In 'On General Proof Theory §1' Prawitz says "proof theory originated with Hilbert" in 1900. Presumably Frege offered a theory, and then Hilbert saw it as a general project.


The 4 ideas with the same theme [general ideas about the different proof systems]:

Proof theory began with Frege's definition of derivability [Frege, by Prawitz]
Logical proof just explicates complicated tautologies [Wittgenstein]
An 'informal proof' is in no particular system, and uses obvious steps and some ordinary English [Bostock]
'Induction' and 'recursion' on complexity prove by connecting a formula to its atomic components [Burgess]