[Logiweb] Rule C

[Frederik Eriksen]

Hi logiweb at diku.dk,

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?

Best Regards
Frederik Eriksen.