Subject: Re: Puzzling "premisse"
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-10-11 19:01:01 GMT (30 weeks, 3 days, 7 hours and 55 minutes ago)
Dear Jean-Luc, I use the same notions as Alessio, so I'd like to comment. > 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. From a certain intuitive point of view you are right. However, we do proof theory. Proofs are concrete syntactic objects. In the sequent calculus they are trees, for example. The leaves of these trees are special, and so we give them a name. We use "premise". Some people use "initial sequent" instead of "premise". It's just a technical term to describe something that occurs at a particular place in a certain syntactic object. It's nothing beyond that. The terms derivation, proof, inference rule, premise, etc. all have technical definitions. At least in the case of "premise" this definition does not match your intuition. You can find these definitions in almost all the papers on the CoS website (but my thesis is the only one which also has a large green friendly frog on it). Best wishes, -Kai