3
$\begingroup$

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$.

Improve this question
$\endgroup$
12
  • $\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
    Commented Nov 15, 2015 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
    Commented Nov 15, 2015 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
    Commented Nov 15, 2015 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
    Commented Nov 16, 2015 at 1:23
  • 3
    $\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
    Commented Nov 16, 2015 at 1:40

3 Answers 3

Reset to default
6
$\begingroup$

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.

Improve this answer
$\endgroup$
2
$\begingroup$

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").

Improve this answer
$\endgroup$
1
$\begingroup$

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

Improve this answer
$\endgroup$
0

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .