Logical preliminaries   First order logic

First order logic   (written by Joanna Golińska Pilarek)

Classical Propositional Logic $\mathsf{PC}$

Formalism description Formulas of the classical propositional logic $\mathsf{PC}$ are generated by the following abstract syntax: \[p \, |\, \neg \varphi \, |\, \varphi \vee \psi \, | \, \varphi \wedge \psi \, | \, \varphi \rightarrow \psi\] where $p$ belongs to a countable infinite set of propositional variables $\mathsf{VP}$.

Connectives $\vee$ and $\wedge$ are definable by $\neg$ and $\rightarrow$.

Let $\{0, 1\}$ be the set of truth-values ''false'' and ''true'', respectively. A $\mathsf{PC}$-valuation is any mapping $v: \mbox{VP} \mapsto \{0, 1\}$. The valuation $v$ is extended to all formulas of $\mathsf{PC}$ as usual:

• $v(\neg \varphi) = 1- v(\varphi)$
• $v(\varphi \vee \psi) = \max(v(\varphi), v(\psi))$
• $v(\varphi \wedge \psi) = \min(v(\varphi), v(\psi))$
• $v(\varphi \rightarrow \psi) \max(1-v(\varphi), v(\psi))$

A formula $\varphi$ is $\mathsf{PC}$-satisfied by $v$ whenever $v(\varphi) = 1$ and it is $\mathsf{PC}$-valid whenever it is satisfied by all valuations.

The Hilbert-style axiomatization of $\mathsf{PC}$ contains the following axioms

(Ax1) $(\varphi \rightarrow \psi)\rightarrow [(\psi \rightarrow \vartheta)\rightarrow (\varphi \rightarrow \vartheta)]$
(Ax2) $(\neg \varphi \rightarrow \varphi)\rightarrow \varphi$
(Ax3) $\varphi \rightarrow (\neg \varphi \rightarrow \psi)$

The rule of the system is modus ponens.

A derivation of a formula $\varphi$ from a set $X$ of $\mathsf{PC}$-formulas is a finite sequence $\{\psi_1, \ldots, \psi_n\}$ of $\mathsf{PC}$-formulas such that $\psi_n = \varphi$ and for every $i \in \{1, \ldots, n\}$:

• either $\psi_i \in X$,
• or $\psi_i$ is an axiom,
• or $\psi_i$ is obtained from $\{\psi_1, \ldots, \psi_{i-1}\}$ by an application of the rule.

A formula $\varphi$ is said to be $\mathsf{PC}$-provable whenever there exists a derivation of $\varphi$ from the empty set of $\mathsf{PC}$-formulas.

Theorem 1 (Completeness and soundness of $\mathsf{PC}$) The logic $\mathsf{PC}$ is sound and complete, that is for every $\mathsf{PC}$-formula $\varphi$ the following conditions are equivalent:

• $\varphi$ is $\mathsf{PC}$-provable.
• $\varphi$ is $\mathsf{PC}$-valid.

First-order logic with identity

Formalism description The vocabulary of the first-order logic $\mathsf F$ with identity consists of:

• a countable set of individual variables $\mathsf{V}$;
• for every $k \in \omega, k \geq 1$, a countable set $\mathsf{P}_{k}$ of $k$-ary predicate symbols, such that $= \, \in \mathsf{P}_{2}$;
• the symbols $\neg, \wedge, \vee$ of propositional connectives of negation, conjunction and disjunction, respectively;
• the symbols $\forall, \exists$ of the universal and existential quantifiers, respectively;
• parentheses $(,)$.

The set of atomic formulas of the logic $\mathsf F$ is the smallest set closed under the following rules:

• if $x,y \in \mathsf{V}$, then $(x=y)$ is an atomic formula ;
• for every $k \in \omega$ and $P \in \mathsf{P}_{k}$, if $x_{1}, \ldots, x_{k} \in \mathsf{V}$, then $P(x_{1}, \ldots, x_{k})$ is an atomic formula.

The set of $\mathsf F$-formulas is the smallest set containing the set of atomic formulas and closed on propositional connectives and quantifiers.

The Hilbert-style axiomatization of the logic $\mathsf{F}$ consists of the axioms of $\mathsf{PC}$ and the following specific axioms:

(Ax1) $\forall x \varphi(x) \rightarrow \varphi(y)$
(Ax2) $\varphi(y) \rightarrow \exists x \varphi(x)$

The rules of the system are modus ponens and the following rules: \[\displaystyle\frac{\psi \rightarrow \varphi(x)}{\psi \rightarrow \forall x \varphi(x)} \qquad \displaystyle\frac{\varphi(x) \rightarrow \psi}{\exists x \varphi(x) \rightarrow \psi}\] A derivation of a formula $\varphi$ from a set $X$ of $\mathsf{F}$-formulas is a finite sequence $\{\psi_1, \ldots, \psi_n\}$ of $\mathsf{F}$-formulas such that $\psi_n = \varphi$ and for every $i \in \{1, \ldots, n\}$:

