Decidability and Completeness
Yves Nievergelt · Birkhäuser Boston eBooks · 2002
This chapter explains in detail various methods to investigate which of several alternative logics and axioms for mathematics correspond most closely to the common and scientific patterns of reasoning. Some of these logics have sufficient power, while other logical systems lack the power, to decide whether certain logical formulae are theorems, and hence whether they are allowed (within such logics) in common or scientific arguments. Examples demonstrate that all the proofs within the implicational calculus (with implications, but without negation) do not suffice to prove certain implicational tautologies. In other words, the implicational calculus lacks the power to decide the status of certain of its own implicational formulae. The same examples also demonstrate how a computing language based on axioms and rules might fail to generate all sentences in the language. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.