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