• either $\psi_i \in X$,
• or $\psi_i$ is an axiom,
• or $\psi_i$ is obtained from $\{\psi_1, \ldots, \psi_{i-1}\}$ by an application of some rule.

A formula $\varphi$ is said to be $\mathsf{F}$-provable, whenever there exists a derivation of $\varphi$ from the empty set of $\mathsf{F}$-formulas.

An $\mathsf F$-model is a pair $\mathcal{M} = \langle U, m \rangle$ such that

• $U$ is a non-empty set,
• $m$ is a meaning function such that for every $k$-ary predicate symbol $P$, $m(P) \subseteq U^{k}$, $k \in \omega$,
• $m(=)$ is an equivalence relation on $U$,
• the following extensionality property is satisfied: for all $a_i, b_i \in U, i= 1, \ldots, k$ and every $k$-ary predicate symbol $P, k \in \omega$
  $\mbox{If } (a_1, b_1) \in m(=), \ldots, (a_k, b_k) \in m(=) \mbox{ and } (a_1, \ldots, a_k) \in m(P), \mbox{ then } (b_1, \ldots, b_k) \in m(P)$

An $\mathsf{F}$-model is standard, if the meaning of the identity predicate is \[m(=)=\{(a,a) : a \in U\}.\] Let $\mathcal{M}$ be an $\mathsf F$-model. A valuation in $\mathcal M$ is a mapping $v : \mathsf{V} \to U$. We write $\mathcal{M}, v \models \varphi$ to denote that $\varphi$ is satisfied in $\mathcal M$ by $v$. The relation $\models$ is inductively defined as follows:

• $\mathcal{M}, v \models (x=y) \stackrel{\rm def}{\Longleftrightarrow} \langle v(x), v(y)\rangle \in m(=)$;
• $\mathcal{M}, v \models P(x_{1}, \ldots, x_{k}) \stackrel{\rm def}{\Longleftrightarrow} \langle v(x_{1}), \ldots, v(x_{k})\rangle \in m(P)$;
• $\mathcal{M}, v \models \neg \varphi \stackrel{\rm def}{\Longleftrightarrow} \mbox{ not } \mathcal{M}, v \models \varphi$;
• $\mathcal{M}, v \models \varphi \wedge \psi \stackrel{\rm def}{\Longleftrightarrow} \mathcal{M}, v \models \varphi \mbox{ and } \mathcal{M}, v \models \psi$;
• $\mathcal{M}, v \models \varphi \vee \psi \stackrel{\rm def}{\Longleftrightarrow} \mathcal{M}, v \models \varphi \mbox{ or } \mathcal{M}, v \models \psi$;
• $\mathcal{M}, v \models \forall x \varphi \stackrel{\rm def}{\Longleftrightarrow}$ for every valuation $v'$ in $\mathcal{M}$ such that $v$ and $v'$ coincide on $\mathsf{V} \setminus\{x\}$}, $\mathcal{M}, v' \models \varphi$;
• $\mathcal{M}, v \models \exists x \varphi \stackrel{\rm def}{\Longleftrightarrow}$ for some valuation $v'$ in $\mathcal{M}$ such that $v$ and $v'$ coincide on $\mathsf{V} \setminus\{x\}$}, $\mathcal{M}, v' \models \varphi$;

A formula $\varphi$ is true in $\mathcal M$ if and only if $\mathcal{M}, v \models \varphi$ for every valuation $v$ in $\mathcal{M}$. An $\mathsf{F}$-formula is $\mathsf{F}$-valid whenever it is true in all $\mathsf{F}$-models. An $\mathsf{F}$-formula is $\mathsf{F}^*$-valid whenever it is true in all standard $\mathsf{F}$-models. Clearly, $\mathsf{F}$-validity implies $\mathsf{F}^*$-validity.

Theorem 2 (Completeness and soundness of $\mathsf{F}$) The logic $\mathsf{F}$ is sound and complete, that is for every $\mathsf{F}$-formula $\varphi$ the following conditions are equivalent:

• $\varphi$ is $\mathsf{F}$-provable.
• $\varphi$ is $\mathsf{F}$-valid.
• $\varphi$ is $\mathsf{F}^*$-valid.

Dual tableaux for first-order logic with identity

Formalism description The vocabulary of the first-order logic $\mathsf F$ with identity consists of:

