# Existential Function-free formula

• Mar 28th 2013, 11:58 AM
imssr
Existential Function-free formula
Hi
Can anyone tell me what an "existential function-free formula" is please?
Thanks!
• Mar 28th 2013, 12:14 PM
emakarov
Re: Existential Function-free formula
It's probably a formula that starts with the existential quantifier and does not contain functional symbols.
• Mar 31st 2013, 04:19 PM
imssr
Re: Existential Function-free formula
Hi emakarov
Thanks for your immediate reply. Since you started your answer with 'probably', I expected others to reply to my question as I'm not in a position to accept the answer as correct or incorrect. Anyway, I'm going to explain why I asked this question.

My understanding is that if we check the satisfiability of the two formulae within a given finite scope and do not find a satisfying instance, we cannot say with a guarantee that the formulas are absolutely unsatisfiable i.e. no satisfying instance exists for the formulae () regardless whether they are "existential function-free" or not. Am I right?
Basically, I'm trying to find out how an "existential function-free" formula is different from the one which contains "existential function".
• Apr 1st 2013, 10:34 AM
emakarov
Re: Existential Function-free formula
Quote:

Originally Posted by imssr
My understanding is that if we check the satisfiability of the two formulae within a given finite scope and do not find a satisfying instance, we cannot say with a guarantee that the formulas are absolutely unsatisfiable i.e. no satisfying instance exists for the formulae () regardless whether they are "existential function-free" or not. Am I right?

I am not sure I fully understand the question. Why are you talking about two formulas? Is the situation with a single formula different? Does the finite scope mean a finite model (interpretation)? What is a satisfying instance? For a formula of the form ∃x P(x) we can talk about an instance P(c) of P(x) such that P(c) is true. But I am not sure what satisfying instance is in other contexts.

Yes, is a formula is false in a given model, it does not mean that it is false in all models, i.e., that it is unsatisfiable. What does it have to do with existential function-free formulas?

Quote:

Originally Posted by imssr
Basically, I'm trying to find out how an "existential function-free" formula is different from the one which contains "existential function".

I strongly suspect that "an existential function-free formula" means a formula that is both existential and function-free, not free of existential functions. I am not sure what existential functions are; the only thing that comes to mind are Skolem functions, but I am not sure if "free of Skolem functions" makes sense. Of course, to be sure, you need to check the definitions in your source.