Hi

Can anyone tell me what an "existential function-free formula" is please?

Thanks!

Printable View

- March 28th 2013, 11:58 AMimssrExistential Function-free formula
Hi

Can anyone tell me what an "existential function-free formula" is please?

Thanks! - March 28th 2013, 12:14 PMemakarovRe: Existential Function-free formula
It's probably a formula that starts with the existential quantifier and does not contain functional symbols.

- March 31st 2013, 04:19 PMimssrRe: 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". - April 1st 2013, 10:34 AMemakarovRe: Existential Function-free formula
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.