Subject: Re: Puzzling "premisse"
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-10-12 13:24:22 GMT (30 weeks, 3 hours and 28 minutes ago)
Dear Jean-Luc, > Thanks for your timely response, of course I still disagree. I don't see much room for disagreement. The only way to disagree with a definition, in our case of "premise", is if you already have a different notion of "premise". In that case, we are happy to replace the word "premise" by the word "initial formula" or some other word you happen to have available for our use. > I think the catch lies in the selection of proof as "a concrete > syntactic object", this is probably not abstract enough and guarantees > that you (or anyone else) will be swamped forever in irrelevant tedious > "bureaucracy" with idiosyncratic details pertaining only to the > "current logic under consideration", no matter how you try to tackle > the problems of proofs equivalence/logics equivalence. Sure! That's a well-recognised problem of proof theory and it is in no way specific to deep inference. I don't know anyone who disagrees with that. In fact, I'd say that the deep inference community is particularly aware of it. We even had a workshop dedicated to it: http://www.prooftheory.org/sd05/ . Maybe I can sum up the current status as follows: the problem is far from solved, it's not even clear what "solved" should mean, but trying to solve it does lead to interesting mathematics. -Kai