Hi
Can anyone tell me what an "existential function-free formula" is please?
Thanks!
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".
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?
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.