Author: Jan BurseJan Burse
Date: May 15, 2008 12:06
I have serious doubt about the following theorem:
Theorem II.8.10 (strong soundness theorem). The following
is provable in RCA_0. If there exists a weak countable
model of X subset Snt, then X is consistent.
The doubt concerns the proof of the above theorem. The proof
goes along the following lines:
If X were inconsistent, then there were a proof of
~(s1 & .. & sn), with s1 .. sn in X. Ok, no doubt.
We can assume that we have a cut free proof
of this. Ok, no doubt.
Let M be a weak countable model of X, then we
have for the subformulas s in the proof M(s)=1.
**No, thats not true, big doubt on this.**
Because M(s1)=..=M(sn)=1, and M(~(s1 &..& sn))=1,
we arrive at a contradiction.
My doubt is based on a simple observation how typically
cut free proofs work on propositional formulas(*):
| 
