# Definition:Hilbert Proof System/Predicate Logic/Instance 1

## Definition

This instance of a Hilbert proof system is used in:

Let $\LL$ be the language of predicate logic.

$\mathscr H$ has the following axioms and rules of inference:

### Axioms

Let $x, y, z$ be variables of $\LL$.

Let $\tau$ be a term of $\LL$.

Let $f_n$ be an $n$-ary function symbol of $\LL$ with $n > 0$.

Let $p_n$ be an $n$-ary relation symbol of $\LL$ with $n > 0$.

Let $\mathbf A, \mathbf B$ be WFFs.

Let $\map{ \mathbf A } {x \gets \tau}$ be the substitution instance of $\mathbf A$ substituting $\tau$ for $x$.

The universal closures of the following WFFs are axioms of $\mathscr H$:

 Axiom 1: Propositional tautologies in the sense of Propositional Tautology is Tautology in Predicate Logic Axiom 2: $\mathbf A \implies \paren{ \forall x: \mathbf A }$, where $x$ does not occur freely in $\mathbf A$ Axiom 3: $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$ Axiom 4: $\paren{ \forall x: \mathbf A } \implies \map{ \mathbf A } {x \gets \tau}$ where $\tau$ is free for $x$ in $\mathbf A$ Axiom 5: $\map{ \mathbf A } {x \gets \tau} \implies \paren{ \exists x: \mathbf A }$ where $\tau$ is free for $x$ in $\mathbf A$ Axiom 6: $\paren{ \forall x: \neg \mathbf A } \iff \neg \paren{ \exists x: \mathbf A }$ Axiom 7: $x = x$ Axiom 8: $x = y \iff y = x$ Axiom 9: $x = y \land y = z \implies x = z$ Axiom 10: $x_1 = y_1 \land \ldots \land x_n = y_n \implies \map {f_n} {x_1, \ldots, x_n} = \map {f_n} {y_1, \ldots, y_n}$ Axiom 11: $x_1 = y_1 \land \ldots \land x_n = y_n \implies \map {p_n} {x_1, \ldots, x_n} \iff \map {p_n} {y_1, \ldots, y_n}$

### Rules of Inference

The sole rule of inference is Modus Ponendo Ponens:

From $\mathbf A$ and $\mathbf A \implies \mathbf B$, one may infer $\mathbf B$.

## Source of Name

This entry was named for David Hilbert.