Re:Puzzling "premisse"

Dear Jean-Luc,

At 16:24 +0000 11/10/07, Jean-Luc Delatre (Kevembuangga) wrote:
> In the "Current Research Topics and Open 
> Problems" page 
> (http://alessio.guglielmi.name/res/cos/crt.html) 
> there is the statement :
>
> "I also distinguish between derivation and proof 
> ... a proof is a derivation without premisses, 
> so it's the derivation of a tautology."
>
> I find this not only puzzling but bordering on nonsense!
>
> Does this mean that the axioms *and* derivation 
> rules of some logic are not considered to be an 
> integral part of that logic?
>
> It is certainly more sensible to consider that 
> the axioms and rules of derivation which are 
> *actually* used in some proof *are* in fact the 
> "premisses" of this proof.
>
> If you maintain the opposite view (proofs are 
> derivations without premisses) can you elucidate 
> and support the reasons for this choice?

We use standard terminology, used by many authors.

There are no special reasons for this choice, as 
there is no consensus on terminology for these 
objects, we just belong in one of the many 
traditions. You can read the definitions in 
Bruennler's book 
<http://www.iam.unibe.ch/~kai/Papers/phd.pdf> to 
dissipate any doubt about the meaning of our 
terminology.

In any case, we do consider inference rules an 
integral part of the meaning of a proof.

> There is at least one good reason to reject this 
> which is related to the "logics equivalence" 
> problem appearing in Lutz Straßburger paper 
> "What is a logic, and what is a proof ?" :
>
> Assuming that two different axiomatizations for 
> one and the same logic are truly equivalent, 
> i.e. that after "a while" (some fixed but 
> unspecified number of inferences for each 
> axiomatization) each axiom set appear as derived 
> from the other and all further derivable 
> formulas are identical, these two "logics" would 
> still be seen as different because they do not 
> share their axiom sets.
>
> It seems that this could defeat any attempt to 
> look for proof equivalence in a very trivial 
> case (these two formalisms are obviously "the 
> same" as far as semantics is concerned).

You seem to talk about two distinct equivalences 
here: of proof systems and of proofs.

I'm not sure of what you mean by `truly 
equivalent', but it seems to me that your notion 
entails the well-known notion of polynomial 
equivalence of proof systems. In this case, we do 
indeed consider equivalent different (and 
possibly trivially different) proof systems. A 
recent paper on the subject is 
<http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>.

On the contrary, if we speak about semantics of 
proofs, I am ready to accept that two proofs, 
such that one is obtained by translating the 
other into a polynomially equivalent proof 
system, are different. Anyway, this doesn't have 
to be this way if you disagree, you just have to 
find a way of abstracting the semantics until the 
difference is eliminated.

Ciao,

-Alessio