On the proofs of some formally unprovable propositions and prototype proofs in type theory (Q4736397)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 2085173
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | On the proofs of some formally unprovable propositions and prototype proofs in type theory |
scientific article; zbMATH DE number 2085173 |
Statements
9 August 2004
0 references
type theory
0 references
proof theory
0 references
inductive definition
0 references
Herbrand's proofs
0 references
0.6510362029075623
0 references
0.6128523945808411
0 references
On the proofs of some formally unprovable propositions and prototype proofs in type theory (English)
0 references
The author examines some specific limits of the formalization of logic and mathematics in order to give insight into and encourage a broadening of tools for formal proofs. The role of mathematical induction and well-orderedness in proofs is discussed in great detail, but there is no discussion of the implications of the logical equivalence of mathematical induction and well-orderedness. The author concludes that the foundation of mathematics lies in logic, formalisms and regularities of phenomenal space. For the entire collection see [Zbl 0988.00060].
0 references
