### Doing Proofs

Casually reading through Greg Restall's book on substructural logics, I came across a curious line:

"However, proofs are not so easy to construct in tree form - often it is easier to construct proofs writing the consecutions in a list."

Personally, I have always found the "list" way of constructung proofs to be rather arbitrary and nonintuitive. If I have access to a sequent(esque) system, then I invariably construct the proof by doing a backwards "proof search". But maybe that is because I cut my (logical) teeth by working on theorem proving software.

I'm interested in seeing what method other people prefer, so leave a comment if you have a preference!

## 4 Comments:

Yes, I'm not sure if I agree with me either. I think that if you're constructing proofs

Greg Restall

frompremisestoa conclusion, the benefit of a list is that you can start with your premises before worrying about how they're going to be used. In Gentzen/Prawitz-style natural deduction, where the premises actually end up depends on how they're used. In Lemmon-style natural deduction, any proof from a premise set X can start with each premise in X as the first steps in the proof, before you worry about making other assumptions or anything else.I think that is what I was thinking back then.

I am still trying to articulate my views on the

tacticsof proof-search. (It becomes even more fun in multiple-premise, multiple-conclusion natural deduction, but that's another matter entirely...)Posted by

I agree that "list" style may be better if one is starting from premises. Obviously though, the problem then is "guiding" the proof properly. I have some frivolous ideas related to generating

Jon

random"proofs" thoughs. One example of this is, I guess, generating random sentences based on a Lambek calculus, which would then come equipped with a proof of their "grammaticality". The dynamics could be interesting because there are lots of "proofs" starting from "s" (for example), corresponding to different correct sentence structures.Being a lazy programmer, however, I haven't gotten around to hacking something like that up yet.

Posted by

I learned logic the list-way, and thought that was easier. Then I used theorem proving tools for a while with Gentzen-style sequents, and now I can't understand why I ever liked list-proofs.

Z (just a random reader)

Posted by

Until teaching logic this fall, I was almost incapable of doing proofs more than four lines or so long by hand - I was content to prove metatheorems and let them do all the work. I do seem to remember trees being easier to actually use to construct proofs, though the lists are more natural to think of as a representation, at least when you first come to formal proofs.

Kenny Easwaran

Posted by

Post a Comment

<< Home