Usually classical first-order logic is defined so that classical propositional logic is a literal sublanguage of it. In particular, it is the sublanguage where all relation symbols are nullary (and omitting quantifiers which are essentially useless at that point). This makes it impossible for there to be any place to put terms. Semantically, it then doesn't matter what the domain is as there is no way to refer to any of its elements. The tautological implication relation is the logical implication relation restricted to this sublanguage.
Nevertheless, what you describe works insofar as the theorem in your last bullet holds, but it is kind of a weird way to go about it. You can improve and simplify it by making it a first-order theory rather than constraining the interpretation in an ad-hoc manner. You could add the axioms $\exists x.P(x)$ and $\exists x.\neg P(x)$ which would ensure the domain contains at least two elements and the interpretation of $P$ is non-empty and has a non-empty complement. It may be a bit clearer to just explicitly add two constants $\mathsf{tt}$ and $\mathsf{ff}$ and the axioms $P(\mathsf{tt})$, $\neg P(\mathsf{ff})$, and $\mathsf{tt}\neq\mathsf{ff}$.
There are many other ways to map propositional formulas to FOL formulas such that the original formulas are tautologies if and only if the resulting formula is valid. One notable one is to simply formalize the notion of a Boolean algebra. Alternatively, if you went the route you did because Enderton doesn't allow for nullary relation symbols (or maybe it just didn't occur to you), you could do essentially the same thing I suggested but producing distinct unary predicates for each propositional variable (sentence symbol). Then, to get effectively nullary predicates you could map the propositional variables to formulas like $\forall x.P_n(x)$ (or instead $\exists x.P_n(x)$ or $P_n(\mathsf{c})$ after adding a constant $\mathsf{c}$). This is clearly a bit of a hack to make up for not directly having nullary relation symbols.
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
The inference $\exists x (\phi(x) \to \psi(x)) \nvDash \exists x\phi(x) \to \exists x \psi(x)$ is invalid because there exists a counter model:
Let the domain be $\{a, b\}$ and $\phi$ true of $a$ but not of $b$, and $\psi$ true of none of the elements.
Then for $x \mapsto b$, $\phi(x)$ is false so $\phi(x) \to \psi(x)$ is true, so $\exists x (\phi(x) \to \psi(x))$ is true.
But $\exists x \phi(x)$ is true with $x \mapsto a$ whereas $\exists x \psi(x)$ is false since $\psi$ is true of neither $a$ nor $b$, so $\exists x \phi(x) \to \exists x \psi(x)$ is false.
Since in this structure the premise is true but the conclusion is false, the inference is invalid.
The inference $\exists x (\phi(x) \to \psi(x)) \vDash \forall x\phi(x) \to \exists x \psi(x)$ is valid by the following reasoning:
By assumption, $\phi(x) \to \psi(x)$ holds of some object; let it be $y$. Assume $\forall x \phi(x)$, then in particular $\phi$ holds of $y$. By modus ponens, $\psi$ must also be true of $y$. Hence there exists an object of which $\psi$ holds, so $\exists x \psi(x)$ is true. Thus $\forall x \phi(x) \to \exists x \psi(x)$. Since an object such as $y$ is assumed to exist, $\forall x \phi(x) \to \exists x \psi(x)$ holds regardless of which particular object $\phi(x) \to \psi(x)$ is true of.
As an exercise, you can now try to translate this informal proof into a natural deduction proof.