Mortgage loan: Difference between revisions
en>Barek m Reverted edits by Marksinclair1 (talk) to last version by Barek |
en>Nueragroup m →Recent trends: Fixed broken link and found corresponding pdf on bbc website |
||
Line 1: | Line 1: | ||
In [[mathematical logic]], '''Craig's theorem''' states that any [[recursively enumerable set]] of [[well-formed formula]]s of a [[first-order language]] is (primitively) recursively axiomatizable. This result is not related to the well-known [[Craig interpolation]] theorem. | |||
== Recursive axiomatization == | |||
Let <math>A_1,A_2,\dots</math> be an enumeration of the axioms of a recursively enumerable set T of first-order formulas. Construct another set T* consisting of | |||
:<math>\underbrace{A_i\land\dots\land A_i}_i</math> | |||
for each positive integer ''i''. The [[deductive closure]]s of T* and T are thus equivalent; the proof will show that T* is a decidable set. A decision procedure for T* lends itself according to the following informal reasoning. Each member of T* is either <math>A_1</math> or of the form | |||
:<math>\underbrace{B_j\land\dots\land B_j}_j.</math> | |||
Since each formula has finite length, it is checkable whether or not it is <math>A_1</math> or of the said form. If it is of the said form and consists of ''j'' conjuncts, it is in T* if it is the expression <math>A_j</math>; otherwise it is not in T*. Again, it is checkable whether it is in fact <math>A_n</math> by going through the enumeration of the axioms of T and then checking symbol-for-symbol whether the expressions are identical. | |||
== Primitive recursive axiomatizations == | |||
The proof above shows that for each recursively enumerable set of axioms there is a recursive set of axioms with the same deductive closure. A set of axioms is [[primitive recursive]] if there is a primitive recursive function that decides membership in the set. To obtain a primitive recursive aximatization, instead of replacing a formula <math>A_i</math> with | |||
:<math>\underbrace{A_i\land\dots\land A_i}_i</math> | |||
one instead replaces it with | |||
:<math>\underbrace{A_i\land\dots\land A_i}_{f(i)}</math> (*) | |||
where ''f''(''x'') is a function that, given ''i'', returns a computation history showing that <math>A_i</math> is in the original recursively enumerable set of axioms. It is possible for a primitive recursive function to parse an expression of form (*) to obtain <math>A_i</math> and ''j''. Then, because [[Kleene's T predicate]] is primitive recursive, it is possible for a primitive recursive function to verify that ''j'' is indeed a computation history as required. | |||
==References== | |||
* [[William Craig (logician)|William Craig]]. '''On Axiomatizability Within a System''', ''The Journal of Symbolic Logic'', Vol. 18, No. 1 (1953), pp. 30-32. | |||
[[Category:Computability theory]] | |||
[[Category:Theorems in the foundations of mathematics]] |
Revision as of 06:59, 4 February 2014
In mathematical logic, Craig's theorem states that any recursively enumerable set of well-formed formulas of a first-order language is (primitively) recursively axiomatizable. This result is not related to the well-known Craig interpolation theorem.
Recursive axiomatization
Let be an enumeration of the axioms of a recursively enumerable set T of first-order formulas. Construct another set T* consisting of
for each positive integer i. The deductive closures of T* and T are thus equivalent; the proof will show that T* is a decidable set. A decision procedure for T* lends itself according to the following informal reasoning. Each member of T* is either or of the form
Since each formula has finite length, it is checkable whether or not it is or of the said form. If it is of the said form and consists of j conjuncts, it is in T* if it is the expression ; otherwise it is not in T*. Again, it is checkable whether it is in fact by going through the enumeration of the axioms of T and then checking symbol-for-symbol whether the expressions are identical.
Primitive recursive axiomatizations
The proof above shows that for each recursively enumerable set of axioms there is a recursive set of axioms with the same deductive closure. A set of axioms is primitive recursive if there is a primitive recursive function that decides membership in the set. To obtain a primitive recursive aximatization, instead of replacing a formula with
one instead replaces it with
where f(x) is a function that, given i, returns a computation history showing that is in the original recursively enumerable set of axioms. It is possible for a primitive recursive function to parse an expression of form (*) to obtain and j. Then, because Kleene's T predicate is primitive recursive, it is possible for a primitive recursive function to verify that j is indeed a computation history as required.
References
- William Craig. On Axiomatizability Within a System, The Journal of Symbolic Logic, Vol. 18, No. 1 (1953), pp. 30-32.