Let $\ulcorner \cdot \urcorner$ be a fixed encoding of formulas by numbers, e.g. let $\ulcorner \varphi \urcorner$ denote the Godel number of $\varphi$. Let $T$ be a first-order arithmetic theory, e.g. PA. Let $\Phi$ be a class of closed first-order formulas e.g. $\Sigma^0_1$. Let $Tr$ be a first-order formula defining the truth predicate for the formulas in $\Phi$ in the standard model:

for all $\varphi \in \Phi$, $\mathbb{N} \vDash \varphi$ iff $\mathbb{N} \vDash Tr(\ulcorner \varphi \urcorner)$

E.g. we have: $\mathbb{N} \vDash Tr(\ulcorner \top \urcorner)$, $\mathbb{N} \nvDash Tr(\ulcorner \bot \urcorner)$, $\mathbb{N} \nvDash Tr(\ulcorner \exists x \ (x + 1 = 0)\urcorner)$, etc.

Consider the following property:

for all $\varphi \in \Phi$, $T \vdash Tr(\ulcorner \varphi \urcorner) \to \varphi$.

Does this property have a standard name?

The reflection is similar to the property above with truth replaced with provability: let $\square$ denote the provability in theory $T'$. Then reflection property is:

for all $\varphi \in \Phi$, $T \vdash \square(\ulcorner \varphi \urcorner) \to \varphi$.

| cite | improve this question | | | | |
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Nov 15 '15 at 18:43
  • $\begingroup$ 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$". $\endgroup$ – Andrej Bauer Nov 15 '15 at 19:10
  • $\begingroup$ You introduced the Gödel brackets in the beginning, but then you didn't use them when stating your property. $\endgroup$ – Joel David Hamkins Nov 15 '15 at 23:25
  • 1
    $\begingroup$ (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. $\endgroup$ – Joel David Hamkins Nov 16 '15 at 1:23
  • 2
    $\begingroup$ 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. $\endgroup$ – Joel David Hamkins Nov 16 '15 at 1:40

Biconditionals of the form $Tr(\varphi) \leftrightarrow \varphi$ are known as T-sentences in the literature of philosophical logic, and they date back to Tarski's groundbreaking work on the notion of truth in formalized languages.

However, I have not seen a special name for implications of the form mentioned in the question.

| cite | improve this answer | | | | |

The law $${\rm Tr}(\ulcorner \phi\urcorner) \to \phi$$ is sometimes called the "release scheme". "T-Elim" and "T-Out" are also used, according to this source. The converse is "capture scheme" ("T-Intro", "T-In").

| cite | improve this answer | | | | |

At the risk of stating the obvious, in modal logic the axiom schema $$\Box\varphi\rightarrow\varphi$$ is called the schema T.

| cite | improve this answer | | | | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.