home   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:

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\}$:

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:

First-order logic with identity

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

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

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\}$:

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

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:

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:

Dual tableaux for first-order logic with identity

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

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

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

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:

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:

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:

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.

References

  1. Fitting, M. (1990). First-order Logic and Automated Theorem Proving. New York: Springer-Verlag.
  2. Gentzen, G. (1935). Untersuchungen über das logische Schliessen. Mathematische Zeitschrift 39, 176-210, 405-431.
  3. Golińska-Pilarek, J., and Orłowska, E. (2007). tableaux and Dual tableaux: transformation of proofs. Studia Logica, 85(3), 283-302.
  4. Rasiowa, H., and Sikorski, R. (1960). On Gentzen theorem. Fundamenta Matematicae, 48, 57-69.
  5. Rasiowa, H., and Sikorski, R. (1963). Mathematics of Metamathematics. Warsaw: Polish Scientific Publishers.
  6. Smullyan, R. (1968). First Order Logic. Berlin, Heidelberg, New York: Springer.