• a countable set of individual variables $\mathsf{V}$;
• for every $k \in \omega, k \geq 1$, a countable set $\mathsf{P}_{k}$ of $k$-ary predicate symbols, such that $= \, \in \mathsf{P}_{2}$;
• the symbols $\neg, \wedge, \vee$ of propositional connectives of negation, conjunction and disjunction, respectively;
• the symbols $\forall, \exists$ of the universal and existential quantifiers, respectively;
• parentheses $(,)$.

The set of atomic formulas of the logic $\mathsf F$ is the smallest set closed under the following rules:

• if $x,y \in \mathsf{V}$, then $(x=y)$ is an atomic formula ;
• for every $k \in \omega$ and $P \in \mathsf{P}_{k}$, if $x_{1}, \ldots, x_{k} \in \mathsf{V}$, then $P(x_{1}, \ldots, x_{k})$ is an atomic formula.

The set of $\mathsf F$-formulas is the smallest set containing the set of atomic formulas and closed on propositional connectives and quantifiers.

An $\mathsf F$-model is a pair $\mathcal{M} = \langle U, m \rangle$ such that

• $U$ is a non-empty set,
• $m$ is a meaning function such that for every $k$-ary predicate symbol $P$, $m(P) \subseteq U^{k}$, $k \in \omega$,
• $m(=)$ is an equivalence relation on $U$,
• the following extensionality property is satisfied: for all $a_i, b_i \in U, i= 1, \ldots, k$ and every $k$-ary predicate symbol $P, k \in \omega$
  If $ (a_1, b_1) \in m(=), \ldots, (a_k, b_k) \in m(=)$ and $(a_1, \ldots, a_k) \in m(P)$, then $(b_1, \ldots, b_k) \in m(P)$

An $\mathsf{F}$-model is standard, if the meaning of the identity predicate is \[m(=)=\{(a,a) : a \in U\}.\] Let $\mathcal{M}$ be an $\mathsf F$-model. A valuation in $\mathcal M$ is a mapping $v : \mathsf{V} \to U$. We write $\mathcal{M}, v \models \varphi$ to denote that $\varphi$ is satisfied in $\mathcal M$ by $v$. The relation $\models$ is inductively defined as follows:

• $\mathcal{M}, v \models (x=y) \stackrel{\rm def}{\Longleftrightarrow} \langle v(x), v(y)\rangle \in m(=)$;
• $\mathcal{M}, v \models P(x_{1}, \ldots, x_{k}) \stackrel{\rm def}{\Longleftrightarrow} \langle v(x_{1}), \ldots, v(x_{k})\rangle \in m(P)$;
• $\mathcal{M}, v \models \neg \varphi \stackrel{\rm def}{\Longleftrightarrow} \mbox{ not } \mathcal{M}, v \models \varphi$;
• $\mathcal{M}, v \models \varphi \wedge \psi \stackrel{\rm def}{\Longleftrightarrow} \mathcal{M}, v \models \varphi \mbox{ and } \mathcal{M}, v \models \psi$;
• $\mathcal{M}, v \models \varphi \vee \psi \stackrel{\rm def}{\Longleftrightarrow} \mathcal{M}, v \models \varphi \mbox{ or } \mathcal{M}, v \models \psi$;
• $\mathcal{M}, v \models \forall x \varphi \stackrel{\rm def}{\Longleftrightarrow}$ for every valuation $v'$ in $\mathcal{M}$ such that $v$ and $v'$ coincide on $\mathsf{V} \setminus\{x\}$, $\mathcal{M}, v' \models \varphi$;
• $\mathcal{M}, v \models \exists x \varphi \stackrel{\rm def}{\Longleftrightarrow}$ for some valuation $v'$ in $\mathcal{M}$ such that $v$ and $v'$ coincide on $\mathsf{V} \setminus\{x\}$, $\mathcal{M}, v' \models \varphi$;

A formula $\varphi$ is true in $\mathcal M$ if and only if $\mathcal{M}, v \models \varphi$ for every valuation $v$ in $\mathcal{M}$. An $\mathsf{F}$-formula is $\mathsf{F}$-valid whenever it is true in all $\mathsf{F}$-models. An $\mathsf{F}$-formula is $\mathsf{F}^*$-valid whenever it is true in all standard $\mathsf{F}$-models. Clearly, $\mathsf{F}$-validity implies $\mathsf{F}^*$-validity.

Dual tableau for $\mathsf{F}$ is determined by the rules and axiomatic sets. The rules of the system preserve and reflect validity of the sets of formulas, which are their conclusions and premises. Validity of a set of formulas is defined as validity of disjunction of its elements. We say that a variable in a rule is new whenever it appears in a conclusion of the rule and does not appear in its premise.

Let $\varphi, \psi$ denote $\mathsf{F}$-formulas. Dual tableau for $\mathsf{F}$ contains decomposition rules of the following forms:

($\vee$)	$\displaystyle\frac{\{\varphi \vee \psi\}}{ \{\varphi, \psi\}}$	($\neg \vee$)	$\displaystyle\frac{\{\neg(\varphi \vee \psi)\}}{\{\neg \varphi\} \quad | \quad \{\neg \psi\}}$
($\wedge$)	$\displaystyle\frac{\{\varphi \wedge \psi\}}{\{\varphi\}\quad | \quad \{\psi\}}$	($\neg \wedge$)	$\displaystyle\frac{ \{\neg(\varphi \wedge \psi)\}}{\{\neg \varphi, \neg \psi\}}$
($\neg$)	$\displaystyle\frac{\{\neg \neg \varphi\}}{\{\varphi\}}$
($\forall$)	$\displaystyle\frac{\{\forall x \varphi(x)\}}{ \{\varphi(z)\}}$	($\neg \forall$)	$\displaystyle\frac{\{\neg\forall x \varphi(x)\}}{\{\neg \varphi(z), \neg \forall x \varphi(x)\}}$
	$ z$ is a new variable		$ z$ is any variable
($\exists$)	$\displaystyle\frac{\{\exists x \varphi(x)\}}{\{\varphi(z), \exists x \varphi(x)\}}$	($\neg \exists$)	$\displaystyle\frac{\{\neg \exists x \varphi(x)\}}{\{\neg \varphi(z)\}}$
	$ z$ is any variable		$ z$ is a new variable

and the specific rules of the following form:

($=$)	$\displaystyle\frac{\{\varphi(x)\}}{\{x=z, \varphi(x)\} \quad | \quad \{\varphi(z), \varphi(x)\}}$
	$ z$ is a variable, $ \varphi$ is an atomic formula

A finite set of formulas is $\mathsf{F}$-axiomatic whenever it includes either of the following subsets:

(Ax1)	$\{x=x\}$ ,         $ x$ is any variable,
(Ax2)	$\{\varphi, \neg \varphi\}$ ,         $ \varphi$ is any formula.

A finite set of formulas $\{\varphi_{1}, \varphi_{2}, \ldots, \varphi_{n}\}$ is said to be an $\mathsf{F}$-set whenever the disjunction of its elements is $\mathsf{F}$-valid. That is ',' (comma) is interpreted as disjunction.

A rule of the form \[\frac{\Phi}{\Phi_{0} | \Phi_{1}}, \quad \left(\mbox{resp. } \frac{\Phi}{\Phi_0} \right)\] is $\mathsf{F}$-correct, whenever $\Phi$ is an $\mathsf{F}$-set iff $\Phi_{0}$ and $\Phi_1$ are $\mathsf{F}$-sets (resp. $\Phi$ is an $\mathsf{F}$-set iff $\Phi_0$ is an $\mathsf{F}$-set). It follows that '$|$' (branching) is interpreted as conjunction.

A proof in dual tableau system has the form of a finitely branching tree whose nodes are finite sets of formulas. Let $\varphi$ be an $\mathsf{F}$-formula. An $\mathsf{F}$-proof tree for $\varphi$ is a tree with the following properties:

• the formula $\varphi$ is at the root of this tree,
• each node except the root is obtained by the application of an $\mathsf{F}$-rule to its predecessor node,
• a node does not have successors whenever it is an $\mathsf{F}$-axiomatic set.

A branch of an $\mathsf{F}$-proof tree is said to be closed whenever it contains a node with an $\mathsf{F}$-axiomatic set of formulas. An $\mathsf{F}$-tree is closed iff all of its branches are closed. An $\mathsf{F}$-formula $\varphi$ is $\mathsf{F}$-provable whenever there is a closed proof tree for $\varphi$.

Theorem 3 (Completeness and Soundness for $\mathsf{F}$)

Let $\varphi$ be an $\mathsf{F}$-formula. Then the following conditions are equivalent:

• $\varphi$ is $\mathsf{F}$-provable.
• $\varphi$ is $\mathsf{F}$-valid.
• $\varphi$ is $\mathsf{F}^*$-valid.

Application fields Dual tableaux system for the classical first-order logic is a basis for dual tableau formalisms for various non-classical logics. In particular, axiomatization of relational logics is often presented in a dual tableaux style (see this Handbook...).

Comments and references The dual tableaux for classical first-order logic (without the identity) is introduced in Rasiowa and Sikorski 1960, see also Rasiowa and Sikorski 1963. The system is cut free, and it does not require a cut rule in the proof of completeness theorem as does the Gentzen system Gentzen 1935. A duality between the tableaux system of Smullyan 1968 and Rasiowa-Sikorski dual tableaux is presented in Golińska-Pilarek and Orłowska 2007 together with an algorithm for transformation of the proofs in one of the systems into the proofs in the other.