Definition:Hilbert Proof System/Predicate Logic/Instance 1
< Definition:Hilbert Proof System(Redirected from Definition:Hilbert Proof System Instance 1 for Predicate Logic)
Jump to navigation
Jump to search
 | It has been suggested that this page be renamed. In particular: I feel this is not sustainable To discuss this page in more detail, feel free to use the talk page. |
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$.
Derived Rules
- Deduction Theorem for Hilbert Proof System for Predicate Logic
- Proof by Contradiction for Hilbert Proof System Instance 1 for Predicate Logic
- Reductio ad Absurdum for Hilbert Proof System Instance 1 for Predicate Logic
Source of Name
This entry was named for David Hilbert.
Sources
- 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.10$ Formal Proofs: Definition $\text{II}.10.1$ (axioms)