💡 A proof system is a quadruple $\Pi =(\mathcal{S},\mathcal{P},\tau ,\varphi )$, as above.

💡 A proof system $\Pi =(\mathcal{S},\mathcal{P},\tau ,\varphi )$ is sound if no false statement has a proof, i.e., if for all $s\in \mathcal{S}$ for which there exists $p\in \mathcal{P}$ with $\varphi (s,p)=1$, we have $\tau (s)=1$.

💡 A proof system $\Pi =(\mathcal{S},\mathcal{P},\tau ,\varphi )$ is complete if every true statement has a proof, i.e., if for all $s\in \mathcal{S}$ with $\tau (s)=1$, there exists $p\in \mathcal{P}$ with $\varphi (s,p)=1$.

💡 A goal of logic is to provide a specific proof system $\Pi =(\mathcal{S},\mathcal{P},\tau ,\varphi )$ for which a very large class of mathematical statements can be expressed as an element of $\mathcal{S}$.

💡 The syntax of a logic defines an alphabet $\Lambda$ (of allowed symbols) and specifies which strings in ${\Lambda }^{\ast }$ are formulas (i.e., are syntactically correct).

💡 The semantics of a logic defines (among other things) a function $\text{free}$ which assigns to each formula $F=(f_1,f_2,\dots ,f_k)\in {\Lambda }^{\ast }$ a subset $\text{free}(F)\subseteq \{1,\dots ,k\}$ of the indices. If $i\in \text{free}(F)$, then the symbol $f_i$ is said to occur free in $F$.

💡 An interpretation consists of a set $\mathcal{Z}\subseteq \Lambda$ of symbols of $\Lambda$, a domain (a set of possible values) for each symbol in $\mathcal{Z}$, and a function that assigns to each symbol in $\mathcal{Z}$ a value in its associated domain.

💡 An interpretation is suitable for a formula $F$ if it assigns a value to all symbols $\beta \in \Lambda$ occurring free in $F$.

💡 The semantics of a logic also defines a function $\sigma$ assigning to each formula $F$, and each interpretation $\mathcal{A}$ suitable for $F$, a truth value $\sigma (\mathcal{F},\mathcal{A})$ in $\{0,1\}$. In treatments of logic one often writes $\mathcal{A}(F)$ instead of $\sigma (\mathcal{F},\mathcal{A})$ and calls $\mathcal{A}(F)$ the truth value of $F$ under interpretation $\mathcal{A}$.

💡 A (suitable) interpretation $\mathcal{A}$ for which a formula $F$ is true, (i.e., $\mathcal{A}(F)=1$) is called a model for $F$, and one also writes

$$\mathcal{A}\models F.$$

More generally, for a set $M$ of formulas, a (suitable) interpretation for which all formulas in $M$ are true is called a model for $M$, denoted as

$$\mathcal{A}\models M.$$

If $\mathcal{A}$ is not a model for $M$ one writes $\mathcal{A}\cancel{\models }M$.

💡 A formula $F$ (or a set $M$ of formulas) is called satisfiable if there exists a model for $F$ (or $M$), and unsatisfiable otherwise. The symbol $\perp$ is used for an unsatisfiable formula.

💡 A formula $F$ is called a tautology or valid if it is true for every suitable interpretation. The symbol $\top$ is used for a tautology.

💡 A formula $G$ is a logical consequence of a formula $F$ (or a set $M$ of formulas), denoted

$$F\models G(\text{or}M\models G),$$

if every interpretation suitable for both $F$ (or $M$) and $G$, which is a model for $F$ (for $M$), is also a model for $G$.

💡 Two formulas $F$ and $G$ are equivalent, denoted $F\equiv G$, if every interpretation suitable for both $F$ and $G$ yields the same truth value for $F$ and $G$, i.e., if each one is a logical consequence of the other:

$$F\equiv G\stackrel{\mathrm{def}}{⟺}F\models G\text{and}G\models F.$$

💡 If $F$ is a tautology, one also writes $\models F$.

💡 If $F$ and $G$ are formulas, then also $\neg F,(F\wedge G)$ and $(F\vee G)$ are formulas.

💡 $\mathcal{A}((F\wedge G))=1$ if and only if $\mathcal{A}(F)=1$ and $\mathcal{A}(G)=1$. $\mathcal{A}((F\vee G))=1$ if and only if $\mathcal{A}(F)=1$ or $\mathcal{A}(G)=1$. $\mathcal{A}(\neg F)=1$ if and only if $\mathcal{A}(F)=0$

📌 For any formulas $F$, $G$ and $H$ we have

