Timeline for Semantic reflection
Current License: CC BY-SA 3.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 16, 2015 at 4:11 | answer | added | Nik Weaver | timeline score: 2 | |
| Nov 16, 2015 at 1:40 | comment | added | Joel David Hamkins | I stand by my remarks. If you don't have $\Phi\subset\Sigma^0_n$, at least up to equivalence, then $\Phi$-truth is not generally expressible by a formula in the language of arithmetic. And if you do have this and use the standard $\Sigma^0_n$ truth predicate, then the implication is easily provable in a very weak theory. Your question is about what $T$ proves, and so it must involve non-standard models. From my perspective, your question has some fundamental confusion concerning the treatment of truth predicates. | |
| Nov 16, 2015 at 1:39 | history | edited | Kaveh | CC BY-SA 3.0 |
added 4 characters in body
|
| Nov 16, 2015 at 1:37 | comment | added | Kaveh | @Joel, sorry, but I don't see which part is confusing. Maybe I should have used $Tr_{\Phi}$. $Tr$ is a first-order formula that in the standard model represents the truth of formulas in $\Phi$. I don't talk about any model other than the standard model anywhere. The last part of your comment is not correct. It might help to think $\Phi$ as a complexity class like $NC^1$. (I used Godel coding because it is more familiar but it is not a good one from complexity perspective.) | |
| Nov 16, 2015 at 1:23 | comment | added | Joel David Hamkins | (Your link doesn't work for me, since my quota is used up in that book, but thanks anyway; I don't need an example.) Also, in the question you at first define Tr as truth-in-the-standard-model, but now you are saying that Tr(x) refers to truth-as-defined-in-the-model for formulas of uniformly bounded complexity, and this is not the same thing. Of course, with this latter definition, then any theory $T$ that is able to implement the Godel coding will prove your implication, by a simple induction on formulas. So basically every theory $T$ has that property. | |
| Nov 16, 2015 at 1:22 | comment | added | Kaveh | @Joel, of course, that is why it is restricted to work only for $\Phi$. I don't think there is a need to state that $\Phi \subseteq \Sigma^0_n$. I have a class of formulas $\Phi$ and first-order formula that defines the truth predicate for the formulas in $\Phi$. If you want an example, check here. I just want to check if there is a standard name for the property before using something like "semantic reflection" to refer to it. | |
| Nov 16, 2015 at 1:11 | comment | added | Joel David Hamkins | That isn't possible in the generality in which you stated your question, for example, when $\Phi$ is all formulas, or includes formulas of unbounded complexity. If that is what you meant, then you should state so more explicitly in the question, and also state that $\Phi\subset\Sigma^0_n$ for some finite $n$. | |
| Nov 16, 2015 at 1:07 | comment | added | Joel David Hamkins | My point was that PA does not include any reference to a predicate symbol Tr, and it can't prove anything of consequence about some new unary predicate symbol, since PA doesn't know anything about the fact that you wanted to interpret it as a truth predicate in the standard model. Rather, you can prove things about $\Sigma^0_n$ truth when you define the truth predicate in the theory as such. So PA+"Tr is the $\Sigma^0_n$ truth predicate" can prove things about Tr. That is, you must make the underlying assumptions about what Tr is part of the theory. | |
| Nov 16, 2015 at 1:04 | history | edited | Kaveh | CC BY-SA 3.0 |
added 7 characters in body
|
| Nov 16, 2015 at 1:02 | answer | added | Bjørn Kjos-Hanssen | timeline score: 1 | |
| Nov 16, 2015 at 1:01 | comment | added | Kaveh | @Joel, it is not true that PA cannot prove anything about Tr. It can for restricted classes of formulas e.g. $\Phi = \Sigma^0_0$. | |
| Nov 16, 2015 at 0:56 | history | edited | Kaveh | CC BY-SA 3.0 |
added 40 characters in body
|
| Nov 15, 2015 at 23:29 | comment | added | Joel David Hamkins | ...If by "arithmetic", you mean that the axioms of $T$ are in the language of arithmetic, then no such $T$ will have your property, for the same reason. So I guess you intend really to consider arithmetic theories to which the implications you discuss have been added as axioms. The situation with provability is totally different, since provability is formalizable in the language of arithmetic. But truth is not, by Tarski's theorem on the non-definability of truth. | |
| Nov 15, 2015 at 23:29 | comment | added | Joel David Hamkins | What I find strange about your question is that in the first part, you provide what amounts to an interpretation of the predicate Tr in the standard model, but then in the latter part, you are asking about provability concerning this predicate. Of course, PA proves nothing about this new predicate, and so PA definitely does not have this property, since for all it knows, Tr(x) means "x is prime" or whatever. | |
| Nov 15, 2015 at 23:25 | comment | added | Joel David Hamkins | You introduced the Gödel brackets in the beginning, but then you didn't use them when stating your property. | |
| Nov 15, 2015 at 19:27 | history | edited | Kaveh | CC BY-SA 3.0 |
added 159 characters in body
|
| Nov 15, 2015 at 19:18 | history | edited | Kaveh | CC BY-SA 3.0 |
added 159 characters in body
|
| Nov 15, 2015 at 19:10 | comment | added | Andrej Bauer | Ah, I misunderstood. Perhaps it would be clearer to say then "let $Tr$ be the formula expressing the truth conditions of the formulas in $\Phi$" or just "Let $Tr$ be the truth predicate for formulas in $\Phi$". | |
| Nov 15, 2015 at 18:43 | comment | added | Andrej Bauer | I would expect falsity $\bot$ to be in $\Phi$ because we can define what it means for $\bot$ to be true. You should probably replace "let $Tr$ be a first-order formula expressing the truth of formulas in $\Phi$" with "let $Tr$ be a first-order formula which describes the true formulas in $\Phi$" or some such. | |
| Nov 15, 2015 at 16:23 | answer | added | Ali Enayat | timeline score: 6 | |
| Nov 13, 2015 at 16:11 | history | edited | Kaveh | CC BY-SA 3.0 |
added 213 characters in body
|
| Nov 13, 2015 at 16:05 | history | asked | Kaveh | CC BY-SA 3.0 |