Subject: Re:Puzzling "premisse"
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-10-11 19:55:55 GMT (30 weeks, 3 days, 7 hours and 7 minutes ago)
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