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!
posted by Jon @ 10:41 AM
4 Comments:
Yes, I'm not sure if I agree with me either. I think that if you're constructing proofs from premises to a 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 tactics of proof-search. (It becomes even more fun in multiple-premise, multiple-conclusion natural deduction, but that's another matter entirely...)
Posted by Greg Restall
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 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 Jon
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.
Posted by Z (just a random reader)
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.
Posted by Kenny Easwaran
Post a Comment
<< Home