The n-Category Café

It’s frequently important to distinguish between syntactic strings and their propositional content. In semantic theory, a proposition is defined to be the semantic content of a sentence, so that synonymous sentences have the same content (express the same proposition). Propositions themselves aren’t syntactic entities. No one really has a good theory of propositions, although there are hundreds of articles and many books on the topic. It was the source of a famous correspondence between Frege and Russell around 1902.

If $L$ is a formalized language with alphabet $A$, then $A^{\ast}$ is the set of finite sequences from $A$ (these are the strings or words from $A$). A certain inductively subset of these are the terms of $L$ and a certain inductively defined subset are the formulas of $L$, and the sentences of $L$ are those formulas with no free variables.

Let $L$ be the formalized language of arithmetic with signature $\{\underline{0},s,+,\times\}$. It contains a constant $\underline{0}$ and function symbol $s$. The sequence of terms $\underline{0}, s\underline{0}, ss\underline{0}, sss\underline{0}, \dots$ are called canonical numerals. In general, $\underline{n}$ is the $n$th canonical numeral. Under the intended interpretation $\mathbb{N}$, we have $(\underline{n})^{\mathbb{N}} = n$, so $\underline{n}$ denotes (refers to) $n$.

Where $A^{\ast}$ is the set of strings from $L$, we can code these strings as numbers, using a godel coding function $f : A^{\ast} \to \mathbb{N}$. So, if $E$ is a string from $L$, then it has a godel code $f(E)$. If $n = f(E)$, then it is denoted by the numeral $\underline{n}$, and this is written: $\lceil E \rceil$. This closed term behaves like a quotation name of the string $E$.

For the version of Tarski’s T-scheme you’ve written down at the n-lab post, note that it is inconsistent with very weak principles of arithmetic. The instances are called T-sentences, and have the form $T(\lceil \phi \rceil) \leftrightarrow \phi$, where $\phi$ is a sentence of $L$. Suppose $Q$ is the very weak theory known as Robinson arithmetic. For any formula $\Psi(x)$, there is a sentence $G$ such that $Q$ proves $G \leftrightarrow \Psi(\lceil G \rceil)$. In particular, if one has a truth predicate $T(.)$ lying around, there is a sentence $\lambda$ such that $Q$ proves $\lambda \leftrightarrow \neg \T(\lceil \lambda \rceil)$. This contradicts the T-sentence $T(\lceil \lambda \rceil) \leftrightarrow \lambda$. So, one cannot consistently add the set of all T-sentences to any theory which extends (or interprets) $Q$.

David, at the n-lab post on propositional extensionality, you write,

Hence propositional extensionality in type theory is the statement that $('P' = 'Q') \simeq (P \simeq Q)$.

Let me rewrite this as,

$(\lceil \phi \rceil = \lceil \theta \rceil) \leftrightarrow (\phi \leftrightarrow \theta)$.

because I’m not sure of the intended formal rules for $\simeq$. (I suspect that, formally, $\simeq$ behaves like a strong biconditional, such as $\square (\phi \leftrightarrow \theta)$, but let’s go with $\leftrightarrow$.)

This axiom will fail when $\phi$ and $\theta$ are distinct but logically equivalent formulas, because $\phi \leftrightarrow \theta$ is true, even though $\phi$ is distinct from $\theta$. Even if you replace your identity symbol = by some arbitrary relation symbol, say $E$, the result is inconsistent with $Q$. E.g.,

$E(\lceil \phi \rceil, \lceil \theta \rceil) \leftrightarrow (\phi \leftrightarrow \theta)$.

For let $\theta$ be $\top$, some arbitrary tautology. Then $\phi \leftrightarrow \top$ is equivalent to $\phi$, by a truth table. So, the axiom implies,

$E(\lceil \phi \rceil, \lceil \top \rceil) \leftrightarrow \phi$.

Define the formula $T(x)$ to mean $E(x,\lceil \top \rceil)$. So, the axiom implies,

$T(\lceil \phi \rceil) \leftrightarrow \phi$.

But this is the T-scheme, and it is inconsistent with Robinson arithmetic $Q$, as I mentioned before, because one can define a “liar” sentence $\lambda$ such that

$Q \vdash \lambda \leftrightarrow \neg T(\lceil \lambda \rceil)$

I wouldn’t say that. It’s true that there is variety in whether type theories use Tarski or Russell universes, but I wouldn’t consider that a point of disagreement in the community. It’s just a choice to be made when formulating a type theory formally, and I don’t think there’s a right or a wrong choice; each choice has its uses.

Jeffrey is of course right that propositional extensionality means that even the “names of propositions” that it refers to are not purely syntactic objects but already have been “semanticized” to some extent. The disagreement I was referring to has to do not so much with anything formal, but rather with to what things the word “proposition” should apply: types (truncated or not), or the syntax describing types, or something in between.

“How tall is $X$?”