Definition:Hilbert Proof System/Predicate Logic/Instance 1

From ProofWiki
Jump to navigation Jump to search


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:


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.