\( \mathcal{L} \)-formula implication
We wish to introduce an idea of implication between sets of \( \mathcal{L} \)-formula.
First, we must generalize the idea of truth/satisfaction that was introduced for \( \mathcal{L} \)-formula.
The idea of truth/satisfaction is recapped on the back side.
Model
Let \( \mathcal{L} \) be a first-order language. Let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for \( \mathcal{L} \) and let \( \phi \) be an \( \mathcal{L} \)-formula of \( \mathcal{L} \).
If \( \mathfrak{U} \vDash \phi[s] \) for every variable assignment function \( s \), then we say that \( \mathfrak{U} \) is a model of \( \phi \) (or \( \mathfrak{U} \) models \( \phi \)). We write \( \mathfrak{U} \vDash \phi \).
Extendion to sets of \( \mathcal{L} \)-formula: if \( \mathfrak{U} \) is a model for every \( \mathcal{L} \)-formula in a set of \( \mathcal{L} \)-formulas, \( \Phi \), then we say \( \mathfrak{U} \) is a model of \( \Phi \), and we write \( \mathfrak{U} \vDash \Phi \).
If we compare two sets of \( \mathcal{L} \)-formula we arrive at a type of implication.
Logical implication, under a structure
Let \( \Delta \) and \( \Gamma \) be two sets of \( \mathcal{L} \)-formulas from the same language \( \mathcal{L} \). Let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for \( \mathcal{L} \).
If \( \mathfrak{U} \vDash \Delta \) implies \( \mathfrak{U} \vDash \Gamma \), we say that \( \Delta \) logically implies \( \Gamma \) under \( \mathfrak{U} \).
In other words, if whenever all the \( \mathcal{L} \)-formulas of \( \Delta \) are satisfied by \( \mathfrak{U} \) so too are the \( \mathcal{L} \)-formulas of \( \Gamma \).
Finally, we remove the dependency on a specific structure.
Logical implication
Let \( \Delta \) and \( \Gamma \) be two sets of \( \mathcal{L} \)-formulas from the same language \( \mathcal{L} \).
If \( \Delta \) logically implies \( \Gamma \) under \( \mathfrak{U} \) for any \( \mathcal{L} \)-structure \( \mathfrak{U} \) of \( \mathcal{L} \), then we say that \( \Delta \) logically implies \( \Gamma \). We write this as \( \Delta \vDash \Gamma \).
Zooming out
In the presence of an \( \mathcal{L} \)-structure and a variable assignment function, the terms and formulas of a first-order language have been assigned meaning. Terms are mapped to elements of the universe, and formulas are assigned to the idea of being true or false. In this setting, if we compare two formulas and observe a truth table implication, we can call this implication between formulas within the setting of the semantic assignments. This implication is strengthened if it is independent of the variable assignment function, and it is strengthened again if it is independent of any particular structure. If our implication is independent of structure, then we have achieved an implication that is not tied to the semantic structure of sets, instead the syntax is sufficient to conclude implication. This isn't quite true! The implication is still tied to the assumption that truth is decided relative to some \( \mathcal{L} \)-structure.
Recap
Recap of formula assignment.
Formula assignment: truth/satisfaction
Let \( \mathcal{L} \) be a first-order language, and let \( \mathfrak{U} \) be an \( \mathcal{L} \)-structure for the language. Let \( A \) be the universe of \( \mathfrak{U} \) and let \( s \) be a variable assignment function (and \( \bar{s} \) the resulting term assignment function). Let \( \phi \) be a formula valid in \( \mathcal{L} \).
We say that \( \phi \) is true in \( \mathfrak{U} \), or that \( \mathfrak{U} \) satisfies \( \phi \), and we write \( \mathfrak{U} \vDash \phi \), iff one of the following recursive condition holds:
- \( \phi :\equiv Rt_1t_2...t_n \) and the \( (\bar{s}(t_1), \bar{s}(t_2), ..., \bar{s}(t_n)) \in R^{\mathfrak{u}} \).
- \( \phi :\equiv (\alpha \lor \beta) \) and \( \mathfrak{U} \vDash \alpha \) or \( \mathfrak{U} \vDash \beta \).
- \( \phi :\equiv \forall x \; (\alpha) \) and for each element \( a \in A \), \( \mathfrak{U} \vDash \alpha[s(x|a)] \).
- \( \phi :\equiv \lnot \alpha (\lnot \alpha) \) and \( \mathfrak{U} \nvDash \alpha[s] \).
\( \mathfrak{U} \nvDash \phi \) means it's not the case that \( \mathfrak{U} \vDash \phi \).