I want to prove $\phi \models \psi$ iff $\phi \cup \{\neg \psi\}$ unsatisfiable.

What's the meaning of the union operator w.r.t. satisfiability in FOL?

Does it mean that all such interpretations $\mathcal{I}$ of the LHS also have to model $\phi$ and $\{\neg \psi\}$?

So $\phi \cup \{\neg \psi\} \Leftrightarrow \phi \wedge \neg \psi$ ?

I read a few other related posts.

First one which I changed w.r.t. my proof:

Let $\phi$ be a set of propositional formulas and $\psi$ a propositional formula.


Assume $\phi\models \psi$ and $\phi \cup \{\neg \psi\}$ satisfiable

Then there is a variable assignment s.t. $\forall \varphi:(\beta \models \varphi) \wedge (\beta \models \neg\psi)$

It follows that $\beta \nvDash \psi$. Therefore $\psi$ not a consequence of $\phi$.


Assume $\psi \cup \{\neg \psi\}$ not satisfiable and $\beta$ any variable assignment s.t. $\beta \models \phi$.

To be shown $\beta \models \psi$.

For contradiction assume $\beta \nvDash \psi$.

Then $\beta \models \neg \psi$, whch implies $\beta \models \phi \cup \{\neg \psi\}$. So $\phi \cup \{ \neg \psi\}$ satisfiable, which is a contradiction.

Is this correct?

Source of first proof

Another proof with natural deduction.

$\frac{\psi \cup \{\phi\} \models \bot}{\phi \models \neg \psi}$


$\frac{\phi \models \psi}{\phi \cup \{ \neg \psi\}\models \bot}$


If $\phi \models \psi$ then $\phi \cup \{\neg \psi\} \models \psi$.

But $\phi \cup \{\neg \psi\} \models \{ \neg \psi\}$.

Can't be satisfied, because it proves contradiction.


If $\phi \cup \{ \neg \psi\} \models \phi$ can't be satisfied, then it has no models and so $\phi \cup \{ \neg \psi\} \models \bot$

By usage of semantic completeness theorem we get $\phi \cup \{ \neg \psi \} \models \bot$.

Which by usage of natural deduction results in $\phi \models \psi$.

In the deductions I changed $\vdash$ to $\models$, is this still correct?

Source of second proof

  • 4
    $\begingroup$ You can simplify your argument if you note that $\phi \vDash \psi$ iff there is no interpretation $\mathfrak{I}$ which is a model of $\phi$ and is not a model of $\psi$. $\endgroup$
    – Lucas
    Sep 22 at 22:25
  • 4
    $\begingroup$ There are some notational difficulties here. It seems like $\phi$ is playing the role of a set of sentences, whereas $\psi$ is a sentence, but later you use $\phi$ as a sentence. I'll assume it's supposed to be a sentence. It's common sometimes to write $\phi\models \psi$ to mean the same thing as $\{\phi\}\models \psi.$ But you should always write "$\{\phi, \lnot\psi\}$ is satisfiable". It makes sense, but is somewhat odd, to write the equivalent: " $\{\phi\}\cup \{\lnot \psi\}$ is satisifiable". However, "$\phi\cup\{\lnot \psi\}$ is satisfiable" doesn't make sense unless $\phi$ is a set. $\endgroup$ Sep 22 at 22:57
  • 2
    $\begingroup$ (If it’s supposed to be a set, a better notation would be $\Phi$, but then $\Phi\land \lnot\psi$ doesn’t make sense.) $\endgroup$ Sep 22 at 23:26
  • $\begingroup$ I just consulted my script where the definition for $X \models \phi$ states that $X$ is a set of sentences and $\phi$ is a sentence. The part with $\Phi \wedge \neg \psi$ is just my question. So it's probably not correct that $\phi \cup \{ \neg \psi\}$ is the same as $\phi \wedge \neg \psi$? And it states that an interpretation has to satisfy all formulas in the resulting set from the union, i.e. $\{ \phi, \neg \psi\}$? $\endgroup$ Sep 23 at 1:16

1 Answer 1


I want to prove $\phi \models \psi$ iff $\phi \cup \{\neg \psi\}$ unsatisfiable.

What's the meaning of the union operator w.r.t. satisfiability in FOL?

We have to be careful with symbols. $a\models b$ could mean one of two things:

  • $a$ is a model, and the formula $b$ is true for $a$.
  • $a$ is a set of formulas, and for every model $\mathcal M$ that satisfies $a$, it must satisfy $b$.

In your case, it seems you mean $\phi$ is either a formula or a set of formulas. If $\phi$ is a set of (well-formed) formulas that are understood as axioms, then $\cup$ is literally the union of the two sets, that is to add $\neg\psi$ as a new axiom.

Now the statement is almost trivial: if $\phi\models \psi$, i.e. for any model $\mathcal M$ that satisfies $\phi$, it must satisfy $\psi$, hence it cannot satisfy $\neg\psi$, so $\phi\cup\{\neg\psi\}$ cannot be satisfied. If $\mathcal M$ satisfies $\phi\cup\{\neg\psi\}$, it satifies $\phi$ but not $\psi$, which contradicts the meaning of $\phi\models\psi$.

This is trivial precisely because $\vDash$ is about semantics. Only "$\phi\vdash\psi$ iff $\phi\cup\{\neg\psi\}$ cannot be satisfied" needs the Godel completeness theorem. See the difference between $\vdash$ and $\vDash$.

There seem to be many notational problems. Just to name a few, but you probably should read entire sections of your study materials more carefully.

So $\phi \cup \{\neg \psi\} \Leftrightarrow \phi \wedge \neg \psi$ ?

$\phi\wedge\neg\psi$ makese no sense, unless $\phi$ is a single formula instead of a (potentially infinite) set of formulas.

$\forall \varphi:(\beta\models \varphi) \wedge (\beta \models \neg\psi)$.

"$\forall, \wedge$" are reserved symbols in the FOL, so better to avoid using them on the meta-level. If $\beta$ is actually a model/interpretation (together with assignment for free variables if necessary), it's correct to use $\vDash$ here, but this $\vDash$ has a different meaning from the one in $\phi\vDash\psi$. Also, are you suggesting $\varphi\in\phi$?

If $\phi \cup \{ \neg \psi\} \models \phi$ can't be satisfied, then it has no models and so $\phi \cup \{ \neg \psi\} \models \bot$

It makes no sense to say whether "$a\vDash b$" can be satisfied, which is either true or false objectively. Only a set of sentences can be satisfied or not.

  • $\begingroup$ So if $\phi$ is a set of sentences and $\phi \models \psi$ iff $\phi \cup \{\neg \psi\}$ unsatisfiable it states that every model $\mathcal{M}$ which satisfies the set of sentences $\phi$ has to satisfy the sentence $\psi$ iff such models can't also satisfy the set of axioms $\phi \cup \{\neg \psi\} = \{\phi, \neg \psi\}$. $\endgroup$ Sep 23 at 2:10
  • $\begingroup$ Pretty much. Minor correction: "Every model $\mathcal M$ that satisfies each one in $\phi$ must satisfy $\psi$" iff "No model $\mathcal M$ satisfies $\phi\cup\{\neg\psi\}$" (the phrase "such models" would add confusion.). Also $\phi\cup\{\neg\psi\}\not=\{\phi,\neg\psi\}$, as the RHS is a set of two elements. E.g. $\{1,2\}\cup\{3\}$ is different from $\{\{1,2\},3\}$. $\endgroup$ Sep 23 at 3:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .