Let A be a well-formed statement of L and let L+ be the extension of L obtained by including A as a new axiom. Prove that the set of theorems of L+ is different from the set of theorems of L if and only if A is not a theorem of L.

Printable View

- Oct 5th 2010, 04:19 PMDavyHilbertLogic (L system)
Let A be a well-formed statement of L and let L+ be the extension of L obtained by including A as a new axiom. Prove that the set of theorems of L+ is different from the set of theorems of L if and only if A is not a theorem of L.

- Oct 5th 2010, 07:44 PMDavyHilbert
is it begging the question to say that since adding A to L increases Thm(L) that A is not a tautology and thus is not an element of L?

- Oct 6th 2010, 03:12 AMemakarov
This is pretty clear, so it may be hard to find precisely correct words to justify it.

Quote:

Prove that the set of theorems of L+ is different from the set of theorems of L if and only if A is not a theorem of L.

Quote:

since adding A to L increases Thm(L) that A is not a tautology and thus is not an element of L

The left-to-right direction can be shown by contradiction using this property: If and , then (here denotes derivability in L). How this property is proved depends on the specifics of L. - Oct 8th 2010, 12:38 AMPiperAlpha167
Presumably, system L is decidable; otherwise, I think we won't have an effective method for determining exactly what's in Thm(L) and Thm(L+).

If, in addition, the definitions of theorem and proof in system L are given in the usual way, then an axiom is a theorem with a one-line proof.

In such a system, I think both directions of the claim should go through pretty easily.

For example, in the => direction, argue the contrapositive.

That is, assume A is in Thm(L), and show then that the collection of theorems of the "extended" system L+, i.e., Thm(L+), must be identical with Thm(L). - Oct 8th 2010, 12:49 AMemakarovQuote:

Presumably, system L is decidable; otherwise, I think we won't have an effective method for determining exactly what's in Thm(L) and Thm(L+).