Timeline for Subtler than meets the eye: does x=y imply forall x forall y x=y? [closed]
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 29, 2011 at 18:56 | history | closed |
Andrés E. Caicedo Ryan Budney Andreas Blass Simon Thomas Noah Snyder |
not a real question | |
| Jul 29, 2011 at 17:35 | comment | added | Emil Jeřábek |
(There must have been mist over my eyes or something. Of course, $\forall x\forall y\,x=y$ is not provable, $\forall x\,x=x$ is.)
|
|
| Jul 29, 2011 at 17:13 | answer | added | Peter LeFanu Lumsdaine | timeline score: 1 | |
| Jul 29, 2011 at 10:15 | comment | added | Emil Jeřábek |
@Sam: The completeness theorem is usually formulated so that it only applies to provability from a set of sentences, in which case the distinction disappears. In any case, in your particular example, $\forall x\forall y\,x=y$ is provable by itself without any assumptions.
|
|
| Jul 29, 2011 at 7:28 | comment | added | Sam Alexander | You're absolutely right of course. It does raise some interesting questions for logicians though. The Completeness Theorem says x=y implies forall x forall y x=y iff x=y proves forall x forall y x=y. If the completeness theorem is true according to both authors' texts, it necessarily means the things which are formally provable are different. Best I can tell, this hinges on whether or not the Rule of Generalization is allowed: from phi, deduce forall x phi. (But to sour things, Bilaniuk does NOT include this rule. Plot hole?) | |
| Jul 29, 2011 at 7:15 | answer | added | Andreas Blass | timeline score: 5 | |
| Jul 29, 2011 at 7:13 | comment | added | Ryan Budney | In every field there are common symbols that are used for different purposes by different authors. Why should this be a conundrum? | |
| Jul 29, 2011 at 6:58 | history | asked | Sam Alexander | CC BY-SA 3.0 |