Timeline for Reflection principles
Current License: CC BY-SA 3.0
25 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 12, 2013 at 3:06 | history | protected | Andrés E. Caicedo | ||
| Jul 2, 2013 at 22:53 | history | edited | jeq | CC BY-SA 3.0 |
Improved mark-up
|
| Mar 7, 2013 at 21:23 | vote | accept | Jaykov Foukzon | ||
| Mar 7, 2013 at 21:23 | vote | accept | Jaykov Foukzon | ||
| Mar 7, 2013 at 21:23 | |||||
| Mar 7, 2013 at 18:12 | comment | added | user10290 | Thanks for clarifying which type of reflection principle this question asks about, and sorry for the redundant comment, I didn't understand some of the comments before. | |
| Mar 7, 2013 at 14:57 | history | edited | Jaykov Foukzon | CC BY-SA 3.0 |
added 29 characters in body; added 2 characters in body; Post Made Community Wiki
|
| Mar 7, 2013 at 14:33 | answer | added | Andreas Blass | timeline score: 4 | |
| Mar 7, 2013 at 4:27 | comment | added | Everett Piper | Erin, I'm curious about the specific reflection principle you're interested in. It seems you are interested primarily in set theory so it may very well be the case that you are interested in a set-theoretic reflection principle as opposed to a proof-theoretic principle. Proof-theoretic principles are typically formalized versions of the intuition that a particular proof-system or set of axioms is sound. Set-theoretic reflection principles seem to express the intuition that certain kinds of structure in V keep repeating or reflecting arbitrarily high up in the cumulative hierarchy. | |
| Mar 7, 2013 at 4:16 | comment | added | Everett Piper | principles. For example, there really is no "good" formalization of "is provable" in the sense that there are lots of non-standard proof predicates that can be constructed and there is no mathematical distinction between the non-standard and standard proof predicates. There is also ambiguity in the sentence(s) formalizing that S is a consistent theory (or has a model, or has an omega-model, etc.). There is an excellent article (and also a book) by Torkel Franzen. Smorynski's article in the Handbook of Mathematical Logic is also a good place to start. I can provide lots more info/literature if | |
| Mar 7, 2013 at 4:10 | comment | added | Everett Piper | It might be worthwhile to note the reflection principle mentioned by Jaykov is actually a schema; there is such a conditional for every sentence $\phi$ in the formal language being used. Further, the intuitive reading for each individual member of the scheme is something like "If S proves $\Phi$ then $\Phi$ is true (or $\Phi$ holds, or whatever variation you prefer)". For arbitrary $\Phi$ this is known as the Uniform Reflection Principle for S. Feferman (Turing, Beklemishev, Smorynski and others) have shown that there are all kinds of subtleties involving these proof-theoretic reflection | |
| Mar 6, 2013 at 23:33 | history | edited | Jaykov Foukzon | CC BY-SA 3.0 |
added 10 characters in body
|
| Mar 6, 2013 at 23:24 | history | edited | Jaykov Foukzon | CC BY-SA 3.0 |
added 149 characters in body; added 2 characters in body; added 2 characters in body
|
| Mar 6, 2013 at 23:12 | comment | added | user10290 | I am interested in a very specific reflection principle, and would like to understand this question. Please, could you please explain the meaning of Bew_{S}(A_M) --> A_M? What are the definitions of "Bew" and "A_M"? | |
| Mar 6, 2013 at 23:11 | comment | added | Jaykov Foukzon | jdh.hamkins.org I asking also for an explanation of the paradox in the link cs.nyu.edu/pipermail/fom/2007-October/012035.html of the case S=ZFC+ omega-model? | |
| Mar 6, 2013 at 23:02 | comment | added | Jaykov Foukzon | wff being "over M" meant an wff with bounded quantifiers restrict by M. | |
| Mar 6, 2013 at 22:57 | comment | added | Ali Enayat | I am with Andreas in his interpretation; and I suspect that the phrase "is satisfied" at the end of the question was meant to be "is satisfied in M$. In this reading, the answer is clearly YES. | |
| Mar 6, 2013 at 22:45 | comment | added | Andreas Blass | Of course Bew_S(X)--->X is true for any X, because all the axioms of S are true. But that argument uses information that goes beyond ZFC, so presumably the question should be whether Bew_S(A_M)--->A_M is provable in some (yet to be specified) formal system. It should also be explained what is meant by a wff being "over M" and in particular why such a wff is in the language of S so that Bew_S(A_M) makes sense. | |
| Mar 6, 2013 at 22:41 | comment | added | Andreas Blass | Joel, I think Bew_S(A_M) is supposed to be (a formalization of) the statement that A_M is provable in S. ("Bew" was, I believe, used by Gödel to abbreviate "beweisbar".) | |
| Mar 6, 2013 at 22:39 | comment | added | Jaykov Foukzon | Bew_{S}(A_M) mean that A_M is provable in S. | |
| Mar 6, 2013 at 22:35 | comment | added | Joel David Hamkins | I don't know what Bew_S(A) means here. Are you asking for an explanation of the paradox in the link you mention? | |
| Mar 6, 2013 at 22:31 | comment | added | Jaykov Foukzon | cs.nyu.edu/pipermail/fom/2007-October/012035.html | |
| Mar 6, 2013 at 22:25 | history | edited | Jaykov Foukzon | CC BY-SA 3.0 |
added 29 characters in body
|
| Mar 6, 2013 at 22:20 | comment | added | Joel David Hamkins | Could you explain what does $Bew_S(A_M)$ mean? Also, perhaps you could re-word your final question somehow; I don't really understand it as it is written. | |
| Mar 6, 2013 at 21:45 | history | edited | Jaykov Foukzon | CC BY-SA 3.0 |
added 6 characters in body
|
| Mar 6, 2013 at 21:37 | history | asked | Jaykov Foukzon | CC BY-SA 3.0 |