Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I have a claim I need to prove or disprove. Let Sk(A) be the Skolemization of A (A is a sentence). If Sk(A) is valid then A is also valid.

In other exercise I was asked if A is valid then Sk(A) is also valid, but I think I disproved it with a counter example(if it is right then please let me know hehe)

I think that its true that if Sk(A) is valid then A is also valid, but I don't know how to show that.

Any ideas where to start?

share|improve this question
    
What does valid mean? In a given $L$-structure? The language has changed, and one technically needs to provide an interpretation for the new constant symbols/function symbols. However, under any such interpretation, if the Skolemization is valid, then the sentence is. –  André Nicolas Dec 14 '12 at 19:33
    
"I was asked if A is valid then Sk(A) is also valid, but I think I disproved it with a counter example" Example? –  Peter Smith Dec 14 '12 at 20:18

1 Answer 1

Skolemization is refutation complete but not validation complete. Means if you have a theory T, and its skolemization T^S, you will know:

T |= [] iff T^S |= [].

This is why skolemization is often found in theorem proving. For validity you would need Herbrandization which will attack forall quantifiers and not existential quantifiers. With Herbrandization one has:

[] |= T iff [] |= T^H

Both Skolemization and Herbrandization are based on the following higher order identity and its dual which can be obtained by negating both sides:

forall x exists y A(x,y) <-> exists f forall x A(x,f(x))

The identity makes use of the axiom of choice in one direction. The quantification of the functorial f is delegated to the signature of the first order theory and the definition of the |= sign.

Possibly Skolemization and Herbrandization can be combined, but I wouldn't confuse it with Morleyization since both Skolemization and Herbrandization introduce function symbols and not relation symbols.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.