Kurt Schutte Proof Theory (Theorem 1.5 proof)

115 Views Asked by At

I had a question regarding the proof of Theorem 1.5 in Kurt Schutte's Proof Theory.

Theorem 1.5 If $\mathcal{E}$ is a $P$-form and $V$ a sentential valuation with $VA = t$, then $V \mathcal{E}[A] = t$.

We proceed by induction on the length of $\mathcal{E}$. The first part is clear, if $\mathcal{E}$ is of the form $*_1$, then $V\mathcal{E}[A] = V *_1 [A] = VA = t$ since we replace each occurrence of $*_1$ in $*_1$ with $A$ and the result is just $A$. However, if $\mathcal{E}$ is of the form $\mathcal{P}[(*_1 \vee B)]$ where $\mathcal{P}$ is a $P$-form and $B$ is a formula, then how would I evaluate and justify $V \mathcal{P}[(*_1 \vee B)][A]$ to arrive at $V[(A \vee B)] = t$? Thanks.

1

There are 1 best solutions below

2
On

Welcome to math.SE!

Formally, what we're trying to establish is equivalent to the following:

For any sentential valuation $V$, it is the case that for every P-form $\mathcal{E}$, the following holds: for any $A$, if $VA = t$ then $V\mathcal{E}[A] = t$.

Hence, we can fix a sentential valuation $V$ and take the induction hypothesis to be the following:

For any P-form $\mathcal{P}$ that is strictly shorter than $\mathcal{E}$, the following holds: for any $A$, if $VA = t$ then $V\mathcal{P}[A] = t$.

Now, we need to prove that the same conclusion holds for $\mathcal{E}$, i.e.

for any $X$, if $VX = t$ then $V\mathcal{E}[X] = t$.

We deal with the case when $\mathcal{E}$ can be written in the form $\mathcal{P}[*_1 \vee B]$ for some $\mathcal{P}$. Then $\mathcal{P}$ is shorter than $\mathcal{E}$, so the induction hypothesis gives us the following:

For any $A$, if $VA = t$ then $V\mathcal{P}[A] = t$.

Consider any $X$, and set $A=X \vee B$. From $V(X) = t$ it follows that $V(X\vee B) = t$, so by the induction hypothesis we have that $V\mathcal{P}[X \vee B] = t$. But then we get $$V\mathcal{E}[X] = V(\mathcal{P}[*_1 \vee B])[X] = V\mathcal{P}[X \vee B] = t$$ as desired (the second equality follows by definition of substitution on top of page 11).