Formalism, Platonism and Mentalese

This is a sequel to an earlier post on Tarski and Mentalese.  I am writing this sequel for two reasons. First, I just posted a new version of my treatment of type theory which focuses on “naive semantics”. I want to explain here what that means. Second, after many attempts to get formalists to accept Platonic proofs I have decided that it is best to approach the issue from the formalist point of view. In this new approach I present Platonism as just a translation from a formal language (such as a programming language or mathematical logic) to some symbolic internal mentalese. Human mathematical thought can presumably be modeled, to some extent at least, as symbolic computation involving expressions of mentalese.  Formalists will accept the idea of a symbolic language of thought but some deep learning people resist the idea that symbolic computation is relevant to any form of AI.  I will avoid that latter discussion here and assume that a mentalese of mathematics exists.

To understand the issues of formalism vs. Platonism and the relationship of both to semantics it is useful to consider an example. In type theory we have dependent pair types. These are written fairly obscurely as $\Sigma_{x:\sigma} \;\tau[x]$.  This expression denotes a type (think class). An instance of this type (or class) is a pair $(x,y)$ where $x$ is an instance of the type $\sigma$ and $y$ is an instance of the type $\tau[x]$ where $\tau[x]$ is a type (class) whose definition involves the value $x$.  To make this more concrete consider the following example.

DiGraph = $\Sigma_{s:set}\;(s \times s \rightarrow \mathbf{Bool})$

This is the type (or class) of directed graphs where we are taking a directed graph to be a pair $(N,P)$ where $N$ is a set of “nodes” and $P$ is an “edge predicate” on the nodes which is true of two nodes if there is a directed edge between them.

The above paragraph defines the notation $\Sigma_{x:\sigma}\;\tau[x]$ in a way that would be sufficient when introducing notation in a mathematics class.   Mathematical notation is generally defined before it is used.  Above we define the notation $\Sigma_{x:\sigma}\;\tau[x]$ in much the same way that any mathematical notation is defined in the practice of mathematics. A simpler example would be to introduce the symbol $\cup$ by saying that for sets $s$ and $u$ write $s \cup u$ to denote the union of the sets $s$ and $u$.  This style of definition provides a translation of formal notation into the natural language (such as English) which is the language of mathematical discourse in practice.

But logicians are not satisfied with this style of definition.  They prefer a more formal treatment known as Tarskian compositional semantics.  My previous post introduces this by treating the semantics of arithmetic expressions.  We introduce a value function ${\cal V}[e]\rho$ where $e$ is an arithmetic expression and $\rho$ is a variable interpretation assigning a value to the variables occurring in $e$.  Now consider how notation is defined in mathematics.  We might say “we write $n!$ for the the product of the natural numbers from 1 to $n$”.  We can write a compositional semantics specification of the meaning of $n!$ as follows.

$V[e!]\rho \equiv \prod_{i=1}^{V[e]\rho}\;i$

Here $V[w]\rho$ is the notation for the value of $e$ under variable interpretation $\rho$.  This looks more explicitly like a translation between formal notations. However, this notation assumes that the product notation is already understood — can be reasoned about in internal mentalese.  This notation can still be interpreted as a translation from an external notation to mentalese.

In type theory, as in most programming languages, variables are typed.  A math class might start with the sentence “Let $B$ be a Banach space.”.  In type theory this is a declaration of the variable $B$ as being of type “Banach space”.  A set of variable declarations and assumptions constraining the variable values is called a “context”. Contexts are often denoted by $\Gamma$.  In my work on type theory I subscript the value function with a context declaring the types of the free variables that can occur in the expression. For example we might have

$V_{G:\mathbf{DiGraph}}\;[e[G]]\rho$

Here $\rho$ must assign a value to the variable $G$ and that value must be a directed graph.  The type of directed graphs can be expressed as a dependent pair type as described above.

The phrase “naive semantics”, or more specifically “naive type theory”, involves assigning the expressions  their naive meaning.  For example we have

$V_\Gamma[\Sigma_{x:\sigma}\;\tau[x]]\rho =\{(a,b),\;a \in V_\Gamma[\sigma]\rho,\;b \in V_{\Gamma;\;x:\sigma}[\tau[x]]\rho[x \leftarrow a]\}$

This is just the first definition of the dependent pair type notation given above expressed within a Tarskian compositional semantics.  The above definition can be viewed as simply providing a translation of a formal expression into the notation of practical mathematical discourse and hence as a translation of formal expressions into the language of mentalese.

Of course when push comes to shove mathematics grounds out in sets. The notion of “set” is taken to be primitive and is not defined in terms of more basic notions.  We have learned, however, to be precise about the properties of sets using the axioms of ZFC.  In the modern understanding of sets (since about 1925) we distinguish sets from classes where classes are collections too large to be sets such as the collection of all groups or the collection of all topological spaces.  Naive type theory starts from this (sophisticated) notion of sets and classes and then gives all the other expressions of type theory their naive meanings.  This is no different from the introduction of notation in any particular area of mathematics except that type theory is about all the areas of mathematics — it is part of the foundations of mathematics.

Naive type theory is almost trivial.  However, considerable effort is required to handle the notion of isomorphism within naive type theory.  Handling isomorphism within naive type theory is the main point of my work in this area.