tag:blogger.com,1999:blog-11295132.post114080614205664136..comments2015-03-02T09:54:13.745-08:00Comments on A Neighborhood of Infinity: The cut rule and reading seminarsDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger10125tag:blogger.com,1999:blog-11295132.post-1143743930359402672006-03-30T10:38:00.000-08:002006-03-30T10:38:00.000-08:00One reason that you might want to prove that cut i...One reason that you might want to prove that cut is redundant even while you use it is that proving cut elimination can be an economic means of proving consistency. <BR/><BR/>Since we can't have a cut free proof of falsity, we mearly have to prove that cut is redundant and we get consistency for free.<BR/><BR/>One curious thing about proofs without cut is that they are so much larger, yet they are easier to find in an automated fashion. This seems to me like it means that it is easier to verify a cut-full proof, yet easier to find a cut-free one. Presumably cut introduction would be a means of optimising functional programs. I guess this just corresponds to finding good lemmas or perhaps refactoring. <BR/><BR/>I think you should start a reading club. I'm new to logic and category theory, and I would find it extremely helpful.Jacobianhttp://www.blogger.com/profile/03650584449231540008noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1141053199151249792006-02-27T07:13:00.000-08:002006-02-27T07:13:00.000-08:00Actually, I think your question almost answers its...Actually, I think your question almost answers itself - the reason axiomatic hilbert style methods are preferred to type theoretic ones, is that mathematicians don't like thinking about their proofs in a combinatorial manner!<BR/><BR/>Slightly more seriously, I think it's because this is the natural way of looking at things if you're used to doing mathematics in the classical manner. You have a bunch of assumptions (axioms) and from them you want to prove a conclusion (theorem). The method of going from left to right is not nearly as important as the fact that you got there (as long as the method in question is valid).David R. MacIverhttp://www.blogger.com/profile/12893796777558636623noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1141000666343217382006-02-26T16:37:00.000-08:002006-02-26T16:37:00.000-08:00I'm not a proof theorist, but I'm a programming la...I'm not a proof theorist, but I'm a programming languages guy, so I can fake it pretty well. <BR/><BR/>Anyway, the motivation is this: proof theorists don't really care about theorems! Instead, they care about about proofs considered as mathematical objects. Inference rules that are "redundant" from the point of view of (say) a model theorist, who only cares about truth or falsity, can be tremendously interesting from a proof-theoretic point of view, because in this POV rules of inference that prove exactly the same theorems can give rise to radically different sets of proofs.<BR/><BR/>You can convert any theorem in propositional classical logic into something that only uses the single connective NAND (aka the Sheffer stroke), but to do so is perverse -- no one would willingly reason with classical logic that way, and the reason is that you destroy all the symmetry and combinatorial structure of the logic when you fuse all the connectives into a single monster. <BR/><BR/>Anyway, back to cut elimination. Cut elimination is interesting for several reasons. First, the proof of cut elimination gives you an estimate of the logical strength of the cut principle. You can look at the cut elimination procedure, and see that it can expand a cut-ful proof into a cut-free one that is possibly hyper-exponentially larger. <BR/><BR/>Secondly, the cut rule has the strange property that it includes a formula in its premises that doesn't appear in the conclusion. That is, in the cut rule<BR/><BR/>If Gamma ==> A, and Gamma, A ==> B are<BR/>derivable, then Gamma ==> B is derivable.<BR/><BR/>the formula A doesn't appear in the consequent. All of the other connectives have this "subformula property" (even forall and exists, once you generalize subformula appropriately), and having the subformula property gives you a very useful property to do induction on when proving things about logics. So if you prove that cut is eliminable, then you can frequently "port" properties from the cut-free variant of the logic, in which the proof is easy, to the cut-full version, where it is harder.<BR/><BR/>The computational version of this is that cut-free logics are vastly easier to do proof search in. With cut, you have to guess which A to use when applying the cut rule, and this creates an infinite amount of nondeterminism in your proof search. <BR/><BR/>Also, seeing which features destroy cut-eliminability is itself interesting. For example, adding an induction axiom to first-order logic will cause cut-elimination to fail. When you do a proof that requires strengthening an induction hypothesis, you see this phenomenon in action. This is also why writing theorem provers that can automatically find inductive proofs is so hard.<BR/><BR/>So, I guess I'll ask a question in turn: what is the appeal of Hilbert-style axiomatic presentations of logic and ZF-style set theory? I'm afraid I don't get it; type-theoretic presentations make vastly more sense to me, since the combinatorial properties of proofs are much more apparent.Neel Krishnaswamihttp://www.blogger.com/profile/09691828772507600568noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140876783966977642006-02-25T06:13:00.000-08:002006-02-25T06:13:00.000-08:00Kenny, good point about the ZF axioms. I think the...Kenny, good point about the ZF axioms. <BR/><BR/>I think there's some disagreement about the biconditionals (well, not actual disagreement int he sense that people have arguments about it, but that different people do different things). Certainly the first set theory course I took which introduced the ZF axioms only had conditionals there (but was immediately followed by the comment that biconditionals are an easy consequence of this and separation). <BR/><BR/>I'd tend to use biconditionals for the sake of convenience - if the two axioms are so obviously equivalent, it probably doesn't matter much which you choose.David R. MacIverhttp://www.blogger.com/profile/12893796777558636623noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140857758051879462006-02-25T00:55:00.000-08:002006-02-25T00:55:00.000-08:00The point of cut elimination is basically that we ...The point of cut elimination is basically that we want this metatheorem to hold for any logical system if we'll really consider it a logic. Just like the deduction theorem (that A,B|=C is a valid sequent iff A|=(B->C) is). Since cut is unidirectional, it makes sense to phrase it as a rule that we then prove is "admissible" from the others, while the deduction theorem goes two ways, and the converse direction just _is_ the only rule of inference in many systems.<BR/><BR/>Another point about cut elimination (assuming that lack of sleep isn't messing me up right now) is that cut can be eliminated in proofs of sequents just using the rules of inference, but I think it can't be eliminated in some cases where extra non-logical axioms are assumed.<BR/><BR/>As for the redundancy of ZF (pairing is redundant, and many phrasings of replacement make separation redundant as well - some phrasings also include the existence of the emptyset, which is redundant given infinity and separation) there's another reason for that. The system Z, which consists of all the axioms except replacement, is quite natural, as is the system ZF-Inf, which has all the axioms except infinity. In each of these theories, some of the previously redundant axioms are now necessary. And in many particular consistency proofs, we construct a structure and then show it satisfies ZF plus whatever else we want. However, we often need the whole machinery of Z to prove that the system satisfies replacement, so it makes sense to prove that the axioms hold one by one, even though at the end we won't need some of the earlier ones.<BR/><BR/>One point that I haven't quite understood though is why all the axioms seem to have biconditionals built in, where conditionals would be sufficient, given separation. (That is, rather than phrasing the union axiom as saying that the union of a set of sets exists, we could phrase it as saying that there is a set having all the previous ones as subsets, and then use separation to cut the union itself out of this big set.)Kennyhttp://www.blogger.com/profile/12226268498253877151noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140821983502325692006-02-24T14:59:00.000-08:002006-02-24T14:59:00.000-08:00David,Yes, my first thought was "why not make it a...David,<BR/><BR/>Yes, my first thought was "why not make it a metatheorem?" if it's useful.<BR/><BR/>Derek's recommendation has made things a lot clearer.<BR/><BR/>I did already understand the analogy with programming, the reuse of a lemma is similar to the reuse of a function and cut elimination is like function application. (And Curry-Howard etc. formalises this). But I couldn't understand why logicians would be so hung up on cut elimination.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140816378469858392006-02-24T13:26:00.000-08:002006-02-24T13:26:00.000-08:00As well as the practical reason, there's the philo...As well as the practical reason, there's the philosophical one.<BR/><BR/>Cut elimination basically says 'you can use lemmas'. So we're using cut elimination all the time, and it's essentially a fundamental part of our logic. It's the fact that you don't *have* to use it that's interesting - even though it's in principle unnecesary, we're still going to be using it all the time. Some classical logics do indeed take the principle that because it's redundant you shouldn't take it as an axiom, but they then have to immediately go on to prove it as a metatheorem before they can do anything especially useful! <BR/><BR/>(Which isn't to say that they're wrong in doing so, just that cut elimination will come up regardless of how you slice it).<BR/><BR/>Oh, idle note. The ZF axioms are redundant. Specification follows from replacement, and pairing follows from replacement + power set. I think that's it, but I'm not really sure. They're kept in for more or less the same reason - were they not axioms, you would need to immediately make them theorems.David R. MacIverhttp://www.blogger.com/profile/12893796777558636623noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140809363545919202006-02-24T11:29:00.000-08:002006-02-24T11:29:00.000-08:00I'm glad Derek posted as he did. It seemed to me t...I'm glad Derek posted as he did. It seemed to me that this had to be the reason: namely that the cut-rule, though redundant, makes things a lot easier. <BR/><BR/>In theoretical computer science, we often wave our hands around machine models because we know that somewhere it can be shown that they are mostly equivalent. And so a result that shows that a particular machine model is not special is very important, even if one goes on proving results in that machine model.Sureshhttp://www.blogger.com/profile/16443460499476270978noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140809058002083392006-02-24T11:24:00.000-08:002006-02-24T11:24:00.000-08:00Hi Derek. At one point that paper asks "what is th...Hi Derek. At one point that paper asks "what is the point of sequents?" and proceeds to answer. And it asks "what is the price for eliminating cuts?", which is the subject of the paper. In other words, it has informal text that asks the kinds of questions that I've been asking myself. This is excellent. Exactly what I'm looking for. It even talks a little about linear logic which is my longer range target. Many thanks!sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1140807005079677192006-02-24T10:50:00.000-08:002006-02-24T10:50:00.000-08:00http://www.ams.org/bull/1997-34-02/S0273-0979-97-0...<A HREF="http://www.ams.org/bull/1997-34-02/S0273-0979-97-00715-5/S0273-0979-97-00715-5.pdf" REL="nofollow">http://www.ams.org/bull/1997-34-02/S0273-0979-97-00715-5/S0273-0979-97-00715-5.pdf<BR/></A><BR/><BR/>Here's an article about removing the cut rule. Apparently, you can do proofs without, but the proofs become much more complicated.Derekhttp://www.blogger.com/profile/12934077022923410500noreply@blogger.com