Subject: Re: Puzzling "premisse"
Newsgroups: gmane.science.mathematics.frogs
Date: 2007-10-13 15:25:07 GMT (30 weeks, 1 day, 12 hours and 34 minutes ago)
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 derivat= ion > without premisses, so it's the derivation of a tautology." > > I find this not only puzzling but bordering on nonsense! > I am sorry you could not find sense in that. > Does this mean that the axioms *and* derivation rules of some logic are n= ot > considered to be an integral part of that logic? No, in particular, it does not mean that. > It is certainly more sensible to consider that the axioms and rules of > derivation which are *actually* used in some=20 >proof *are* in fact the "premisses" > of this proof. Issue of terminology. We have our definition of premise -"fancy" though you find it, you have yours (or rather, your intuition). > commonly construed sense of "premise" as a distal necessary condition In science you need to be more precise than that. =46or the sake of communication we could adopt a real definition different from ours in an e-mail discussion, but not in academic papers and on the website, which are read mostly by people who use the same terminology as we do. > If you maintain the opposite view (proofs are=20 >derivations without premisses) can > you elucidate and support the reasons for this choice? With your intuitive notion of the word "premise", I would tend to think that we do not maintain the opposite view. > There is at least one good reason to reject=20 >this which is related to the "logics > equivalence" problem appearing in Lutz=20 >Stra=E0=FCburger paper "What is a logic, and > what is a proof ?" : > > Assuming that two different axiomatizations for=20 >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=20 >identical, these two "logics" would > still be seen as different because they do not share their axiom sets. > Errr, the logic is the same, but the two axiomatisations/presentations are different but logically equivalent, by definition (ie having the same set of theorems/same logic). > It seems that this could defeat any attempt to=20 >look for proof equivalence in a > very trivial case (these two formalisms are obviously "the same" as far a= s > semantics is concerned). No, you get confused (about formalisations) between "being the same" and "being logically equivalent". What you describe here as a problem is not one. > my criticism that two > "obviously" equivalent logics (in the strong sense that all their true > formulas but a finite few are syntactically identical) fancy notion of "being obviously equivalent", which does not imply "being equivalent" in my sense (or "being logically equivalent"), according to which the sets of theorems are actually identical. Let's forget about "but a finite few". And it seems there that you build on a confusion of terminology again. What you call "a logic" I call "formalisation of a logic in a formalism", or "presentation of a logic" for short, while "a logic" is for me just the set of provable formulae. > will be seen as > formally non equivalent whenever their axioms sets are different but > entails each other (and are thus in some sense equivalent, am I wrong > on this?) because the leaves of the proofs (in your sense of proofs as > trees) are different. The leaves of what proofs? Two proofs in the same (presentation of the given) logic, one proof in one (presentation of the given) logic and one proof of the same formula in the other (presentation of the given) logic? Be precise. =46rom what I gather from your sentence, no, they will not be seen as non equivalent. Indeed in any case, the two (presentations of the given) logic(s) will be considered equivalent because they prove the same formulae. This is the very definition of being (logically) equivalent. Establishing such equivalences is what we spend a lot of time on, there are examples of such proofs in Kai's thesis. > It follows from this incommensurability that neither the proofs nor the > logics are even comparable whereas they are "trivially" equivalent to > common sense. No, -for the same syntaxes of formulae, two logics are always comparable (equal/included/just different), this is simply comparing the sets of provable formulae -for the same logic, two presentations can always be compared by studying the encodings from the proofs of one into those of the other (is the identity/inclusion such an encoding, etc). If you have a notion of size of proof that makes sense in both presentations, you can refine the comparison by looking at polynomial encodings, etc... -for the same presentation of the logic, you can compare two proofs by the comparison tools of the structure you use to represent them, be it trees, rewrite sequences, graphs,etc... > 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. It depends on what you call "selection of proof as a concrete syntactic object". If it is committing to a particular structure such as trees, well-bracketed expressions... then maybe these are doomed. If you challenge the very fact of committing to a definition (that is, a mathematical one), because it is not abstract enough, then I suggest you join a mailing list in Philosophy rather than in Science. > Not that this will not lead to a few more excellent thesis... It will. >> 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. Maybe if you gave definitions instead of using inverted commas for vague notions it would help. Again, "being equivalent" (for axiomatisations/presentations), means generating the same logic, ie the same set of theorems. > 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 By "the formalisation", do you mean the Calculus of Structure? I think no one claims it "captur[es] the intuitive notions of equivalent logics and proofs". It is a tool that we find useful in that quest (and I apologise if you don't). Not the answer to it. > 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. I think we all agree with that. Let's stick to ours! >> 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. Proofs are about communicating certainty. A presentation of a logic is a language for this communication. In the same language, you have tools to compare two things that establish the same fact (one is shorter, one is a paraphrase of the other, one is more elegant...). In two different languages, you can try to do the same but all comparisons are done via translations. And maybe there will be no way to translate something with the same properties, connotations... Maybe you will also lose criteria of comparison when you translate. Comparing two speeches depending on whether they use "tu" or "vous" is a comparison that makes sense in French, but becomes meaningless via a translation into English... Proof theory is very much the same. We look for a good notion of "proof equivalence" in one presentation of a logic (actually aiming at this "incredible -and utterly unlikely- stroke of luck that there exists some sort of "universal [presentation of a] logic" that nobody ever thought of and which has just to be discovered"), and we also compare with proofs in other presentations via translations (potentially lifting, via the translations, the notion of proof equivalence to proofs in different presentations). > 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=E0=E8dinger > You are learned. >> In any case, we do consider inference rules an >> integral part of the meaning of a proof. >> > I am not too sure there isn't some more "terminology" problem here. > Do you call inference rules the various "shortcuts" which are usually > built along the development of proofs, that is, some theorems which are > in effect turned into new ways to derive formulas from premisses (in > your sense of proximal conditions) or do you include also the "basic > inference mechanisms" of a given logic which are the most elementary > syntactic manipulations allowing to create proofs and new formulas? > If you don't include these basic rules you cannot compare logics having > markedly different syntactic forms. > If you do, how do you describe these basic syntactic rules? The inference rules are roughly "the axioms and derivation rules" of the presentation of the logic that you were talking about in a previous e-mail. No "shortcuts" things. In other words, they are the "basic inference mechanisms" of [A PRESENTATION OF] a given logic which are the most elementary syntactic manipulations allowing to create proofs. > It needs some "meta-level" description which has to be valid across all > possible syntactic features... Define "valid across all possible syntactic features". >> 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. >> > Nah! > No need for this level of sophistication to show a counterexample (see > my response to Kai), two different axiomatisations within the same > syntactic framework where each axiom set entails the other are > enough. I have seen no counter-example so far. >> 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. >> > Very interesting approach, given any two proofs conjectured to be "the > same" is there a "natural limit" to what is achievable as an > equivalence demonstration, if so doesn't this mean that there is some > kind of "canonical form" to which both proofs are reducible, when and > how such canonical form can be found, is there a decidable procedure > for this search, etc... > > This seems to bring back to confluence and termination problems in > rewriting systems, may be a little "cross fertilisation" is in order? Indeed that's a promising direction of research, and we haven't waited for your suggestion to start investigating it. > My overall take on this is that focusing too early on a *specific* > syntactic formalism, be it the Calculus of Structures or anything else > even more "clever" will hinder the understanding of the "true nature" > of proofs and logics. > If we are trying to go from the informal ("intuitive" understanding) > to the formal (axiomatized theories) lingering a bit more within the > informal probably pays off *a lot* in spared useless efforts. And how long do you suggest to do philosophy for? >> It would be nice >> if we could dedicate ourselves to finding the >> true nature of proofs, but the reality is that we >> cannot and nobody really cares. Or, at least, I >> don't care and I don't know anybody that does. >> > ROFLMAO > > Would you write "I don't care and I don't know anybody that does" in a > grant submission? > > Wasn't the 2005 ICALP Workshop titled : > "STRUCTURES AND DEDUCTION" > "The quest for the essence of proofs" > > Would you tell the sponsors of such events that "nobody really cares"? No no, just tell you. > Actually I do care for the "true nature of proofs" and this is NOT a > "metaphysical quest" driven by lunatic interests, if I may explain. > > When I started my career at IBM in 1968 > [...] > I have been and still am disappointed by the goals and methods of > scientific research, I'm sorry about that. I hope you get over it. > I DO understand that you cannot help but follow > the crowd and that "the reality is that [you] cannot [do any REAL > research]" and you have to produce shitloads of papers instead, and > that any actual USEFULL result is just a fortunate but minor by-product > of academic research. Again, I'm sorry our research hasn't been useful to your life yet. > I am only suggesting that diverting a small amount of efforts toward > actual THINKING instead of grinding over and over on well known and > "promising" subject matters may lead to better insights and probably > even allow to produce more *significant* papers (Wow!). I suggest you start "diverting a small amount of efforts" towards that, so that we see it working. But maybe we should all go back to our areas of expertise. >> So, maybe, can we drop this discussion? >> > Not a problem for me if you "drop this discussion" since it wastes > valuable time that could be used for polishing the "next paper" or the > "next grant", this isn't necessarily the case for everybody on this > list. It did waste my Saturday, but I was only thinking of going hiking instead. Stephane