1. $\ast F\wedge F\equiv F$ and $F\vee F\equiv F$ (idempotence)*
2. $\ast F\wedge G\equiv G\wedge F$ and $F\vee G\equiv G\vee F$ (commutativity)*
3. $\ast (F\wedge G)\wedge H\equiv F\wedge (G\wedge H)$ and $(F\vee G)\vee H\equiv F\vee (G\vee H)$ (associativity)*
4. $\ast F\wedge (F\vee G)\equiv F$ and $F\vee (F\wedge G)\equiv F$ (absorption)*
5. $\ast F\wedge (G\vee H)\equiv (F\wedge G)\vee (F\wedge H)$ (distributive law)*
6. $\ast F\vee (G\wedge H)\equiv (F\vee G)\wedge (F\vee H)$ (distributive law)*
7. $\neg \neg F\equiv F$ (double negation)
8. $\ast \neg (F\wedge G)\equiv \neg F\vee \neg G$ and $\neg (F\vee G)\equiv \neg F\wedge \neg G$ (de Morgan’s rules)*
9. $\ast F\vee \top \equiv \top$ and $F\wedge T\equiv F$ (tautology rules)*
10. $\ast F\vee \perp \equiv F$ and $F\wedge \perp \equiv \perp$ (unsatisfiability rules)*
11. $F\vee \neg F\equiv \top$ and $F\wedge \neg F\equiv \perp$.

📌 A formula $F$ is a tautology if and only if $\neg F$ is unsatisfiable.

📌 The following three statements are equivalent:

1. $\{F_1,F_2,\dots ,F_k\}\models G$
2. $\ast \{F_1\wedge F_2\wedge \dots \wedge F_k\}\to G$ is a tautology*
3. $\ast \{F_1,F_2,\dots ,F_k,\neg G\}$ is unsatisfiable*

💡 A derivation rule is a rule for deriving a formula from a set of formulas (called the precondition). We write

$$\{F_1,\dots ,F_k\}{⊢}_{R}G$$

if G can be derived from the set $\{F_1,\dots ,F_k\}$ by rule $R$.

💡 (Informal.) The application of a derivation rule $R$ to a set $M$ of formulas means

1. Select a subset $N$ of $M$.
2. For the place-holders in $R$: specify formulas that appear in $N$ such that $N{⊢}_{R}G$ for a formula $G$.
3. Add $G$ to the set $M$ (i.e., replace $M$ by $M\cup \{G\}$).

💡 A (logical) calculus $K$ is a finite set of derivation rules: $K=\{R_1,\dots ,R_m\}$.

💡 A derivation of a formula $G$ from a set $M$ of formulas in a calculus $K$ is a finite sequence (of some length $n$) of applications of rules in $K$, leading to $G$. More precisely, we have

• $M_0:=M$
• $M_i:=M_{i-1}\cup \{G_i\}$ for $1\le i\le n$, where $N{⊢}_{R_i}{G}_i$ for some $N\subseteq M_{i-1}$ and for some $R_j\in K$, and where
• $G_n=G$

We write

$$M{⊢}_{K}G$$

if there is a derivation of $G$ from $M$ in the calculus $K$.

💡 A derivation rule $R$ is correct if for every set $M$ of formulas and every formula $F$, $M{⊢}_{R}F$ implies $M\models F$:

$$M{⊢}_{R}F⟹M\models F.$$

💡 A calculus $K$ is sound or correct if for every set $M$ of formulas and every formula $F$, if $F$ can be derived from $M$ then $F$ is also a logical consequence of $M$:

$$M{⊢}_{K}F⟹M\models F,$$

and $K$ is complete if for every $M$ and $F$, if $F$ is a logical consequence of $M$, then $F$ can also be derived from $M$:

$$M\models F⟹M{⊢}_{K}F.$$

A calculus $K$ is hence sound and complete if

$$M{⊢}_{K}F⟺M\models F$$

i.e., if logical consequence and derivability are identical. Clearly, a calculus is sound if and only if every derivation rule is correct. One writes ${⊢}_{K}F$ if $F$ can be derived in $K$ from the empty set of formulas. Note that if ${⊢}_{K}F$ for a sound calculus, then $\models F$, i.e., $F$ is a tautology.

📌 If $\{F_1,\dots ,F_k\}{⊢}_{K}G$ holds for a sound calculus, then

$$\models ((F_1\wedge \dots \wedge F_k)\to G).$$

💡 (Syntax.) An atomic formula is of the form $A_i$ with $i\in \mathbb{N}$. A formula is defined as follows:

• An atomic fomula is a formula.
• If $F$ and $G$ are formulas, then also $\neg F,(F\wedge G)$ and $(F\vee G)$ are formulas.

