Confused by this Corollary I am reading Shawn Hedman's First Course in Logic an Introduction to Model Theory. I am confused by the proof for Corollary 1.38 on page 19.
"Corollary: If $G$ can be derived from the empty set, then $G$ is a tautology.
Proof: If $\emptyset \vdash G$, then, by Monotonicity, $\mathcal{F} \vdash  G $ for every set of formulas $\mathcal{F}$. By
Theorem 1.37 , $\mathcal{F} \models G$  for every set of formulas $\mathcal{F}$. It follows that $ \mathcal{A}\models G$ for any
assignment $\mathcal A$  and $G$ is a tautology."
I don't understand how it follows that $G$ is a tautology using Monotonicity. My guess is we could substitute a known tautology for $\mathcal F $ that is unrelated to $G$, e.g.  $ \{ C \lor \neg C \} \vdash G $. Then by Monotonicity $ \{ C \lor \neg C \} \models G $ , which reads, for all assignments $\mathcal A $, if $\mathcal A \models C \lor \neg C $ then $ \mathcal A \models G$. And since $\mathcal A \models C \lor \neg C $ because $C \lor \neg C$ is a tautology, by modens ponens we get $ \mathcal A \models G$. I am not sure about that, would like confirmation. Maybe I missed something obvious.
Also I don't understand why we need to use Monotonicity in the first place (to be fair the author never said that, I am just wondering). Can't we use the Soundness theorem directly? If $\emptyset \vdash G$ then by the Soundness theorem we get $\emptyset \models G$. If we can show $\emptyset \models G$ implies $G$ is a tautology, then we are done.
The statement $\emptyset \models G$ reads, for any assignment $\mathcal A $   if $\mathcal A \models \emptyset  $  then $\mathcal A \models G$. Equivalently if $\mathcal A(\emptyset)=1  $ then $\mathcal A(G)=1  $. But you can't assign the empty set. So maybe the conditional is vacuously true because $\mathcal A(\emptyset) $ is always $0$. I am stumped by this. Maybe we can use an equivalent form for the conditional $p \rightarrow q \equiv \neg ~p \lor q$ .
For reference, Theorem 1.37, also known as the Soundness theorem, is the statement if $ \mathcal{F } \vdash G $ then $\mathcal{ F}\models G$, and Monotonicity is a rule for proof derivation,  if $\mathcal{ F} \vdash G$ and $\mathcal{F} \subset \mathcal{F' }$ then $\mathcal{F'} \vdash G$.
 A: Here’s a more complete answer. I went to Hedman’s book to try and understand what’s going on. First, it is worth noting that you are talking about propositional logic, NOT first order logic.
I do not understand why Hedman tries to use Monotonicity. It is strictly unnecessary. Suppose that $\emptyset \vdash G$. By soundness, it follows that $\emptyset \vDash G$. Every assignment $\mathcal{A}$ trivially models $\emptyset$. Thus for every assignment we have $\mathcal{A} \vDash G$, making $G$ a tautology.

If I had to try to Guess what Hedman was thinking, I would guess he was suggesting for a given assignment $\mathcal{A}$, you could choose $\mathcal{F}$ to be a collection of formulae that are true for the assignment $\mathcal{A}$. Thus we would find that $\mathcal{A} \vDash \mathcal{F}$, and $\mathcal{F} \vDash \mathcal{G}$, proving the result.
Your argument choosing $\mathcal{F}$ to be a tautology also works.
A: Propositional calculus, by its nice metalogical properties (simultaneously holding soundness, consistency, completeness, decidability, compactness), allows us to pass from deductive derivation to logical consequence and back smoothly, which lays down a broad range of possibilities to approach a proof of a theorem. However, it should not give us the false impression that the relevant syntactic and semantic considerations are dual to each other for any argument over the system.
The main thrust of the question, as I understand it, is whether, having gripped Hedman's thread of presentation, we could show the mentioned Corollary 1.38 directly by an application of the soundness theorem without a detour through monotonicity.
Then, wWe can briefly state the sequence of inferences we need as follows:
$\mathit{G}\text{ is deducible without appealing to any particular set of hypothesis; hence }\emptyset\vdash G\iff\mathcal{A}\models\emptyset,\text{hence }\mathcal{A}\models G, \text{for }\mathit{any}\text{ model }\mathcal{A}.$
$\text{For }\mathit{any}\text{ model }\mathcal{A},\mathcal{A}\models G\iff\mathit{G}\text{ is a logical consequence without appealing to any particular model; hence }\emptyset\models G.$
It may be worth a remark that $\vDash$ is often used as a polysemous symbol: In one usage, both left-hand and right-hand sides are occupied by formulas, $\phi\vDash\psi$, the model(s) is implicitly referred (whatever model true of $\phi$ is true of $\psi$ as well). In the other, $\mathcal{M}\vDash\phi$, the model is explicitly stated. Perhaps, that is why the designers of Unicode has specified two distinct symbols, ⊧ (U+22A7, 'models') and ⊨ (U+22A8, 'true').
The critical hurdle appears to formulate "any model $\mathcal{A}$"; that is, we have to be able to systematically enlarge the set of models that satisfies $G$ from a model $\mathcal{A}$ to any model $\mathcal{A}$.
Let us expand on monotonicity  a bit. It is actually a general linguistic phenomenon of inference; simple examples to illustrate its familiarity:

*

*The antelope runs swiftly $\implies$ The antelope runs

*Some whales inhabit polar oceans $\implies$ Some mammals inhabit polar oceans

The interested may refer to Johan van Benthem and Fenrong Liu's New Logical Perspectives on Monotonicity for a logically focused treatment of this phenomenon. In logic, since we take up arguments from a formal viewpoint, adding irrelevant hypotheses is also allowed. The term monotonicity connotes semantic aspects, for the deductive contexts, weakening (or thinning) is used more often.
On the derivational side, we begin with inductive definitions, and to express monotonicity or other arguments, we have definite combinatorial methods of lengthening and multiplying formulas.
We have also methods to extend or restrict the interpretations, but not at that basic level. More precisely to say, such methods of that level will call on (composition and valuation of) formulas at some point; hence, they will be formula-driven anyhow. This is understandable; at the base of the theory, a model does not stand alone, it is always a model of a (set of) formula.
