Mortgage loan: Difference between revisions

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 $A_{1}, A_{2}, \dots$ be an enumeration of the axioms of a recursively enumerable set T of first-order formulas. Construct another set T* consisting of

\underset{i}{\underset{⏟}{A_{i} \land \dots \land A_{i}}}

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 $A_{1}$ or of the form

\underset{j}{\underset{⏟}{B_{j} \land \dots \land B_{j}}} .

Since each formula has finite length, it is checkable whether or not it is $A_{1}$ 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 $A_{j}$ ; otherwise it is not in T*. Again, it is checkable whether it is in fact $A_{n}$ 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 $A_{i}$ with

\underset{i}{\underset{⏟}{A_{i} \land \dots \land A_{i}}}

one instead replaces it with

\underset{f (i)}{\underset{⏟}{A_{i} \land \dots \land A_{i}}}

(*)

where f(x) is a function that, given i, returns a computation history showing that $A_{i}$ 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 $A_{i}$ 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.

@@ Line 1: / Line 1: @@
-Myrtle Benny is how I'm known as and I feel comfy when people use the complete name. Doing ceramics is what love doing. North Dakota is our birth location. My working day job is a librarian.<br><br>Here is my blog :: at home std testing; [http://www.Cam4teens.com/blog/84472 just click the next post],
+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]]

Mortgage loan: Difference between revisions

Revision as of 06:59, 4 February 2014

Recursive axiomatization

Primitive recursive axiomatizations

References

Navigation menu

Search