Re: Puzzling "premisse"

Dear Jean-Luc,

We are academics, and we ultimately need to churn 
out many papers and theses in order to have 
brilliant careers, honours, etc. 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.

So, maybe, can we drop this discussion?

Ciao,

-Alessio


At 14:23 +0200 12/10/07, Jean-Luc Delatre (Kevembuangga) wrote:
> Hi Alessio,
>
> Thanks for your comments, I have some more myself.
>
> >  You can read the definitions in Bruennler's book
> >  <http://www.iam.unibe.ch/~kai/Papers/phd.pdf> to
> >  dissipate any doubt about the meaning of our
> >  terminology.
>
> Done.
>
> >  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?
> It needs some "meta-level" description which has to be valid across all
> possible syntactic features...
>
> >  >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).
> >
> >  You seem to talk about two distinct equivalences
> >  here: of proof systems and of proofs.
>
> Yes and no.
> Yes, because incommensurability of proof systems entails
> incommensurability of proofs from incomparable systems.
> No, because if you choose to take "essence of proofs" as the measuring
> stick between proof systems irrducibility of proofs conversely entails
> incommensurability of proof systems.
>
> >  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.
>
> >  A recent paper on the subject is
> >  <http://cs.bath.ac.uk/ag/p/PrComplDI.pdf>.
>
> Mmmmm...
> "Selling" the Calculus of Structures, why not, but I am not talking
> about this level of investigations but about more primitive (intuitive)
> concepts of what proofs and logics are.
>
> >  On the contrary, if we speak about semantics of
> >  proofs, I am ready to accept that two proofs,
> >  such that one is obtained by translating the
> >  other into a polynomially equivalent proof
> >  system, are different.
>
> Huh?
> Which "purpose" does this serves?
> If you have a decidable (or semi-decidable if one-way only) equivalence
> at hand what's the point of "ignoring" it?
>
> >  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?
>
> BTW, there are well known nasty impossibilities for normal forms in
> bare bones boolean algebra which I mentionned to Lutz Straßburger :
> http://portal.acm.org/citation.cfm?id=111853.111875
> Which can be finessed by moving to boolean ring instead of algebra
> http://www.csie.ntu.edu.tw/~hsiang/
> J. Hsiang and G.S. Huang, ``Some Fundamental Properties of Boolean Ring
> Normal Forms'', DIMACS series on Discrete Mathematics and Computer
> Science: The Satisfiability Problem, American Mathematical Society,1996.
>
> 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.
> But as I said to Kai this is not the Academic Way, thesis have to be
> churned out...
>
> Cheers,
>
> JLD