Math and science::Theory of Computation::Modal theory
-formula implication
We wish to introduce an idea of implication between sets of
-formula.
First, we must generalize the idea of truth/satisfaction that was introduced
for -formula.
The idea of truth/satisfaction is recapped on the back side.
Model
Let be a first-order language. Let be
an -structure for and let be an
-formula of .
If for every variable assignment function
, then we say that is a model
of (or models ). We write
.
Extendion to sets of -formula: if
is a model for every -formula in a set of
-formulas, , then we say
is a model of , and we write .
If we compare two sets of -formula we arrive at a type of implication.
Logical implication, under a structure
Let and be two sets of -formulas
from the same language .
Let be an -structure for .
If implies ,
we say that
logically implies under .
In other words, if whenever all the -formulas of are satisfied by so too are the -formulas of .
Finally, we remove the dependency on a specific structure.
Logical implication
Let and be two sets of -formulas
from the same language .
If logically implies under
for any -structure of ,
then we say that logically implies .
We write this as .
Zooming out
In the presence of an -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-structure.
Recap
Recap of formula assignment.
Formula assignment: truth/satisfaction
Let be a first-order language, and let be an
-structure for the language. Let be the universe of
and let be a variable assignment function (and
the resulting term assignment function). Let be a formula valid in
.
We say that is true in ,
or that satisfies , and we
write , iff one
of the following recursive condition holds:
and the
.
and
or .
and for each element ,
.
and .
means it's not the case that .
Source
A Friendly Introduction to Mathematical Logic, by Leary and Kristiansen