Subject: Puzzling "premisse"
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-10-11 16:24:52 GMT (30 weeks, 3 days, 7 hours and 8 minutes ago)
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? 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). Best, JLD