More on Last Time's Subject

The system I suggested last time, at the end, can actually be stated in a much simpler (more standard) way.

Rather than adding in a totally new notation for representing enumerations of sentences in a Turing-complete manner, all we really need is to allow the use of arbitrary function symbols when making assertions. This sounds trivial! However (as the considerations from last time show) it makes a big difference in the actual behavior of the system.

Added function symbols are a standard part of the machinery of first-order logic, so in some ways it seems only natural to allow their use in first-order arithmetic. However, they are not normally considered a part of that language; functions in first-order arithmetic must be constructed rather than defined.

Considering functions part of the language obviously proves no new theorems about arithmetic, because we don't add any axioms that include the function symbols. The only thing that changes is what we can say. So what can we say?

Well, it allows us to say a whole lot. With function symbols, we can go as far as defining a truth predicate for arithmetic! This means that we can build the metalanguage for arithmetic. We can also go further, building the metametalanguage (the language containing the truth predicate for the metalanguage), et cetera. However, don't be fooled; there is an important difference between being able to build it and having it as part of the system. Normally when we talk about a language containing the truth predicate we mean that we've already got the rules to make it work in the axioms, not that we can add them if we like.

Adding function symbols to arithmetic follows the advice of the edit to the previous post, namely, we don't include any claim that the added statements are true just because all the sentences of arithmetic that they imply are true. This is essentially because the logical system is treating the function-symbols as actual things, not just as notational conveniences. The logic thinks there is a truth of the matter about how "F" behaves, even before we add axioms to define its behavior. It has no idea what that truth is, but it assumes that the truth exists. So even if a particular function-based statement implies only true statements about arithmetic, and so looks totally un-risky, the logic still will think that it implies a bunch of risky statements about the function symbols involved.

It would be interesting to develop a semantics for the function-symbols that did not result in this conclusion... however, as mentioned in the previous post, in that direction there is a strong risk of paradox. Some sort of non-classical system of truth values will almost certainly be needed.