2.1.14: Semantic Notions

\(\def\Assign#1#2{ { #1^{\Struct{#2}} } }\)
\(\def\Atom#1#2{ { \mathord{#1}(#2) } }\)
\(\def\Bin{ {\mathbb{B}} }\)
\(\def\cardeq#1#2{ { #1 \approx #2 } }\)
\(\def\cardle#1#2{ { #1 \preceq #2 } }\)
\(\def\cardless#1#2{ { #1 \prec #2 } }\)
\(\def\cardneq#1#2{ { #1 \not\approx #2 } }\)
\(\def\comp#1#2{ { #2 \circ #1 } }\)
\(\def\concat{ { \;\frown\; } }\)
\(\def\Cut{ { \text{Cut} } }\)
\(\def\Discharge#1#2{ { [#1]^#2 } }\)
\(\def\DischargeRule#1#2{ { \RightLabel{#1}\LeftLabel{\scriptsize{#2} } } }\)
\(\def\dom#1{ {\operatorname{dom}(#1)} }\)
\(\def\Domain#1{ {\left| \Struct{#1} \right|} }\)
\(\def\Elim#1{ { {#1}\mathrm{Elim} } }\)
\(\newcommand{\Entails}{\vDash}\)
\(\newcommand{\EntailsN}{\nvDash}\)
\(\def\eq[#1][#2]{ { #1 = #2 } }\)
\(\def\eqN[#1][#2]{ { #1 \neq #2 } }\)
\(\def\equivclass#1#2{ { #1/_{#2} } }\)
\(\def\equivrep#1#2{ { [#1]_{#2} } }\)
\(\def\Exchange{ { \text{X} } }\)
\(\def\False{ { \mathbb{F} } }\)
\(\def\FalseCl{ { \lfalse_C } }\)
\(\def\FalseInt{ { \lfalse_I } }\)
\(\def\fCenter{ { \,\Sequent\, } }\)
\(\def\fdefined{ { \;\downarrow } }\)
\(\def\fn#1{ { \operatorname{#1} } }\)
\(\def\Frm[#1]{ {\operatorname{Frm}(\Lang #1)} }\)
\(\def\fundefined{ { \;\uparrow } }\)
\(\def\funimage#1#2{ { #1[#2] } }\)
\(\def\funrestrictionto#1#2{ { #1 \restriction_{#2} } }\)
\(\newcommand{\ident}{\equiv}\)
\(\newcommand{\indcase}[2]{#1 \ident #2\text{:}}\)
\(\newcommand{\indcaseA}[2]{#1 \text{ is atomic:}}\)
\(\def\indfrm{ { A } }\)
\(\def\indfrmp{ { A } }\)
\(\def\joinrel{\mathrel{\mkern-3mu}}\)
\(\def\lambd[#1][#2]{\lambda #1 . #2}\)
\(\def\Lang#1{ { \mathcal{#1} } }\)
\(\def\LeftR#1{ { {#1}\mathrm{L} } }\)
\(\def\len#1{ {\operatorname{len}(#1)} }\)
\(\def\lexists#1#2{ { \exists #1\, #2 } }\)
\(\def\lfalse{ {\bot} }\)
\(\def\lforall#1#2{ { \forall#1\, #2 } }\)
\(\newcommand{\lif}{\rightarrow}\)
\(\newcommand{\liff}{\leftrightarrow}\)
\(\def\Log#1{ { \mathbf{#1} } }\)
\(\def\ltrue{ {\top} }\)
\(\def\Id#1{ {\operatorname{Id}_#1} }\)
\(\def\Int{ {\mathbb{Z}} }\)
\(\def\Intro#1{ { {#1}\mathrm{Intro} } }\)
\(\def\mModel#1{ { \mathfrak{#1} } }\)
\(\newcommand{\mSat}[3][{}]{\mModel{#2}{#1}\Vdash{#3}}\)
\(\newcommand{\mSatN}[3][{}]{\mModel{#2}{#1}\nVdash{#3}}\)
\(\def\Nat{ {\mathbb{N}} }\)
\(\def\nicefrac#1#2{ {{}^#1/_#2} }\)
\(\def\num#1{ { \overline{#1} } }\)

\(\def\ran#1{ {\operatorname{ran}(#1)} }\)
\(\newcommand{\Obj}[1]{\mathsf{#1}}\)
\(\def\Rat{ {\mathbb{Q}} }\)
\(\def\Real{ {\mathbb{R}} }\)
\(\def\RightR#1{ { {#1}\mathrm{R} } }\)
\(\def\Part#1#2{ { \Atom{\Obj P}{#1, #2} } }\)
\(\def\pto{ { \hspace{0.1 cm}\to\hspace{-0.44 cm}\vcenter{\tiny{\hbox{|}}}\hspace{0.35 cm} } }\)
\(\def\PosInt{ {\mathbb{Z}^+} }\)
\(\def\Pow#1{ {\wp(#1)} }\)
\(\newcommand{\Proves}{\vdash}\)
\(\newcommand{\ProvesN}{\nvdash}\)
\(\def\Relbar{\mathrel{=}}\)
\(\newcommand{\Sat}[3][{}]{\Struct{#2}{#1}\vDash{#3}}\)
\(\newcommand{\SatN}[3][{}]{\Struct{#2}{#1}\nvDash{#3}}\)
\(\newcommand{\Sequent}{\Rightarrow}\)
\(\def\Setabs#1#2{ { \{#1:#2\} } }\)
\(\newcommand{\sFmla}[2]{#1\,#2}\)
\(\def\Struct#1{ {#1} }\)
\(\def\subst#1#2{ { #1/#2 } }\)
\(\def\Subst#1#2#3{ { #1[\subst{#2}{#3}] } }\)
\(\def\TMblank{ { 0 } }\)
\(\newcommand{\TMendtape}{\triangleright}\)
\(\def\TMleft{ { L } }\)
\(\def\TMright{ { R } }\)
\(\def\TMstay{ { N } }\)
\(\def\TMstroke{ { 1 } }\)
\(\def\TMtrans#1#2#3{ { #1,#2,#3 } }\)
\(\def\Trm[#1]{ {\operatorname{Trm}(\Lang #1)} }\)
\(\def\True{ { \mathbb{T} } }\)
\(\newcommand{\TRule}[2]{#2#1}\)
\(\def\tuple#1{ {\langle #1 \rangle} }\)
\(\newcommand{\Value}[3][\,]{\mathrm{Val}_{#1}^{#3}(#2)}\)
\(\def\Var{ { \mathrm{Var} } }\)
\(\newcommand{\varAssign}[3]{#1 \sim_{#3} #2}\)
\(\def\Weakening{ { \text{W} } }\)

Give the definition of structures for first-order languages, we can define some basic semantic properties of and relationships between sentences. The simplest of these is the notion of validity of a sentence. A sentence is valid if it is satisfied in every structure. Valid sentences are those that are satisfied regardless of how the non-logical symbols in it are interpreted. Valid sentences are therefore also called logical truths—they are true, i.e., satisfied, in any structure and hence their truth depends only on the logical symbols occurring in them and their syntactic structure, but not on the non-logical symbols or their interpretation.

Definition \(\PageIndex{1}\): Validity

A sentence \(A\) is valid, \(\Entails A\), iff \(\Sat{M}{A}\) for every structure \(\Struct M\).

Definition \(\PageIndex{2}\): Entailment

A set of sentences \(\Gamma\) entails a sentence \(A\), \(\Gamma \Entails A\), iff for every structure \(\Struct M\) with \(\Sat{M}{\Gamma}\), \(\Sat{M}{A}\).

Definition \(\PageIndex{3}\): Satisfiability

A set of sentences \(\Gamma\) is satisfiable if \(\Sat{M}{\Gamma}\) for some structure \(\Struct M\). If \(\Gamma\) is not satisfiable it is called unsatisfiable.

Proposition \(\PageIndex{1}\)

A sentence \(A\) is valid iff \(\Gamma \Entails A\) for every set of sentences \(\Gamma\).

Proof. For the forward direction, let \(A\) be valid, and let \(\Gamma\) be a set of sentences. Let \(\Struct M\) be a structure so that \(\Sat{M}{\Gamma}\). Since \(A\) is valid, \(\Sat{M}{A}\), hence \(\Gamma \Entails A\).

For the contrapositive of the reverse direction, let \(A\) be invalid, so there is a structure \(\Struct M\) with \(\SatN{M}{A}\). When \(\Gamma = \{ \ltrue \}\), since \(\ltrue\) is valid, \(\Sat{M}{\Gamma}\). Hence, there is a structure \(\Struct M\) so that \(\Sat{M}{\Gamma}\) but \(\SatN{M}{A}\), hence \(\Gamma\) does not entail \(A\). ◻

Proposition \(\PageIndex{2}\)

\(\Gamma \Entails A\) iff \(\Gamma \cup \{\lnot A\}\) is unsatisfiable.

Proof. For the forward direction, suppose \(\Gamma \Entails A\) and suppose to the contrary that there is a structure \(\Struct M\) so that \(\Sat{M}{\Gamma \cup \{ \lnot A \}}\). Since \(\Sat{M}{\Gamma}\) and \(\Gamma \Entails A\), \(\Sat{M}{A}\). Also, since \(\Sat{M}{\Gamma\cup \{ \lnot A \}}\), \(\Sat{M}{\lnot A}\), so we have both \(\Sat{M}{A}\) and \(\SatN{M}{A}\), a contradiction. Hence, there can be no such structure \(\Struct M\), so \(\Gamma \cup \{ A \}\) is unsatisfiable.

For the reverse direction, suppose \(\Gamma \cup \{ \lnot A \}\) is unsatisfiable. So for every structure \(\Struct M\), either \(\SatN{M}{\Gamma}\) or \(\Sat{M}{A}\). Hence, for every structure \(\Struct M\) with \(\Sat{M}{\Gamma}\), \(\Sat{M}{A}\), so \(\Gamma \Entails A\). ◻

Problem \(\PageIndex{1}\)

1. Show that \(\Gamma \Entails \bot\) iff \(\Gamma\) is unsatisfiable.
2. Show that \(\Gamma \cup \{A\} \Entails \bot\) iff \(\Gamma \Entails \lnot A\).
3. Suppose \(c\) does not occur in \(A\) or \(\Gamma\). Show that \(\Gamma \Entails \lforall{x}{A}\) iff \(\Gamma \Entails \Subst{A}{c}{x}\).

Proposition \(\PageIndex{3}\)

If \(\Gamma \subseteq \Gamma'\) and \(\Gamma \Entails A\), then \(\Gamma' \Entails A\).

Proof. Suppose that \(\Gamma \subseteq \Gamma'\) and \(\Gamma \Entails A\). Let \(\Struct M\) be such that \(\Sat{M}{\Gamma'}\); then \(\Sat{M}{\Gamma}\), and since \(\Gamma \Entails A\), we get that \(\Sat{M}{A}\). Hence, whenever \(\Sat{M}{\Gamma'}\), \(\Sat{M}{A}\), so \(\Gamma' \Entails A\). ◻

Theorem \(\PageIndex{1}\): Semantic Deduction Theorem

\(\Gamma \cup \{A\} \Entails B\) iff \(\Gamma \Entails A \lif B\).

Proof. For the forward direction, let \(\Gamma \cup \{ A \} \Entails B\) and let \(\Struct M\) be a structure so that \(\Sat{M}{\Gamma}\). If \(\Sat{M}{A}\), then \(\Sat{M}{\Gamma \cup \{ A \} }\), so since \(\Gamma \cup \{ A \}\) entails \(B\), we get \(\Sat{M}{B}\). Therefore, \(\Sat{M}{A \lif B}\), so \(\Gamma \Entails A \lif B\).

For the reverse direction, let \(\Gamma \Entails A \lif B\) and \(\Struct M\) be a structure so that \(\Sat{M}{\Gamma \cup \{ A \}}\). Then \(\Sat{M}{\Gamma}\), so \(\Sat{M}{A \lif B}\), and since \(\Sat{M}{A}\), \(\Sat{M}{B}\). Hence, whenever \(\Sat{M}{\Gamma \cup \{ A \} }\), \(\Sat{M}{B}\), so \(\Gamma \cup \{ A \} \Entails B\). ◻

Proposition \(\PageIndex{4}\)

Let \(\Struct{M}\) be a structure, and \(A(x)\) a formula with one free variable \(x\), and \(t\) a closed term. Then:

1. \(A(t) \Entails \lexists{x}{A(x)}\)
2. \(\lforall{x}{A(x)} \Entails A(t)\)

Proof.

1. Suppose \(\Sat{M}{A(t)}\). Let \(s\) be a variable assignment with \(s(x) = \Value{t}{M}\). Then \(\Sat[,s]{M}{A(t)}\) since \(A(t)\) is a sentence. By Proposition 5.13.3, \(\Sat[,s]{M}{A(x)}\). By Proposition 5.12.4, \(\Sat{M}{\lexists{x}{A(x)}}\).
2. Exercise.

◻

Problem \(\PageIndex{2}\)

Complete the proof of Proposition \(\PageIndex{4}\).