🏗️ $\Theta \rho ϵ\eta \Pi \alpha \tau \pi$🚧 (under construction)

A first order language $ℒ$ is an infinite collection of distinct symbols, no one of which is contained in another, separated into the following categories

• Parenthesis: $(,)$
• Connectives: $\vee ,\neg$
• Quantifier: $\forall$
• Variables, one for each $i\in {\mathbb{N}}_1$: $v_i$
• Equality symbol: =
• Constant symbols: A set of symbols
• Function symbols, for each $n\in {\mathbb{N}}_1$: A set of $n$-ary function symbols
• Relation symbols, for each $n\in {\mathbb{N}}_1$: A set of $n$-ary relation symbols

Since the only thing differing from language to language are its constants, variables, functions and relations then we can denote the language $ℒ$ by $(C_{ℒ},F_{ℒ},R_{ℒ})$, we can denote the set of variables by $V_{ℒ}$

If $ℒ$ is a language, a term of $ℒ$ is a nonempty finite string $t$ of symbols from $ℒ$ such that

• $t$ is a variable
• $t$ is a constant
• $t\equiv f{t}_1{t}_2\dots t_n$ is a constant where $f$ is an $n$-ary function symbol if $ℒ$ and each $t_i$ is a term of $ℒ$

If $ℒ$ is a first order language, then a formula of $ℒ$ is a non-empty finite string $\varphi$ of symbols from $ℒ$ such that:

1. $\varphi :\equiv =t_1{t}_2$ where $t_1,t_2$ are terms of $ℒ$
2. $\varphi :\equiv R{t}_1{t}_2\dots t_n$ where $R$ is an $n$-ary relation symbol of $ℒ$ and $t_1,t_2$ are terms of $ℒ$
3. $\varphi :\equiv \left(\neg \alpha \right)$ where $\alpha$ is a formula of $ℒ$
4. $\varphi :\equiv (\alpha \vee \beta )$ where $\alpha ,\beta$ are formulas of $ℒ$
5. $\varphi :\equiv (\forall v)\left(\alpha \right)$ where $v$ is a variable and $\alpha$ is a formula of $ℒ$

The atomic formulas of $\mathcal{L}$ are formulas that satisfy clause 1 or 2 of their definition

We define the language ${ℒ}_{NT}=(\left\{\mathtt{0}\right\},\{𝚂,\mathtt{+},\mathtt{·},𝙴\},\left\{\mathtt{<}\right\})$ as the language of number theory.

Fix a language $ℒ$. An $ℒ$-structure $𝔄$ is a non-empty set $A$, called the universe of $𝔄$, such that the following holds:

• For each constant symbol $c$ of $ℒ$, we have an element $c^{𝔄}$ of $A$
• For each $n$-ary function symbol $f$ of $ℒ$, we have a function $f^{𝔄}:A^n\to A$
• For each $n$-ary relation symbol $R$ of $ℒ$, we have an $n$-ary relation $R^{𝔄}$ on $A$

Similar to a language we may denote it by $(A,\{c^{𝔄}:c\in C_{ℒ}\},\left\{f^{𝔄}:f\in F_{ℒ}\right\},\{R^{𝔄}:R\in R_{ℒ}\})$

Given ${ℒ}_{NT}$, we define the structure $𝔑:=({\mathbb{N}}_0,\left\{0\right\},\{S,+,·,E\},\{<\})$, where the constant symbol $\mathtt{0}$ maps to $0$ (the element of ${\mathbb{N}}_0$), $S$ is the successor function $S\left(2\right)=3$, $+$ is usual addition $3+3=6$, $·$ multiplication $2·4=8$, $E$ for exponentiation $E(3,2)=9$

If $𝔄$ is an $ℒ$-structure, a variable assignment function is any function of the form $s:V_{ℒ}\to A$

If $s$ is a variable assigment function into $𝔄$ and $x\in V_{ℒ}$ and $a\in A$, then $s[x\mid a]$ is the variable assigment function defined as follows and we say that $s[x\mid a]$ is an $x$-modification of the assigment function $s$

Suppose that $𝔄$ is an $L$-structure and $s$ is a variable assigment function into $𝔄$. The function $\bar{s}$, called the term assigment function generated by $s$, is the function with domain consisting of the set of $ℒ$ terms and codomain $A$ defined as follows

• if $t$ is a variable then $\bar{s}\left(t\right)=s\left(t\right)$
• if $t$ is the constant $c$ then $\bar{s}\left(t\right)=c^{𝔄}$
• if $t:\equiv f{t}_1{t}_2\dots t_n$ then $\bar{s}\left(t\right)=f^{𝔄}(\bar{s}\left(t_1\right),\bar{s}\left(t_2\right),\dots ,\bar{s}\left(t_n\right))$

Given an $ℒ$-structure $𝔄$, and a term $t$ from $ℒ$, we say that it's interpretation in $𝔄$ is $\bar{s}\left(t\right)$

Suppose that $v$ is a varaible and $\varphi$ is a formula, then $v$ is free in $\varphi$ iff exactly one of the following holds:

1. $\varphi$ is atomic and $v$ occurs in $\alpha$
2. $\varphi :\equiv \left(\neg \alpha \right)$ and $v$ is free in $\alpha$
3. $\varphi :\equiv (\alpha \vee \beta )$ and $v$ is free in at least one of $\alpha$ or $\beta$
4. $\varphi :\equiv (\forall u)\left(\alpha \right)$ and $v$ is not $u$ and $v$ is free in $\alpha$