In order to grasp the fact that there are two equivalent versions of the same theorem, I think it can be useful to review the details of a typical proof of it. See Joseph Shoenfield, Mathematical Logic (1967), page 43 :
Completeness Theorem (First Form : Gödel). A formula $A$ of a theory $T$ is a
theorem of $T$ iff it is valid in $T$ [see page 22 : By a model of a theory $T$, we mean a structure for $L(T)$ in which all the non-logical axioms of $T$ are valid (true). A formula is valid in $T$ if it is valid in every model of $T$; equivalently, if it is a logical consequence of the nonlogical axioms of $T$.]
This theorem has a second form, which concerns consistency.
Completeness Theorem (Second Form). A theory $T$ is consistent iff it has a model.
We first show that the second form of the completeness theorem implies the first.
In view of the closure theorem and its corollary, it suffices to prove the first form for a closed formula $A$.
By the corollary to the reduction theorem for consistency [see page 42], $A$ is a theorem of $T$ iff $T \cup \{ \lnot A \}$ is inconsistent.
By the second form of the completeness theorem, this holds iff $T \cup \{ \lnot A \}$ has no model. Now since $A$ is closed, a model of $T \cup \{ \lnot A \}$ is simply a model of $T$ in which $A$ is not valid. Hence $A$ is a theorem of $T$ iff $A$ is valid in every model of $T$.
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.
Best Answer
It is true that, thanks to completeness (and soundness) theorem, proving Points 1 and 2 is equivalent to prove Points 3 and 4. And your proof of Point 4 is correct. But your proof of Point 3 is not correct, and actually Point 3 (and hence Point 1) does not hold!
Where is the error in your attempt to prove Point 3? From the fact that $\mathcal{A} \models \lnot \phi$ it does not follow that $\Sigma \models \lnot \phi$. Indeed, $\Sigma \models \lnot \phi$ means that for every model $\mathcal{A}'$, if $\mathcal{A}' \models \Sigma$ then $\mathcal{A}' \models \lnot \phi$. But in your attempt to prove Point 3, you have just shown that there exists a model $\mathcal{A}$ such that $\mathcal{A} \models \Sigma$ and $\mathcal{A} \models \lnot \phi$. A priori, it is still possible that there is another model $\mathcal{B}\models \Sigma$ such that $\mathcal{B} \models \phi$, your argument does not exclude this possibility. And actually this is what actually happens!
Why Point 3 does not hold? Suppose that $\Sigma$ is the set of axioms defining a group (it can be easily expressed in first-order logic, see here), and that $\phi$ is the formula expressing that the group is abelian. Clearly, $\Sigma \not\models \phi$ because not all groups are abelian, but from that it does not follow that $\Sigma \models \lnot \phi$ because it is not true that all groups are non-abelian.