💡 (Semantics.) For a set $Z$ of atomic formulas, an interpretation $\mathcal{A}$, called truth assignment, is a function $\mathcal{A}:Z⟶\{0,1\}$. A truth assignment $\mathcal{A}$ is suitable for a formula $F$ if $Z$ contains all atomic formulas appearing in $F$. The semantics (i.e., the truth value $\mathcal{A}(F)$ of a formula $F$ under interpretation $\mathcal{A}$) is defined by $\mathcal{A}(F)=\mathcal{A}(A_i)$ for any atomic formula $F=A_i$,

💡 A literal is an atomic formula or the negation of an atomic formula.

💡 A formula $F$ is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals, i.e., if it is of the form

$$F=(L_{11}\vee \dots \vee L_{1m_1})\wedge \dots \wedge (L_{n1}\vee \dots \vee L_{n{m}_n})$$

for some literals $L_{ij}$.

💡 A formula $F$ is in disjunctive normal form (DNF) if it is a disjunction of conjunctions of literals, i.e., if it is of the form

$$F=(L_{11}\wedge \dots \wedge L_{1m_1})\vee \dots \vee (L_{n1}\wedge \dots \wedge L_{n{m}_n})$$

for some literals $L_{ij}$.

📖 Every formula is equivalent to a formula in CNF and also to a formula in DNF.

💡 A clause is a set of literals.

💡 The set of clauses associated to a formula

$$F=(L_{11}\wedge \dots \wedge L_{1m_1})\vee \dots \vee (L_{n1}\wedge \dots \wedge L_{n{m}_n})$$

in CNF, denoted as $\mathcal{K}(F)$, is the set

$$\mathcal{K}(F)\stackrel{\mathrm{def}}{=}\{\{L_{11},\dots ,L_{1m_1}\},\dots ,\{L_{n1},\dots ,L_{n{m}_n}\}\}.$$

The set of clauses associated with a set $M=\{F_1,\dots F_k\}$ of formulas is the union of their clause sets:

$$\mathcal{K}(M)\stackrel{\mathrm{def}}{=}\bigcup _{i=1}^k\mathcal{K}(F_i).$$

💡 A clause $K$ is a resolvent of clauses $K_1$ and $K_2$ if there is a literal $L$ such that $L\in K_1$, $\neg L\in K_2$, and

$$K=(K_1\setminus \{L\})\cup (K_2\setminus \{\neg L\}).$$

📌 The resolution calculus is sound, i.e., if $\mathcal{K}{⊢}_{\text{Res}}K$ then $\mathcal{K}\models K$.

📖 A set $M$ of formulas is unsatisfiable if and only if $\mathcal{K}(M){⊢}_{\text{Res}}\varnothing$.

💡 (Syntax of predicate logic.)

• A variable symbol is of the form $x_i$ with $i\in \mathbb{N}$.
• A function symbol is of the form $f_i^{(k)}$ with $i,k\in \mathbb{N}$, where $k$ denotes the number of arguments of the function. Function symbols for $k=0$ are called constants.
• A predicate symbol is of the form $P_i^{(k)}$ with $i,k\in \mathbb{N}$, where $k$ denotes the number of arguments of the predicate.
• A term is defined inductively: A variable is a term, and if $t_1,\dots ,t_k$ are terms, then $f_i^{(k)}(t_1,\dots ,t_k)$ is a term. For $k=0$ one writes no parentheses.
• A formula is defined inductively:
  • For any $i$ and $k$, if $t_1,\dots ,t_k$ are terms, then $P_i^{(k)}(t_1,\dots ,t_k)$ is a formula, called an atomic formula
  • If $F$ and $G$ are formulas, then $\neg F$, $(F\wedge G)$, and $(F\vee G)$ are formulas.
  • If $F$ is a formula, then, for any $i$, $\forall x_{i}F$ and $\exists x_{i}F$ are formulas.

💡 Every occurrence of a variable in a formula is either bound or free. If a variable $x$ occurs in a (sub-) formula of the form $\forall xG$ or $\exists xG$, then it is bound, otherwise it is free. A formula is closed if it contains no free variables.

💡 For a formula $F$, a variable $x$ and a term $t$, $F[x/t]$ denotes the formula obtained from $F$ by substituting every free occurrence of $x$ by $t$.

💡 An interpretation or structure is a tuple $\mathcal{A}=(U,\varphi ,\psi ,\xi )$ where

• $U$ is a non-empty set, the so-called universe
• $\varphi$ is a function assigning to each function symbol (in a certain subset of all function symbols) a function, where for $k$-ary function symbol $f$. $\varphi (f)$ is a function
• $\psi$ is a function assigning to each predicate symbol (in a certain subset of all predicate symbols) a function, where for a $k$-ary predicate symbol $P$, $\psi (P)$ is a function $U^k⟶\{0,1\}$
• $\xi$ is a function assigning to each variable symbol (in a certain subset of all variable symbols) a value in $U$.

