3
$\begingroup$

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?

  • 0
    "I was asked if A is valid then Sk(A) is also valid, but I think I disproved it with a counter example" Example?2012-12-14

1 Answers 1

2

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.