View source for Semantics of formulas (FOL)

{{Stub page|grade=A|msg=Created to save me sifting through notes or scouring PDFs needs more references and fleshing out}}
__TOC__
==Definition==
Given a [[first order language]], {{M|\mathscr{L} }} and a {{link|model|FOL}}, {{M|(\mathbf{M},\sigma)}} also, the semantics of a {{link|formula|FOL}}, {{M|A\in\mathscr{L}_F}}, which we denote by {{M|A_{\mathbf{M}[\sigma]} }}, is [[inductive definition|defined inductively]] as follows{{rMLFFISWL}}:
: {{Note|See [[semantics of terms (FOL)|here]] for semantics of terms and [[semantics of logical connectives (FOL)|here]] for logical connectives, which are denoted {{M|\mathbf{B}_*}} for {{M|*\in\{\neg,\vee,\wedge,\rightarrow,\leftrightarrow\} }} }}
# For an ''[[arity|{{n|ary}}]]'' {{link|predicate symbol|FOL}}, {{M|P}} and {{link|term|FOL|s}}, {{M|t_1,\ldots,t_n\in\mathscr{L}_T}} the semantics are: {{M|1=(Pt_1\cdots t_n)_{\mathbf{M}[\sigma]}:=P_\mathbf{M}((t_1)_{\mathbf{M}[\sigma]},\ldots,(t_n)_{\mathbf{M}[\sigma]})}}, recall {{M|P_\mathbf{M} }} denotes {{M|I(P)}} where {{M|I}} is an {{link|interpretation|FOL}}.
# For {{link|term|FOL|s}} then {{M|t_1,t_2\in\mathscr{L}_T}}, {{M|1=(t_1\doteq t_2)_{\mathbf{M}[\sigma]}:=\left\{\begin{array}{lr}T & \text{if } (t_1)_{\mathbf{M}[\sigma]}=(t_2)_{\mathbf{M}[\sigma]}\\ F & \text{otherwise}\end{array}\right.}}, recall {{M|T}} and {{M|F}} are {{link|truth values|FOL}}
# For a {{link|formula|FOL}}, {{M|A\in\mathscr{L}_F}} then: {{M|1=(\neg A)_{\mathbf{M}[\sigma]}:=\mathbf{B}_\neg(A_{\mathbf{M}[\sigma]})}}
# For {{link|formula|FOL|s}}, {{M|A,B\in\mathscr{L}_F}} then: {{M|1=(A\vee B)_{\mathbf{M}[\sigma]}:=B_\vee(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})}}
# For {{link|formula|FOL|s}}, {{M|A,B\in\mathscr{L}_F}} then: {{M|1=(A\wedge B)_{\mathbf{M}[\sigma]}:=B_\wedge(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})}}
# For {{link|formula|FOL|s}}, {{M|A,B\in\mathscr{L}_F}} then: {{M|1=(A\rightarrow B)_{\mathbf{M}[\sigma]}:=B_\rightarrow(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})}}
# For {{link|formula|FOL|s}}, {{M|A,B\in\mathscr{L}_F}} then: {{M|1=(A\leftrightarrow B)_{\mathbf{M}[\sigma]}:=B_\leftrightarrow(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})}}
# For a {{link|formula|FOL}}, {{M|A\in\mathscr{L}_F}} and a {{link|variable symbol|FOL}}, {{M|x\in V}} then: {{M|1=(\forall xA)_{\mathbf{M}[\sigma]}:=\left\{\begin{array}{lr}T & \text{if for every }a\in M,\ A_{\mathbf{M}[\sigma[x:=a]]}=T\text{ holds}\\ F & \text{otherwise}\end{array}\right.}}
# For a {{link|formula|FOL}}, {{M|A\in\mathscr{L}_F}} and a {{link|variable symbol|FOL}}, {{M|x\in V}} then: {{M|1=(\exists xA)_{\mathbf{M}[\sigma]}:=\left\{\begin{array}{lr} T & \text{if there exists an }a\in M\text{ such that }A_{\mathbf{M}[\sigma[x:=a]]}=T\text{ holds} \\ F & \text{otherwise}\end{array}\right.}}
==See next==
* [[Satisfiable formula]]
* [[Valid formula]] ({{AKA}}: {{link|tautology|FOL}})
* [[Satisfiability and validity of formulas and sets of formulas]] - an overview of the above

==References==
<references/>
{{Formal logic navbox|plain}}
{{Definition|Formal Logic}}