💡 An interpretation (structure) $\mathcal{A}$ is suitable for a formula $F$ if it defines all function symbols, predicate symbols, and freely occurring variables of $F$.

💡 (Semantics.) For an interpretation (structure) $\mathcal{A}=(U,\varphi ,\psi ,\xi )$, we define the value (in $U$) of terms and the truth value of formulas under that structure.

• The value $\mathcal{A}(t)$ of a term $t$ is defined recursively as follows:
  • If $t$ is a variable, i.e., $t=x_i$, then $\mathcal{A}(t)=\xi (x_i)$.
  • If $t$ is of the form $f(t_1,\dots ,t_k)$ for terms $t_1,\dots ,t_k$ and a $k$-ary function symbol $f$, then $\mathcal{A}(t)=\varphi (f)(\mathcal{A}(t_1),\dots ,\mathcal{A}(t_k))$.
• The truth value of a formula $F$ is defined recursively by

and

• If $F$ is of the form $F=P(t_1,\dots ,t_k)$ for terms $t_1,\dots ,t_k$ and a $k$-ary predicate symbol $P$, then $\mathcal{A}(F)=\psi (P)(\mathcal{A}(t_1),\dots ,\mathcal{A}(t_k))$.
• If $F$ is of the form $\forall xG$ or $\exists xG$, then let ${\mathcal{A}}_{[x\to u]}$ for $u\in U$ be the same structure as $\mathcal{A}$ except that $\xi (x)$ is overwritten by $u$ (i.e., $\xi (x)=u$):

$$\begin{array}{rl}\mathcal{A}(\forall xG)& =\{\begin{array}{ll}1& \text{if A[x→u](G)=1 for all u∈U}\\ 0& \text{else}\end{array}\\ \mathcal{A}(\exists xG)& =\{\begin{array}{ll}1& \text{if A[x→u](G)=1 for some u∈U}\\ 0& \text{else}\end{array}\end{array}$$

📌 For any formulas $F$, $G$ and $H$, where $x$ does not occur free in $H$, we have

1. $\neg (\forall xF)\equiv \exists x\neg F$
2. $\neg (\exists xF)\equiv \forall x\neg F$
3. $(\forall xF)\wedge (\forall xG)\equiv \forall x(F\wedge G)$
4. $(\exists xF)\vee (\exists xG)\equiv \exists x(F\vee G)$
5. $\forall x\forall yF\equiv \forall y\forall xF$
6. $\exists x\exists yF\equiv \exists y\exists xF$
7. $(\forall xF)\wedge H\equiv \forall x(F\wedge H)$
8. $(\forall xF)\vee H\equiv \forall x(F\vee H)$
9. $(\exists xF)\wedge H\equiv \exists x(F\wedge H)$
10. $(\exists xF)\vee H\equiv \exists x(F\vee H)$

📌 If one replaces a sub-formula $G$ of a formula $F$ by an equivalent (to $G$) formula $H$, then the resulting formula is equivalent to $F$.

📌 For a formula $G$ in which $y$ does not occur, we have

• $\forall xG\equiv \forall yG[x/y]$
• $\exists xG\equiv \exists yG[x/y]$

💡 A formula in which no variable occurs both as a bound and as a free variable and in which all variables appearing after the quantifiers are distinct is said to be in rectified form.

📌 For any formula $F$ and any term $t$ we have

$$\forall xF\models F[x/t].$$

💡 A formula of the form

$$Q_1{x}_1{Q}_2{x}_2\dots Q_n{x}_{n}G$$

where the $Q_i$ are arbitrary quantifiers ($\forall$ or $\exists$) and $G$ is a formula free of quantifiers, is said to be in prenex form.

💡 In order to transform a formula into prenex form one first transforms the formula into an equivalent formula in rectified from and then applies the following equivalences

to move up all quantifiers in the formula tree, resulting in a prenex form of the formula.

📖 For every formula there is an equivalent formula in prenex form.

📖 $\neg \exists x\forall y(P(y,x)\leftrightarrow \neg P(y,y))$

📎 There exists no set that contains all sets $S$ that do not contain themselves, i.e., $\{S|S\notin S\}$ is not a set.

📎 The set $\{0,1{\}}^{\infty }$ is uncountable.

📎 There are uncomputable functions $\mathbb{N}⟶\{0,1\}.$

📎 The function $\mathbb{N}⟶\{0,1\}$ assigning to each $y\in \mathbb{N}$ the complement of what program $y$ outputs on input $y$, is uncomputable.