Page 768 of 800
| Page 768 of 800 | Search internet |
Origin: Peano. Landing-place: diagnose.
Definition soundness check of v failed. Error could be in any, transitively used definition or could be that the definition is circular.
Peano arithmetic PA as defined on the Peano page has a Def rule which is the 'inference of definition'. The inference of definition allows to conclude that two terms are equivalent if they are equal 'by definition'. As an example, the axioms of PA do not mention the 
connective. However, the Peano page defines thus:
That definition together with the Def rule allows to reason about even though no axiom mentions it.
The inference of definition puts a number of restrictions on definitions. Among other, the PA version of the inference of definition does not permit recursive definitions.
Checking definitions for validity on each application would be far too costly in terms of cpu time. For that reason, all definitions on a page are checked in one go by a 'soundness checker'. The soundness checker verifies that all 'math' definitions are valid from the point of view of PA.
The 'Definition soundness check of v failed' message indicates that the given construct had an invalid definition. It is then up to the user to spot the problem since the soundness checker does not provide any more information.
| Page 768 of 800 | Search logiweb.eu |