Timeline for Why are universal introduction and existential elimination valid inference rules?
Current License: CC BY-SA 2.5
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 5, 2010 at 8:50 | comment | added | Neel Krishnaswami | @Joel: IIRC Skolemization doesn't work for intuitionistic logic, and even classically requires introducing higher-type function constants for nested quantifier alternations. It seems simpler to explain substitution correctly in the first place! The proof style you describe is also captured in the rule above, where to prove $forall x. \theta(x)$, you assume $x$ hypothetically and prove $\theta(x)$. You might enjoy the chapter of Paul Taylor's Practical Foundations of Mathematics where he shows how to convert mathematical vernacular to and from natural deduction. | |
| Feb 5, 2010 at 2:08 | comment | added | Charles Stewart | Managing free variables: Lambek & Scott (1986) Introduction to Higher-Order Categorical Logic do exactly this in their treatment of quantified inference. With a nice notation: the set of variables are subscripts to the turnstile. | |
| Feb 5, 2010 at 2:05 | comment | added | Charles Stewart | @Francesco: Lloyd (1987) Foundations of Logic Programming covers the theory of Skolematisation and Herbrandisation well. | |
| Feb 4, 2010 at 22:00 | comment | added | Joel David Hamkins | But is the notation really bad? Surely this method is used throughout ordinary mathematical practice. For example, a group theorist wants to prove that every group has a certain property, so she says "Let G be a group..." and then proves it just for G. To conclude that every group has the property is exactly the universal introduction rule as stated. | |
| Feb 4, 2010 at 16:52 | comment | added | Neel Krishnaswami | Negri and van Plato's Structural Proof Theory ought to have a sensible explanation of this stuff, though I don't have a copy handy. | |
| Feb 4, 2010 at 14:31 | comment | added | Francesco Turco | @NeelKrishnaswami: Do you know any good book or set of notes that uses a coherent notation and deals with Skolem constants? Thanks. | |
| Feb 4, 2010 at 14:19 | comment | added | Harry Gindi | I wasn't faulting you for it, I was just letting Neel know where your answer went, since he noted your post in his. | |
| Feb 4, 2010 at 13:49 | comment | added | Andrej Bauer | Well, that seemed like the best thing to do. Why would I spread my own confusion? | |
| Feb 4, 2010 at 13:41 | comment | added | Harry Gindi | Andrej probably just realized that the first question was about introduction, so he deleted all of his answers and comments. | |
| Feb 4, 2010 at 13:32 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |