(See the entry on the development of proof theory).
For the philosophical position and development of proof theory the entries on Hilbert's program and the development of proof theory as well as Prawitz (1971).
(For further discussion, see the entry on the development of proof theory).
Already much earlier, around 1935, Gerhard Gentzen (see the entry on the development of proof theory) had provided such a statement.
In particular, it turns out that a standard sequent calculus formulation of GL obeys cut elimination, which means, roughly formulated, that each formula provable from GL in the sequent calculus also has a GL sequent proof "without detours" (see Negri (2005), Goré and Ramanayake (2008); see also the entry the development of proof theory for a precise explanation of cut elimination).
It has nevertheless continued to be an influential position in the philosophy of mathematics, and, starting with the work of Gerhard Gentzen in the 1930s, work on so-called Relativized Hilbert Programs have been central to the development of proof theory.
Furthermore, by using B. anthracis (Sterne, 34F2), an animal vaccine and B. cereus- 4342, a γ-phage susceptible rare strain as surrogates of B. anthracis, development of proof-of-concepts for B. anthracis are feasible.
We introduce explicit induction, a new induction scheme targeted to temporal properties, and to interactive development of inductive proofs.
A key aspect of our approach is the introduction of a proof assistant at an early stage, namely during development of the proof.
Moreover, we propose the development of a Proof Certificate standard.
