Axioms of Hilbert Proof System Instance 1 for Predicate Logic are Tautologies

From ProofWiki
Jump to navigation Jump to search


This page has been identified as a candidate for refactoring of basic complexity.
In particular: Transclude axioms
Until this has been finished, please leave {{Refactor}} in the code.

New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only.

Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Refactor}} from the code.


Theorem

Let $\mathscr H$ be Instance 1 of a Hilbert proof system for predicate logic.

Then the axioms of $\mathscr H$ are tautologies.


Proof


Although this article appears correct, it's inelegant. There has to be a better way of doing it.
In particular: For each axiom this should link to a theorem page instead, but I had difficulties coming up with names. Maybe subpages?
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Improve}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.


Axiom 1

This is precisely the statement of Propositional Tautology is Tautology in Predicate Logic.

$\Box$


This article needs proofreading.
In particular: below
If you believe all issues are dealt with, please remove {{Proofread}} from the code.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Proofread}} from the code.



Although this article appears correct, it's inelegant. There has to be a better way of doing it.
In particular: The theorem cited below is actually Universal Generalisation for semantics of PredLog
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by redesigning it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Improve}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.


By Well-Formed Formula is Tautology iff Universal Closure is Tautology, we prove the results for axioms 2 through 11 for the WFFs instead of their universal closures.

Let $\sigma$ be an assignment in a structure $\AA$.

Let $\map { \operatorname{val}_\AA } {\cdot} \sqbrk \sigma$ be the value mapping for $\sigma$ in $\AA$.


Axiom 2: $\mathbf A \implies \paren{ \forall x: \mathbf A }$

We have that $\map { \operatorname{val}_\AA } {\forall x: \mathbf A} \sqbrk \sigma = T$ if and only if:

$\forall a \in A: \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma + \paren{ a / x } } = T$

By assumption, $x$ does not occur freely in $\mathbf A$.

By Value of Formula under Assignment Determined by Free Variables, it follows that:

$\forall a \in A: \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma + \paren{ a / x } } = \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma }$

and hence:

$\map { \operatorname{val}_\AA } {\forall x: \mathbf A} \sqbrk \sigma = \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma }$

Therefore:

\(\ds \map { \operatorname{val}_\AA } {\mathbf A \implies \paren{ \forall x: \mathbf A } } \sqbrk \sigma\) \(=\) \(\ds \map { f^\to } { \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk \sigma, \map { \operatorname{val}_\AA } {\forall x: \mathbf A} \sqbrk \sigma }\)
\(\ds \) \(=\) \(\ds \map { f^\to } { \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk \sigma, \map { \operatorname{val}_\AA } {\mathbf A} \sqbrk \sigma }\)
\(\ds \) \(=\) \(\ds T\) Definition of Truth Function of Conditional

Since $\AA$ and $\sigma$ are arbitrary, it follows that $\mathbf A \implies \paren{ \forall x: \mathbf A }$ is a tautology.

$\Box$


Axiom 3: $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$

Aiming for a contradiction, suppose that $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$ is not a tautology.

Then there exist $\AA, \sigma$ such that:

$\map { \operatorname{val}_\AA } { \paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } } } \sqbrk \sigma = F$

By definition of $\operatorname{val}_\AA$, this means:

$\map { f^\to } { \map { \operatorname{val}_\AA } {\forall x: \mathbf A \implies \mathbf B} \sqbrk \sigma, \map { \operatorname{val}_\AA } {\paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } } \sqbrk \sigma } = F$

By definition of the truth function $f^\to$, this happens if and only if:

$\map { \operatorname{val}_\AA } {\forall x: \mathbf A \implies \mathbf B} \sqbrk \sigma = T$
$\map { \operatorname{val}_\AA } {\paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } } \sqbrk \sigma = F$

and, applying the same argument on the second statement, we get:

$\map { \operatorname{val}_\AA } {\forall x: \mathbf A \implies \mathbf B} \sqbrk \sigma = T$
$\map { \operatorname{val}_\AA } {\forall x: \mathbf A } \sqbrk \sigma = T$
$\map { \operatorname{val}_\AA } {\forall x: \mathbf B } \sqbrk \sigma = F$

By definition of $\operatorname{val}_\AA$, the last of these statements means that for some $a \in A$:

$\map { \operatorname{val}_\AA } {\mathbf B } \sqbrk { \sigma + \paren{x / a} } = F$

where $\sigma + \paren{x / a}$ is the extension of $\sigma$ by mapping $x$ to $a$.

Similarly, from the first two statements it follows that:

$\map { \operatorname{val}_\AA } {\mathbf A } \sqbrk { \sigma + \paren{x / a} } = T$
$\map { \operatorname{val}_\AA } {\mathbf A \implies \mathbf B} \sqbrk { \sigma + \paren{ x / a} } = T$

However, by definition of $\operatorname{val}_\AA$:

\(\ds \map { \operatorname{val}_\AA } {\mathbf A \implies \mathbf B} \sqbrk { \sigma + \paren{ x / a} }\) \(=\) \(\ds \map { f^\to } {\map { \operatorname{val}_\AA } {\mathbf A} \sqbrk { \sigma + \paren{ x / a} }, \map { \operatorname{val}_\AA } {\mathbf B} \sqbrk { \sigma + \paren{ x / a} } }\)
\(\ds \) \(=\) \(\ds \map { f^\to } { T , F }\) from above
\(\ds \) \(=\) \(\ds F\) Definition of Truth Function of Conditional

Thus, by Proof by Contradiction, $\paren{ \forall x: \mathbf A \implies \mathbf B } \implies \paren{ \paren{ \forall x: \mathbf A } \implies \paren{ \forall x: \mathbf B } }$ is a tautology.

$\Box$


Axiom 4-11


This needs considerable tedious hard slog to complete it.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Finish}} from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Axioms_of_Hilbert_Proof_System_Instance_1_for_Predicate_Logic_are_Tautologies&oldid=591579"