Timeline for Community experiences writing Lamport's structured proofs
Current License: CC BY-SA 2.5
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 6, 2021 at 3:49 | comment | added | Timothy Chow | The difficulties with quotients seem related to the difficulties with defining precisely what it means for two things to be "the same" or "canonically isomorphic." Kevin Buzzard has raised this issue in the context of the real numbers and has also blogged about working with isomorphisms in Lean. Perhaps these difficulties are in some sense unavoidable when you are being completely rigorous. | |
| Feb 4, 2016 at 11:30 | comment | added | darij grinberg | Quotients are a godforsaken mess; it's not just undergrads that are struggling with them. They aren't easy to use in Coq either, unless one essentially constructs them by hand (i.e., instead of equivalence classes one uses objects defined explicitly, with explicit projection and lift maps). | |
| Aug 17, 2010 at 7:57 | comment | added | Per Vognsen | Anthony: By subderivation he means the part of the proof that refers to the representative of the equivalence class. For example, say you're working with the rationals represented as pairs of natural numbers p/q. The whole part of the proof that manipulates some p/q must be invariant under multiplying p and q by a nonzero integer. Anyway, I'm not sure I agree with Neel that this is any less of a problem in non-structural proofs; it's just that dealing with these issues formally is a little painful. When possible, one could alleviate part of the pain by working with normal forms. | |
| Aug 17, 2010 at 2:03 | comment | added | Anthony Pulido | Thank you, Per, for pointing that out. If Lamport knew about Jaskowski style natural deduction and its practicality compared to G-P style, its likely he chose to model his method on it. I'll definitely look at Restall's overview more closely. Many thanks again. | |
| Aug 17, 2010 at 1:58 | comment | added | Anthony Pulido | Thanks Neel very much for your comments and for sharing your experience. I'm wondering if you'd clarify your statement "it requires proving something about the whole subderivation which uses the member of the quotient set." I apologize in advance if this is an extremely naive question, but to what is "subderivation" referring? | |
| Aug 16, 2010 at 17:36 | comment | added | Per Vognsen | If anyone is interested in the background of my remark, a quick overview (with an attractively typeset demonstration of Jaskowski-style proof boxes) can be found in the History section, page 44, of Restall's Proof Theory and Philosophy: consequently.org/papers/ptp.pdf | |
| Aug 16, 2010 at 12:35 | comment | added | Per Vognsen | It might be worth mentioning that Lamport's approach more closely follows Jaskowski-style natural deduction rather than the Gentzen and Prawitz style of natural deduction that most people are taught in courses on proof theory, lambda calculus, etc. They represent essentially the same abstract structure but the practical difference in usability is very great. | |
| Aug 16, 2010 at 9:17 | comment | added | Neel Krishnaswami | @Pete: Thanks! Your suggestion is a good one, so I've changed the phrasing a little to fit. | |
| Aug 16, 2010 at 9:14 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
fixed usage
|
| Aug 16, 2010 at 9:13 | history | edited | Pete L. Clark | CC BY-SA 2.5 |
tvaluable |-> valuable
|
| Aug 16, 2010 at 9:12 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
fixed usage
|
| Aug 16, 2010 at 8:54 | comment | added | Pete L. Clark | @Neel: A linguistic comment. In writing math (i) we strive for clarity of meaning above all else and (ii) we have a truly international audience, I think it is a good idea to try to use words and terminology which are maximally transparent. Ideally, someone encountering a term for the first time can reasonably guess its meaning. As a corollary, I think we should try to avoid "tricky" words which mean the opposite of what someone might guess. In this case, you say utterly invaluable, and, though your usage is utterly correct, I can imagine many readers here misinterpreting it. | |
| Aug 16, 2010 at 8:36 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |