Return to Question

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

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

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

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

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 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(\varphi) \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(\varphi) \to \varphi$.

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