Difference between revisions of "Semantics of formulas (FOL)"
From Maths
m (→See next: Added to section) |
m (→See next: Added another) |
||
| Line 17: | Line 17: | ||
* [[Valid formula]] ({{AKA}}: {{link|tautology|FOL}}) | * [[Valid formula]] ({{AKA}}: {{link|tautology|FOL}}) | ||
* [[Satisfiability and validity of formulas and sets of formulas]] - an overview of the above | * [[Satisfiability and validity of formulas and sets of formulas]] - an overview of the above | ||
| + | * {{Link|Logical consequence|FOL}} | ||
==References== | ==References== | ||
Latest revision as of 07:53, 11 September 2016
Stub grade: A
This page is a stub
This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:
Created to save me sifting through notes or scouring PDFs needs more references and fleshing out
Contents
Definition
Given a first order language, [ilmath]\mathscr{L} [/ilmath] and a model, [ilmath](\mathbf{M},\sigma)[/ilmath] also, the semantics of a formula, [ilmath]A\in\mathscr{L}_F[/ilmath], which we denote by [ilmath]A_{\mathbf{M}[\sigma]} [/ilmath], is defined inductively as follows[1]:
- See here for semantics of terms and here for logical connectives, which are denoted [ilmath]\mathbf{B}_*[/ilmath] for [ilmath]*\in\{\neg,\vee,\wedge,\rightarrow,\leftrightarrow\} [/ilmath]
- For an [ilmath]n[/ilmath]-ary predicate symbol, [ilmath]P[/ilmath] and terms, [ilmath]t_1,\ldots,t_n\in\mathscr{L}_T[/ilmath] the semantics are: [ilmath](Pt_1\cdots t_n)_{\mathbf{M}[\sigma]}:=P_\mathbf{M}((t_1)_{\mathbf{M}[\sigma]},\ldots,(t_n)_{\mathbf{M}[\sigma]})[/ilmath], recall [ilmath]P_\mathbf{M} [/ilmath] denotes [ilmath]I(P)[/ilmath] where [ilmath]I[/ilmath] is an interpretation.
- For terms then [ilmath]t_1,t_2\in\mathscr{L}_T[/ilmath], [ilmath](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.[/ilmath], recall [ilmath]T[/ilmath] and [ilmath]F[/ilmath] are truth values
- For a formula, [ilmath]A\in\mathscr{L}_F[/ilmath] then: [ilmath](\neg A)_{\mathbf{M}[\sigma]}:=\mathbf{B}_\neg(A_{\mathbf{M}[\sigma]})[/ilmath]
- For formulas, [ilmath]A,B\in\mathscr{L}_F[/ilmath] then: [ilmath](A\vee B)_{\mathbf{M}[\sigma]}:=B_\vee(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})[/ilmath]
- For formulas, [ilmath]A,B\in\mathscr{L}_F[/ilmath] then: [ilmath](A\wedge B)_{\mathbf{M}[\sigma]}:=B_\wedge(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})[/ilmath]
- For formulas, [ilmath]A,B\in\mathscr{L}_F[/ilmath] then: [ilmath](A\rightarrow B)_{\mathbf{M}[\sigma]}:=B_\rightarrow(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})[/ilmath]
- For formulas, [ilmath]A,B\in\mathscr{L}_F[/ilmath] then: [ilmath](A\leftrightarrow B)_{\mathbf{M}[\sigma]}:=B_\leftrightarrow(A_{\mathbf{M}[\sigma]},B_{\mathbf{M}[\sigma]})[/ilmath]
- For a formula, [ilmath]A\in\mathscr{L}_F[/ilmath] and a variable symbol, [ilmath]x\in V[/ilmath] then: [ilmath](\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.[/ilmath]
- For a formula, [ilmath]A\in\mathscr{L}_F[/ilmath] and a variable symbol, [ilmath]x\in V[/ilmath] then: [ilmath](\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.[/ilmath]
See next
- Satisfiable formula
- Valid formula (AKA: tautology)
- Satisfiability and validity of formulas and sets of formulas - an overview of the above
- Logical consequence
