Theorem II.8.10 (SOSOA): maybe interesting result, probably wrong proof

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(*):

A cut free proof, is nothing else then
a equivalence transformation of the original formula
into a conjunctive normal form, and stripping
those conjuncts which contain A v ~A, in the
end arriving at an empty conjunct, and thus
have shown that the original formula is a tautology.

Example:

-----------
a->f,b->f,a
-----------
a->f,b->a
---------
a->(b->a)

The conjunctive normalform of a->(b->a) is
indeed ~a v ~b v a. And the conjunct contains
a v ~a, thus can be removed. So that in the
end we have:

a->(b->a) <=> t

But for a model of a->(b->a) its not necessarly
that M(b)=1.

In summary, the invocation of cut free proofs is
even not needed in theorem II.8.10, because anyway
a weak model requires M(s1)=..=M(sn)=1.

comments welcome

Bye

(*)
We can use the following propositional variation of
http://www.xlog.ch/papers/calculi93/calculi93.pdf:

(A->B)' := A & B'.
(A & B)' := A -> B'.
P' := P -> f
(P->f)' := P


--------
G,P,P->f


G,A',B
------
G,A->B

G,A G,B
---------
G,A&B
.

Quantcast