How to prove that if $\vdash_{ax} A$, then, for every formula B that is an instance of A, $\vdash_{ax} B$?

63 Views Asked by At

$\vdash_{ax} A$ means that $A$ is a theorem - a formula such that there's a derivation $A_1, \ldots, A_n = A$. A derivation is a sequence of formulas $A_1, \ldots, A_n$ such that each formula in the sequence is either an instance of an axiom or is obtained through modus ponens.

My textbook says, as a "hint", that I should prove it by induction on size of the derivation $A:\ A_1, \ldots, A_n = A$.

Here's my attempt (sorry for any grammar mistakes, english is not my first language. It is also worth saying that $A[p := X]$ means that $A$ is an instantiation which $p$ was replaced by $X$).

Let $D$ be a derivation $A_1, \ldots, A_n$:

Base case: For $n = 1$. If $|D| = 1$, then $A$ itself is an axiom. If $B$ is an instance of $A$, then there's two cases:

Let $p$ be any atom of $A$.

Case 1. $B = A[p := p]$. In this case, $B$ and $A$ are the same axiom. So if $\vdash_{ax} A$, we have also $\vdash_{ax} B$.

Case 2. $B = A[p := X]$, let $X$ be any logic formula. In this case, there is a derivation $A_1, A[p := X] = B$, therefore, $\vdash_{ax} B$, since the only difference between the deduction of $A$ and the deduction of $B$ was the inclusion of $A[ p:= X ]$, which is an instantiation of an axiom, which remains consistent with the definition of deduction.

Inductive step: Now, let's assume that the statement is true for every deduction $D$ of size less than or equal to $n$. In other words, let's assume that if $A_1,\ \ldots,\ A_n = A$, then $A_1,\ \ldots,\ A_n, A[ p:= X ] = B$, $| D| \le n$.

Therefore, if $D, \ A_{n + 1} = A$, then $D,\ A_{n + 1}, A[ p:= X ] = B$


This proof isn't finished and I actually don't know how to proceed from there. My thinking was that, if I could show that $A_{n+1}$ is either an axiom instance or obtained via modus ponens, then my job was almost done, since I'd have shown that $B$ was also a theorem. But I was wrong, because $A[ p:= X ]$ isn't necessarily the instance of an axiom but it is primarily the instance of $A$, which is a theorem... and by definition, I'm allowed to use only instance of axioms and modus ponens in a derivation and not instances of a theorem.

So, I probably am not in the right path with this proof and I should, maybe, try to show that if I can obtain $B$ through instantiation of $A$, then I could do the same substitution before in the derivation...

1

There are 1 best solutions below

0
On BEST ANSWER

I’ll just sketch how I would go about it. Each line in $D$ must be an instance of an axiom, or follow from modus ponens. Suppose $\mathcal A_a$ is an axiom instance used to prove $A$. Then, $\mathcal A_b$ is the substitution used to prove $B$. This holds for each instance of an axiom, and the modus ponens steps will be identical.

For example, one can use the same steps in the proof that $A\implies A$ to prove $(P\implies Q)\implies (P\implies Q)$.

The actual proof that $B$ is a valid substitution instance probably needs to use induction, but all you have to show is that each axiom used in $B$’s proof is an appropriate instance of an axiom that would have been used in $A$’s proof.