First-Order Logic

logic

Definition

First-Order Logic

First Order Logic (FOL) is a formal system used in mathematics, philosophy, linguistics, and computer science to represent reason about propositons involving objects and their relationships. It extends propositional logic by incorporating quantifiers and predicates, enabling more expressive steatement about the properties and relatiolns between objects within a particular domain.

Universe

Syntax

Syntax of Propositional Formulas

The syntax is constructed from a tuple called the signature:

$$(\mathcal{F},\mathcal{P})$$

where $\mathcal{F}$ is the set of functions and $\mathcal{P}$ is the set of predicates.

The set of first-order logic formulas $\mathcal{P}\mathcal{F}$ over a signature $\mathcal{F},\mathcal{P}$ is defined as the smallest set such that:

$$\begin{array}{rl}P\in \mathcal{P}\mathcal{F}& ⟺P/0\in \mathcal{P}\\ P(t_1,\dots ,t_n)\in \mathcal{P}\mathcal{F}& ⟺P/n\in \mathcal{P}\wedge t_1,\dots ,t_n\in \mathcal{T}(\mathcal{F},\mathcal{V})\\ \top ,\perp \in \mathcal{P}\mathcal{F}& \\ \neg F\in \mathcal{P}\mathcal{F}& ⟺F\in \mathcal{P}\mathcal{F}\\ (F\ast G)\in \mathcal{P}\mathcal{F}& ⟺F,G\in \mathcal{P}\mathcal{F}\wedge \ast \in \{\wedge ,\uparrow ,\vee ,\downarrow ,\iff ,\nLeftrightarrow ,⟹,⟸\}\\ \forall xF\in \mathcal{P}\mathcal{F}& ⟺x\in \mathcal{V}\wedge F\in \mathcal{P}\mathcal{F}\\ \exists xF\in \mathcal{P}\mathcal{F}& ⟺x\in \mathcal{V}\wedge F\in \mathcal{P}\mathcal{F}\end{array}$$

where $\mathcal{T}(\mathcal{F},\mathcal{V})$ is the term language over $\mathcal{F}$ and $\mathcal{V}$. Note that the definition of * might differ depending on the literature.

Note that $F/n$ denotes the arity of $F$.

Semantics

Semantics of Propositional Formulas

Semantics are introduced using an interpretation $I$, a variable assignment $\sigma$ and a function ${\mathrm{val}}_{I,\sigma }$

The value function ${\mathrm{val}}_{I,\sigma }$ is defined as:

$$\begin{array}{rl}{\mathrm{val}}_{I,\sigma }(P)& =I(P)\text{for}P/0\in \mathcal{P}\\ {\mathrm{val}}_{I,\sigma }(P(t_1,\dots ,t_n))& ={\mathrm{val}}_{I,\sigma }(P/n)({\mathrm{val}}_{I,\sigma }(t_1),\dots ,{\mathrm{val}}_{I,\sigma }(t_n))\\ {\mathrm{val}}_{I,\sigma }(\top )& =1\\ {\mathrm{val}}_{I,\sigma }(\perp )& =0\\ {\mathrm{val}}_{I,\sigma }(\neg P)& =\neg {\mathrm{val}}_{I,\sigma }(P)\\ {\mathrm{val}}_{I,\sigma }(P\ast Q)& ={\mathrm{val}}_{I,\sigma }(P)⊛{\mathrm{val}}_{I,\sigma }(Q)\\ {\mathrm{val}}_{I,\sigma }(\forall xF)& =\{\begin{array}{ll}1& \text{if}{\mathrm{val}}_{I,\sigma }(F)=1\forall {\sigma }^{\prime }\stackrel{x}{\sim }\sigma \\ 0& \text{else}\end{array}\\ {\mathrm{val}}_{I,\sigma }(\exists xF)& =\{\begin{array}{ll}1& \text{if}{\mathrm{val}}_{I,\sigma }(F)=1\exists {\sigma }^{\prime }\stackrel{x}{\sim }\sigma \\ 0& \text{else}\end{array}\end{array}$$

where $⊛$ is the boolean function of operator $\ast$.

The notation ${\sigma }^{\prime }\stackrel{x}{\sim }\sigma$ means that ${\sigma }^{\prime }$ is a variable assignment that is equal to $\sigma$ except for the value of $x$.

Variant Notation

Variant Notation

The ${\sigma }^{\prime }\stackrel{x}{\sim }\sigma$ notation does not have a standard name r at least I cannot find one.

It expresses that ${\sigma }^{\prime },\sigma$ are a variable assigment that only differs in the value of variable $x$. The word “differs” is confusing here because “differs” means that all other variables are fixed and only $x$ varies, meaning that ${\sigma }^{\prime }\stackrel{x}{\sim }\sigma$ means there also exists a ${\sigma }^{\prime }$ where ${\sigma }^{\prime }(x)=\sigma (x)$.

Model

Model

The tuple $(I,\sigma )$, where $I$ is an interpretation of and interprets $F$ and $\sigma$ is a value assignment. is called a model of a formula $F$.