Subject: Re: Puzzling "premisse"
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-10-12 18:41:10 GMT (30 weeks, 2 days, 4 hours and 14 minutes ago)
Le Fri, 12 Oct 2007 15:24:22 +0200, "Kai Brünnler" <kai.bruennler@...> a écrit : > 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. Excuse me but I am not arguing about terminology. I agreed that I could use *your* definitions and still meet the problem I am complaining about, that "equivalent" but distinct axiomatisations give rise to "different" logics which cannot be proved equivalent. That is, the formalisation is missing it's alleged goal of capturing the intuitive notions of equivalent logics and proofs (an instance of the kind of problems which "bug" Solomon Feferman). "Three Conceptual Problems That Bug Me (1996)" http://citeseer.ist.psu.edu/327750.html Furthermore one can *still* disagree about definitions (these or any others about any subject, mathematical or not) in the sense that a clumsy choice of definitions definitely hampers the prospects of a successfull study of a given domain. > 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. Yes, "The quest for the essence of proofs", this is exactly what I am talking about and I am saying that NO investigation about this or that formalisation will lead to any significant progress since looking for "the essence of proofs" is a META question with respect to proofs. That is, unless by an incredible (and utterly unlikely) stroke of luck there exists some sort of "universal logic" that nobody ever thought of and which has just to be "discovered", the "essence of proofs" is NOT likely definable within the syntactic formalisms we are used to in logic. If I may cite one of my favorite quotes: "Thus, the task is not so much to see what no one has yet seen; but to think what nobody has yet thought, about that which everybody sees." -- Erwin Schrödinger Best, JLD