[Logiweb] Rule C

[Klaus Ebbe Grue]

Hi Frederik,

> I'm working with an axiomatic system which is based upon system S from the 
> "check" page. I've come accross the following problem:
>
> Sometimes in a proof, you want to infer e.g. 'a=a' from Ex.x=x, where 'E' is 
> the existential quantifier, and 'a' is a fresh variable. In section 2.6 of 
> Mendelson, he introduces a so-called "rule C" to accomodate this need. He 
> also gives an example of how you can get by without rule C, but this seems to 
> be a very cumbersome task indeed. How do you deal with inferences like the 
> above in system S?

Yes, it is cumbersome. But no more cumbersome than Deduction. Actually, it 
is the same algorithm, so there is no need to program something new. 
Mendelson, page 81, Section 2.6: "RULE C" considers the following example:

L Lemma A: Ex:((B(x) => C(x)) |- Ax:B(x) |- Ex:C(x)

L proof of A:
L01: Premisse >>           Ex: (B(x) => C(x)) ;
L02: Premisse >>           Ax: B(x) ;
L03: Rule C >>             B(b) => C(b) ; (for some b)
L04: Rule A4 |> L02 >>     B(b) ;
L05: MP |> L03 |> L04 >>   C(b) ;
L06: Rule E4 |> L05 >>     Ex: C(x)

A translation of the proof above using deduction reads:

L proof of A:
L01: Premisse >>           Ex: (B(x) => C(x)) ;
L02: Premisse >>           Ax: B(x) ;
L99: Block >>              Begin ;
L03: Premisse >>             B(y) => C(y) ;
L04: Rule A4 |> L02 >>       B(y) ;
L05: MP |> L03 |> L04 >>     C(y) ;
L06: Rule E4 |> L05 >>       Ex: C(x) ;
L07: Block >>              End ;
L08: Ded |> L07 >>         (B(y) => C(y)) => Ex: C(x);
L09: B |> L01 |> L08 >>    Ex: C(x)

To make the translation work, we need an auxiliary lemma:

L lemma B: x#H ||- Ex: G(x) |- G(x) => H |- H

Above, x#H says that x does not occur free in H.

L proof of B:
L01: Premisse >>           Ex:G(x) ;
L02: Premisse >>           G(x) => H ;
L03: Gen |> L02 >>         Ax:(G(x) => H) ;
L04: Tautology |> 2.32d >> Ex:G(x) => H ;
L05: MP |> L04 |> L01 >>   H

And how do we prove 2.32d in Mendelson? That is one of Mendelsons
exercises :-)

But I will take a look at 2.32d later.

-Klaus