## Very Basic Model Theory

18 31 October 2013 07:06AM

In this post I'll discuss some basic results of model theory. It may be helpful to read through my previous post if you haven't yet. Model Theory is an implicit context for the Heavily Advanced Epistemology sequence and for a few of the recent MIRI papers, so casual readers may find this brief introduction useful. And who knows, maybe it will pique your interest:

## A tale of two logics

propositional logic is the "easy logic", built from basic symbols and the connectives "and" and "not". Remember that all other connectives can be built from these two: With Enough NAND Gates You Can Rule The World and all that. Propositional logic is sometimes called the "sentential logic", because it's not like any other logics are "of or relating to sentences" (/sarcasm).

first order logic is the "nice logic". It has quantifiers ("there exists", "for all") and an internal notion of equality. Its sentences contain constants, functions, and relations. This lets you say lots of cool stuff that you can't say in propositional logic. First order logic turns out to be quite friendly (as we'll see below). However, it's not strong enough to talk about certain crazy/contrived ideas that humans cook up (such as "the numbers").

There are many other logics available (second order logic AKA "the heavy guns", ω-logic AKA "please just please can I talk about numbers", and many more). In this post we'll focus on propositional and first-order logics.

## Training Wheels

As a warm-up, let's define "models" for propositional logic.

Remember, logics together with languages produce sentences. Languages of propositional logic are sets of basic symbols. From these symbols and the two connectives of propositional logic (∧ and ¬) we construct our sentences.

For example, from the language `{x, y}` we can build the sentences `x`, `¬x`, `x∧y`, and many more. We cannot build sentences like `hello` (which doesn't use the right symbols) or `¬xy` (which breaks the rules of the logic).

We want to study interpretations for such sentences, where an "interpretation" is some object which assigns a truth value to each sentence. This is denoted by the ⊧ operator: `A⊧B` expresses some form of "A models B as true". This operator is used frequently and in many contexts throughout model theory.

What we're looking for is some object (set) such that there is a relation (⊧) between the object and all sentences generated by the language under consideration. There are many object/relation pairs that assign truth values in a stupid way. For example, an interpretation that assigns "true" to every sentence is quite useless.

Many other interpretations are somewhat useful but still "wrong". For example, there are interpretations of sentences which treat `∧` like implication instead of conjunction. Somebody may have use for such things, but we certainly don't.

We want to narrow our consideration to interpretations where `∧` means "and" and `¬` means "not", so we explicitly require object/relation pairs such that whenever the object models both `φ` and `ψ`, it also models `φ∧ψ`. (And `X⊧φ` iff it is not the case that `X⊧¬φ`, where `X` is the object under consideration.)

If we can find any objects that work like this, we'll be justified in calling them "models". However, we haven't defined any such objects yet — we've only constrained their potential behavior.

Any interpretation of the sentences generated from a language L of propositional logic must assign truth values to all basic sentence symbols in L. It turns out, once we select which sentence symbols are "true", we're done. The rest of the behavior is completely specified by the rules about `∧` and `¬`.

In other words, any object/relation which assigns truth values to sentences according to the above rules is isomorphic to a set S of sentence symbols with the operator `⊧` defined in the obvious way (starting with `S⊧x iff x∈S`).

Exploring this idea gives you a feel for how to define models of a logic.

## More power

Propositional logic is pretty boring. If you want to say anything interesting, you've got to be able to say more than just "and" and "not". Let's move on to a stronger logic.

First-order logic uses the symbols `( ) ∀ ∃ ∧ ¬ ν ' ≡` or equivalent (where ν ν' ν'', etc. are variables) with the familiar syntactic rules. A language of first-order logic has three different types of symbols: relation symbols, function symbols, and constant symbols. The rules of logic are designed such that symbols act as you expect, given their names.

An interpretation of the sentences generated by some language in first-order logic is (as before) an object that assigns each sentence a truth value (via a relation). We narrow these objects down to the ones that treat all the symbols in ways that justify their names.

More specifically, we consider interpretations that have of some "universe" (set) of items. Constant symbols are interpreted as specific items in the universe. Relation/function symbols are interpreted as relations/functions on the universe.

We further restrict consideration to interpretations where the logical symbols act in the intended fashion. For example, we require that the interpretation hold `c≡d` true (where `c` and `d` are constant symbols) if and only if the interpretation of `c` in the universe is equal to the interpretation of `d` in the universe.

All this is pretty mechanical. The resulting objects are "models". Some of the early results in model theory show that these mathematical objects have indeed earned the name.

## Completeness

Completeness is the poster-child of model theory, and it warrants quite a bit of exploration. It's actually saying a few different things. I'll break it down:

1. Theorems of first-order logic are true in every model of first-order logic.

A theorem of first-order logic is something we can prove from the logic alone, such as `(∀ν)(ν≡ν)`. Contrast this with a sentence like `(∃ν)(F(ν)≡c)`, where `F` is a function symbol and `c` is a constant symbol — the truth of this sentence depends entirely upon interpretation.

So what (1) says is that there aren't any models that deny tautological truths of first-order logic. This result should not be surprising: this claim merely states that we picked a good definition for "models". If instead we found that there are models which deny theorems, this would not be some big grand proof about the behavior of first-order logic. Rather, it would mean that we put the "model" label on the wrong group of thingies, and that we should go back and try again.

2. Any sentence true in every model of first-order logic is a theorem of first-order logic.

This is the converse to (1), and it's quite a bit more powerful. This states that the theorems of a language are only the things true in every model of that language. There's no mystery sentence that is true in every model but not provable from the syntax of the logic.

From one point of view, this says that there are no "missing" models that "would have" said the mystery sentence was false (hence "completeness"). From another, this says that all sentences are "well behaved": no sentence "outwits" all models.

It's worth noting that this is where completeness fails for models of second order logic. From one perspective, there must be some "missing models" in second-order logic. From the other perspective, there must be certain sentences which can "outwit" their models (presumably Gödel sentences). I haven't spent any time formally examining these intuitive claims yet; I have much to learn about second-order logic.

I should also note that I've been implicitly assuming completeness for the last two posts by ignoring the syntactic rules of the logics under consideration. The completeness theorem lets me do this, because it states that the results interpreted by first-order models are exactly the same as the results derived from the syntactic rules of first-order logic. Because the completeness theorem holds, I'm allowed to treat the logical sentences as dead symbols and consider the binding `M⊧φ∧ψ iff M⊧φ and M⊧ψ` to be the means by which `∧` obtains its meaning.

When the completeness theorem fails (as it does in stronger logics) then there is a gap between what the rules of the logic allow and what the models of the logic can say. In that case I must separately consider what the rules say and what the models model. This is the edge of my comfort zone; more exploration with second-order logic is necessary.

Fortunately, everything is well-behaved in first order logic. In fact, (1) and (2) above can be made stronger:

3. A set Σ of sentences is consistent if it has a model.

This is another sanity check that we've put the "model" label on the right thing. A set of sentences is inconsistent if it can derive both `φ` and `¬φ` for some sentence φ. (More specifically, Σ is inconsistent if it can derive everything. If there is any sentence that Σ cannot derive, Σ is consistent. Remember that from a contradiction, anything follows.)

Our models are defined such that whenever they model `φ`, they do not model `¬φ` (and vice versa). Thus, if a set of sentences has a model (Σ "has a model" when there is some model that holds true every sentence σ in Σ) then there must be some sentences which Σ cannot deduce (¬σ for each σ in Σ, for instance). Thus, Σ is consistent.

4. A set Σ of sentences has a model if it is consistent.

This is where things get interesting again. This is a stronger version of (2) above: every consistent theory has a model.

This makes a lot of sense after you understand (2) and (3), but don't underestimate its importance. This tells us that for every consistent theory there is some interpretation following the rules which we laid out. Again, this says something positive about our models (they are strong enough to handle any consistent theory) and something negative about the logic (it's not strong enough to permit a consistent theory stating "I cannot be modeled").

Note: I'm not sure what it would mean for a theory to state "I cannot be modeled", nor am I convinced that the idea is meaningful. Again, we're nearing the edge of my comfort zone.

The point is, the completeness theorem for first order logic says "if you hand me a consistent theory, I can build a model of it". This is very useful. We don't have to waste any time worrying whether or not there's an interpretation available that satisfies all our stringent rules about how  actually means "equals" and so on: if the theory is consistent, a model exists.

## Witnesses

There's been a lot of hand-waving going on for the past four points. Let's get back to the models.

In model theory, you're manipulating interpretations for theories. Due to the generality of such work, there are few tools available to manipulate any abstract model. One of the most useful tools in model theory is the ability to extend a model.

Ideally, when you extend a model, you want to make it more manageable without changing its behavior. Our first example of such a technique involves extending a model to add "witnesses".

A "witness" is a constant symbol that witnesses the truth of an existentially quantified sentence. For example, in the language `{S, +, ✕, 0}` of arithmetic, the constant symbol `0` is a witness to the sentence `(∃ν)(Sν≡S0)` (because `0` makes `(Sν≡S0)` true). However, there is no witness to the sentence `(∃ν)(ν≡S0)`, because `1` is not a constant symbol of the language.

However, we can extend a language to add new constant symbols. Specifically, given any model, we can extend the language to contain one constant symbol `ā` for each element `a` in the universe. Then we can extend the model to interpret each `ā` by `a`. Such extension does not change the behavior of the model, but it does give the model a number of nice properties.

A model is said to "have witnesses" if for every existentially quantified sentence shaped like (∃ν)ψ that it models, there is some constant c such that the model models ψ(ν\c) (ψ with ν replaced by c).

Before we discuss them, note a few things:

1. We can also reduce a model & language extended in this way by eliminating the added constants.
2. We can talk about sets of sentences with witnesses if, whenever a sentence shaped like `(∃ν)ψ` is in the set of sentences Σ, there is some constant `c` such that `ψ(ν\c)` is also in Σ.
3. Just as we can extend a model & language so that the model has witnesses, we can extend a set of sentences and language so that the set of sentences has witnesses (by adding a new constant symbol for each existentially quantified sentence). Such extension does not threaten the consistency of a set of sentences.
4. It's easy to construct a model from a consistent set of sentences that has witnesses. The universe is the set of all constant symbols (technically, one element for each equivalent set of constant symbols), and the behavior of function/relation symbols is forced by their behavior on the constant symbols.

Formalize these four points and put them together, and you've just proved the completeness theorem. (Given any consistent set Σ of sentences, add witnesses then make a model then reduce it to the original language, you now have a model of Σ).

## Compactness

The compactness theorem states that A set Σ of sentences has a model iff every finite subset of Σ has a model.

This leads to a pretty surprising result. Let's break it down.

1. If Σ has a model then every finite subset of Σ has a model.

This direction is obvious: any model of Σ is also a model of all subsets of Σ: if a model holds true all sentences σ in Σ then it obviously holds true all sentences σ in any subset of Σ.

2. If every finite subset of Σ has a model then Σ has a model.

This is where things get interesting. Note that we measure the size of a model by measuring the size of its universe. So when we say "a countably infinite model" we mean a model with a countably infinite universe.

The proof of the above is actually quite easy: in first order logic, all proofs are finite. Therefore, any proof of contradiction (and thus inconsistency) must be finite. Since every finite subset of Σ has a model, no finite subset of Σ is inconsistent. Because all inconsistencies are finite, Σ is not inconsistent. Then, by completeness, because Σ is consistent it has a model.

Or, in other words, the compactness theorem says

If Σ wants to be inconsistent it can do it in a finite subset.

When we know that no finite subset of Σ is inconsistent, we know that Σ has a model.

The surprising result that this leads to is as follows:

If a theory T allows arbitrarily large finite models then it has an infinite model.

If you hand me a theory that allows arbitrarily large finite models, I can extend the language by adding countably many constants to the language. Then I can consider the set Σ of sentences built from T joined with sentences of the form "there are at least n distinct constants" for all finite n. Clearly, every finite subset of Σ is satisfied by one of the finite models of T, which come in arbitrarily large sizes — just pick one that fits. Then, by compactness, Σ has a model. The model of Σ has infinitely many constants.

I have just given a fully general recipe for building an infinite model given a theory T that admits arbitrarily large finite models. What does this mean? It means that no theory in first order logic is capable of saying "I admit only finite models". Sentences can say "models must have no more than 10 elements" or "models are allowed to be infinite", but sentences cannot say "My model is finite". This follows directly fro the fact that all proofs of contradiction are finite. You either have a specific limit, or you don't get a limit at all.

## MORE POWER

If you hand me a theory that allows arbitrarily sized finite models, I can hand you back an infinite model.

It gets better.

If you hand me an infinite theory, I can expand it.

Using a method similar to the one above, I can expand T with sentences of the form "there are at least β distinct constants", for all β less than my chosen cardinal α. Following the same argument as above, all finite subsets of this theory have a model so this theory has a model, which obviously is of power α.

In other words, a theory in first-order logic can either say "I am at most `this` big", where `this` is a specific finite number, or "I am `very` big", where `very` is can be any infinite cardinal that you like.

Example: The theory of arithmetic doesn't have a finite cutoff point. There's no maximum number. Countably infinite models are allowed.

Therefore, arbitrarily large infinite models are allowed.

There are countable models of arithmetic (at least one of which you'll find familiar), and there are also models of arithmetic where there are as many "numbers" as there are reals. Then there are bigger models of arithmetic that are saturated, no, dripping with numbers.

Now you understand why first order logic cannot discuss the "standard" model of number theory. No first-order theory can specifically pinpoint "countable" models! A first order theory must either specify a finite maximum size explicitly, or allow models of unfathomable size.

## Even more

I was hoping to get farther than this, but this is a good stopping point. Hopefully you've learned something about model theory. There are many more interesting results yet.

The book Model Theory by Chang and Keisler primarily focuses on introducing new ways to extend arbitrary models (giving them nice properties in the process) and then discusses results that can be gleaned from models extended thus. Focus is also given to special cases where models are well behaved, such as atomic models (which are a sort of minimal model for a given theory) and saturated models (which are a sort of maximal model for a given theory, within a given cardinality. There Are Always Bigger Models).

There's also quite a bit of exploration into manipulating languages (Eliminate Quantifiers To Win Big Prizes!!!) and even manipulating logics (Q. How far beyond first order logic we can go before sacrificing things like completeness and compactness? A. Not very.)

If you're interested in learning more, then… well, I'm probably not the person to talk to. I'm not even halfway through this textbook. But if you're feeling gutsy, consider picking up Model Theory and getting started. Some of the harder concepts would be much easier to work through with other people rather than alone.

In fact, I have a number of notes about trying to learn something difficult on my own (what worked, what didn't) that I plan to share. But that's a story for another day.

Finally, please note that my entire exposure to model theory is half a textbook and some internetting. I guarantee I've misunderstood some things. If you see errors in my explanations, don't hesitate to let me know! My feedback loop isn't very strong right now.

## Mental Context for Model Theory

41 30 October 2013 06:35AM

I'm reviewing the books on the MIRI course list. After my first four book reviews I took a week off, followed up on some dangling questions, and upkept other side projects. Then I dove into Model Theory, by Chang and Keisler.

It has been three weeks. I have gained a decent foundation in model theory (by my own assessment), but I have not come close to completing the textbook. There are a number of other topics I want to touch upon before December, so I'm putting Model Theory aside for now. I'll be revisiting it in either January or March to finish the job.

In the meantime, I do not have a complete book review for you. Instead, this is the first of three posts on my experience with model theory thus far.

This post will give you some framing and context for model theory. I had to hop a number of conceptual hurdles before model theory started making sense — this post will contain some pointers that I wish I'd had three weeks ago. These tips and realizations are somewhat general to learning any logic or math; hopefully some of you will find them useful.

Shortly, I'll post a summary of what I've learned so far. For the casual reader, this may help demystify some heavily advanced parts of the Heavily Advanced Epistemology sequence (if you find it mysterious), and it may shed some light on some of the recent MIRI papers. On a personal note, there's a lot I want to write down & solidify before moving on.

In follow-up post, I'll discuss my experience struggling to learn something difficult on my own — model theory has required significantly more cognitive effort than did the previous textbooks.

## Between what was meant and what was said

Model theory is an abstract branch of mathematical logic, which itself is already too abstract for most. So allow me to motivate model theory a bit.

At its core, model theory is the study of what you said, as opposed to what you meant. To give some intuition for this, I'll re-tell an overtold story about an ancient branch of math.

In olden times, Euclid built Geometry upon five axioms:

1. You can draw a straight line segment between two points.
2. You can extend line segments into infinitely straight lines.
3. You can draw a circle from a straight line segment, with the center at one end and radius the line segment.
4. All right angles are congruent.
5. If two lines are drawn which intersect a third in such a way that the sum of the inner angles on one side is less than two right angles, then the two lines inevitably must intersect each other on that side if extended far enough.

One of these things is not like the other. The fifth axiom is the only one which requires some effort to understand. Intuitively, it states that parallel lines do not intersect. This statement irked Euclid for reasons apart from the ugliness of the axiom.

The fact that parallel lines do not intersect seems like it should follow from the definition of lines and angles. It doesn't seem like something we should have to specify in addition. That we must assume parallel lines do not intersect (rather than proving it) was long seen as a wart on geometry.

This wart irked mathematicians for millennia, until finally it was discovered that the fifth axiom is independent of the other four. You can build consistent systems where parallel lines intersect. You can build consistent systems where they diverge.

This seemed crazy, at the time: parallel straight lines cannot diverge! Surely, a geometry in which they do is absurd!

The problem is that mathematicians were imagining "straight lines" in their head that did not match the mathematical objects specified by the first four axioms of Euclid.

This mistake was invited by names which Euclid chose. "Straight lines" invoke a mental image that is more specific than that which the axioms describe. If you detach the provocative words from the axioms

1. You can make a `LUME` between any two `PTARS`
2. You can extend a `LUME` into a `SLUME`

and so on, then it's much easier to understand that the `LUME`s which Euclid's axioms describe may not match up with the image of a "straight line" in your head. It is much easier to understand that there may be interpretations of `LUME` which do not obey the fifth postulate.

In fact, if you take Euclid's first four postulates, there are many possible interpretations in which "straight line" takes on a multitude of meanings. This ability to disconnect the intended interpretation from the available interpretations is the bedrock of model theory. Model theory is the study of all interpretations of a theory, not just the ones that the original author intended.

Of course, model theory isn't really about finding surprising new interpretations — it's much more general than that. It's about exploring the breadth of interpretations that a given theory makes available. It's about discerning properties that hold in all possible interpretations of a theory. It's about discovering how well (or poorly) a given theory constrains its interpretations. It's a toolset used to discuss interpretations in general.

At its core, model theory is the study of what a mathematical theory actually says, when you strip the intent from the symbols.

## Iron walls

Before you can do model theory, you have to erect iron walls between four different concepts.

1. Logics
2. Languages
3. Theories
4. Models

### Logics

A logic is a formal system for building and manipulating sentences. Traditionally, this logic defines a number of symbols (`( ) ∧ ¬ ∀ ∃ ≡ ν '`, for example) and rules for building sentences from those symbols.

Note that you cannot generate sentences from a logic alone. Rather, you use a logic to generate sentences from a language.

Also, remember that the rules of a logic are syntactic, such as "if `φ` is a sentence then `(¬φ)` is a sentence".

Finally, remember that logics are just rules for generating sentences. A logic is perfectly happy to generate sentences shaped like `x∧(¬x)`, in spite of all your protests about contradictions.

### Languages

A language is a collection of symbols. From those symbols, using a logic, you can start generating sentences.

For example, in the propositional logic, using the language `{x, y}`, the string `hello` is surely not a sentence (for it fails to use the appropriate symbols). Nor is the string `¬xy` a sentence: it fails to follow the rules of the logic. `((¬x)∧y)` is a sentence, for it uses the appropriate symbols and follows the given rules.

Many results in model theory are achieved by holding the logic fixed and varying the language, so it's essential that these concepts be distinct in your mind.

### Theories

A theory is a collection of sentences written in one language. For example, in the language `{≤}` under first-order logic, we can discuss the theory

1. `(∀x)(x≤x)`
2. `(∀xy)(x≤y)∧(y≤x)→(y≡x)`
3. `(∀xyz)(x≤y)∧(y≤z)→(x≤z)`

which is the theory of order. (The axioms above are reflexivity, antisymmetry, and transitivity).

Remember that a theory is just a set of sentences drawn from all available sentences. These sentences aren't particularly special unless you make them special. Sentences like `(∃x)¬(x≤x)` are fine sentences built from the language `{≤}`, even though they directly contradict the theory. Theories don't affect the sentences of a language — they're just a grab-bag of some sentences that seemed interesting to someone.

### Models

A model is an interpretation of the sentences generated by a language. A model is a structure which assigns a truth value to each sentence generated by some language under some logic.

(More specifically, it's a structure that assigns binary values to sentences in such a way that we're justified in the name "truth value": for example, we require that a model says φ is true if and only if it says that ¬φ is false, and so on.)

Only once we start interpreting sentences is it meaningful to talk about valid or refutable sentences. Once you have a model of `{≤}` that happens to say that the axioms 1, 2, and 3 above are true, then you can start talking about how the theory of order rules out the sentence `(∃x)¬(x≤x)` — because there is no model of the theory of order which is also a model of this sentence.

(You can actually talk about how `(∃x)¬(x≤x)` is inconsistent with the theory of order without appealing to model theory, but I find it helpful to treat everything as raw symbols until interpreted by a model.)

To give a concrete example, in first order logic, using the language {S, +, *, 0}, the theory of arithmetic is the theory laid out by the [Peano axioms](http://en.wikipedia.org/wiki/Peano_axioms#First-order_theory_of_arithmetic). The actual natural numbers zero, one, two, ... are a model of this theory (where zero is the interpretation of 0, one is the interpretation of S0, etc.).

Also, it's worth noting that any object that interprets sentences and follows the rules of the logic qualifies as a model. There are often many non-isomorphic objects that interpret the same sentences in the same way. For example, rational numbers and real numbers are models of group theory that agree on every sentence in the language of groups, despite being different models.

Distinctions between these four points is something that seems obvious to me in hindsight, but I explicitly remember expending cognitive effort to separate these concepts mentally, so there you go. Make sure these distinctions are wrought in iron before attempting model theory.

## The Right to use a name

There's something about math education in general that has troubled me for quite some time, and which I'm finally able to articulate. It's quite possible that this is a personal nit, since nobody else seems to care — but I'll share it anyway.

Many math textbooks treat properties that justify a name of a thing as statements about the thing after naming it.

This is a little abstract, so I'll make a silly example. Imagine someone is trying to show that, in category theory, composition of arrows is associative. They shouldn't appeal to visual intuition or any diagrams of arrows.

The concept that following arrows is an associative operation is so ingrained in the concept of "arrow" that it's difficult to describe the property in English without sounding dumb.

If you move from A to B, then move B-to-D-through-C in one step, and if I follow the same paths but move A-to-C-through-B in one step and then from C to D, then we will end up at the same place.

This property of arrows is so stupidly obvious that the statement is frustrating. Further, it hides the following fact:

Associative composition between thingies is something we must have before we're justified in calling the thingies "Arrows".

Associative composition is what allows you to use the name "arrow" and draw visual diagrams. You can't appeal to my intuition about "arrows" to show that composition is associative. It's the other way around! Only after you show that your thingies have associative composition are you allowed to label them as "arrows".

As another example, the axioms of order (above) are what allow us to use the `≤` symbol, which appeals to our intuitive idea of order. Really, it's more honest to say "We have a binary relation `R`, satisfying

1. `(∀x)R(xx)`
2. `(∀xy)R(xy)∧R(yx)→(y≡x)`
3. `(∀xyz)R(xy)∧R(yz)→R(xz)`

which justifies our use of the `≤` symbol for `R`."

I imagine this is not a problem for experienced mathematicians, for whom it goes without saying that you must formally specify (or disregard) all intuitive baggage that comes attached to the names. However, I remember distinctly a number of times when I gnashed my teeth with boredom as teachers made obvious statements (of course `≤` is reflexive, why do we even need to say this?), simply because I didn't understand this idea.

I mention this because the first few sections of the Model Theory textbook make statements that seem quite obvious. It's easy to grind your teeth and say "duh, hurry up". It's a little harder to understand exactly why such things must be said. In that light, I think this is a good piece of advice for learning mathematics in general:

If you find yourself wondering why a statement must be said, check whether the statement is justifying any names.

Binding meaning

The early parts of Model Theory will go down much easier if you realize that they're binding logical symbols to the appropriate meaning (and thus justifying the name "model").

For example, when we state "M models `φ∧ψ` if and only if it models `φ` and it models `ψ`", it's easy to say "well duh". It's a little harder to understand that this is the mechanism by which the symbol `∧` is bound to the interpretation "and".

Also, note that the ability to distinguish between "the symbol `+` in the language L" from "the addition function as interpreted by the model M" is absolutely crucial.

## Totality

Something that kept on biting me was this: Models of first-order logic are "total". They have something to say about every sentence in a language. Even where a theory is incomplete, any individual model is "complete". A model of first-order logic interprets function symbols by total functions and relations by set-theoretic relations. The relationship `⊧` is total: for every sentence, either `M⊧φ` or `M⊧¬φ`.

This is a point where my intuitive notion of "models as interpretations" departed from the actual mathematical objects under consideration — functions are firmly partial-by-default in my mind's eye.

It's important to hold firm the distinction between "model" and "theory" here. Remember that the number theory is incomplete, while the standard model of number theory is the one that picks "true" for all Gödel sentences, has no infinite numbers, etc. (The difficulties in pinpointing such a model is exactly what the incompleteness theorem is all about.)

Be aware that the mathematical definition of a model may not match your intuitive idea of "a structure which interprets a theory", especially if you're coming from computer science (or other constructive fields).

None of this is particularly novel. Rather, this is a collection of distinctions and clarifications that would have made my life a bit easier when beginning the textbook.

In my case, I didn't have any of these concepts wrong, per se — rather, I had them fuzzy. The above distinctions were not yet fleshed out in my mind. This post provides a context for model theory; a taste of the type of thinking you must be ready to think.

I was originally going to use this as context for what I've learned in model theory so far, but this post took longer than expected. I'll follow up tomorrow.

## A Voting Puzzle, Some Political Science, and a Nerd Failure Mode

84 10 October 2013 02:10AM

In grade school, I read a series of books titled Sideways Stories from Wayside School by Louis Sachar, who you may know as the author of the novel Holes which was made into a movie in 2003. The series included two books of math problems, Sideways Arithmetic from Wayside School and More Sideways Arithmetic from Wayside School, the latter of which included the following problem (paraphrased):

The students have Mrs. Jewl's class have been given the privilege of voting on the height of the school's new flagpole. She has each of them write down what they think would be the best hight for the flagpole. The votes are distributed as follows:

• 1 student votes for 6 feet.
• 1 student votes for 10 feet.
• 7 students vote for 25 feet.
• 1 student votes for 30 feet.
• 2 students vote for 50 feet.
• 2 students vote for 60 feet.
• 1 student votes for 65 feet.
• 3 students vote for 75 feet.
• 1 student votes for 80 feet, 6 inches.
• 4 students vote for 85 feet.
• 1 student votes for 91 feet.
• 5 students vote for 100 feet.

At first, Mrs. Jewls declares 25 feet the winning answer, but one of the students who voted for 100 feet convinces her there should be a runoff between 25 feet and 100 feet. In the runoff, each student votes for the height closest to their original answer. But after that round of voting, one of the students who voted for 85 feet wants their turn, so 85 feet goes up against the winner of the previous round of voting, and the students vote the same way, with each student voting for the height closest to their original answer. Then the same thing happens again with the 50 foot option. And so on, with each number, again and again, "very much like a game of tether ball."

Question: if this process continues until it settles on an answer that can't be beaten by any other answer, how tall will the new flagpole be?

Answer (rot13'd): fvkgl-svir srrg, orpnhfr gung'f gur zrqvna inyhr bs gur bevtvany frg bs ibgrf. Naq abj lbh xabj gur fgbel bs zl svefg rapbhagre jvgu gur zrqvna ibgre gurberz.

Why am I telling you this? There's a minor reason and a major reason. The minor reason is that this shows it is possible to explain little-known academic concepts, at least certain ones, in a way that grade schoolers will understand. It's a data point that fits nicely with what Eliezer has written about how to explain things. The major reason, though, is that a month ago I finished my systematic read-through of the sequences and while I generally agree that they're awesome (perhaps moreso than most people; I didn't see the problem with the metaethics sequence), I thought the mini-discussion of political parties and voting was on reflection weak and indicative of a broader nerd failure mode.

TLDR (courtesy of lavalamp):

1. Politicians probably conform to the median voter's views.
2. Most voters are not the median, so most people usually dislike the winning politicians.
3. But people dislike the politicians for different reasons.
4. Nerds should avoid giving advice that boils down to "behave optimally". Instead, analyze the reasons for the current failure to behave optimally and give more targeted advice.

## Robust Cooperation in the Prisoner's Dilemma

66 07 June 2013 08:30AM

I'm proud to announce the preprint of Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic, a joint paper with Patrick LaVictoire (me), Mihaly Barasz, Paul Christiano, Benja Fallenstein, Marcello Herreshoff, and Eliezer Yudkowsky.

This paper was one of three projects to come out of the 2nd MIRI Workshop on Probability and Reflection in April 2013, and had its genesis in ideas about formalizations of decision theory that have appeared on LessWrong. (At the end of this post, I'll include links for further reading.)

Below, I'll briefly outline the problem we considered, the results we proved, and the (many) open questions that remain. Thanks in advance for your thoughts and suggestions!

## Background: Writing programs to play the PD with source code swap

(If you're not familiar with the Prisoner's Dilemma, see here.)

The paper concerns the following setup, which has come up in academic research on game theory: say that you have the chance to write a computer program X, which takes in one input and returns either Cooperate or Defect. This program will face off against some other computer program Y, but with a twist: X will receive the source code of Y as input, and Y will receive the source code of X as input. And you will be given your program's winnings, so you should think carefully about what sort of program you'd write!

Of course, you could simply write a program that defects regardless of its input; we call this program DefectBot, and call the program that cooperates on all inputs CooperateBot. But with the wealth of information afforded by the setup, you might wonder if there's some program that might be able to achieve mutual cooperation in situations where DefectBot achieves mutual defection, without thereby risking a sucker's payoff. (Douglas Hofstadter would call this a perfect opportunity for superrationality...)

## Previously known: CliqueBot and FairBot

And indeed, there's a way to do this that's been known since at least the 1980s. You can write a computer program that knows its own source code, compares it to the input, and returns C if and only if the two are identical (and D otherwise). Thus it achieves mutual cooperation in one important case where it intuitively ought to: when playing against itself! We call this program CliqueBot, since it cooperates only with the "clique" of agents identical to itself.

There's one particularly irksome issue with CliqueBot, and that's the fragility of its cooperation. If two people write functionally analogous but syntactically different versions of it, those programs will defect against one another! This problem can be patched somewhat, but not fully fixed. Moreover, mutual cooperation might be the best strategy against some agents that are not even functionally identical, and extending this approach requires you to explicitly delineate the list of programs that you're willing to cooperate with. Is there a more flexible and robust kind of program you could write instead?

As it turns out, there is: in a 2010 post on LessWrong, cousin_it introduced an algorithm that we now call FairBot. Given the source code of Y, FairBot searches for a proof (of less than some large fixed length) that Y returns C when given the source code of FairBot, and then returns C if and only if it discovers such a proof (otherwise it returns D). Clearly, if our proof system is consistent, FairBot only cooperates when that cooperation will be mutual. But the really fascinating thing is what happens when you play two versions of FairBot against each other. Intuitively, it seems that either mutual cooperation or mutual defection would be stable outcomes, but it turns out that if their limits on proof lengths are sufficiently high, they will achieve mutual cooperation!

The proof that they mutually cooperate follows from a bounded version of Löb's Theorem from mathematical logic. (If you're not familiar with this result, you might enjoy Eliezer's Cartoon Guide to Löb's Theorem, which is a correct formal proof written in much more intuitive notation.) Essentially, the asymmetry comes from the fact that both programs are searching for the same outcome, so that a short proof that one of them cooperates leads to a short proof that the other cooperates, and vice versa. (The opposite is not true, because the formal system can't know it won't find a contradiction. This is a subtle but essential feature of mathematical logic!)

## Generalization: Modal Agents

Unfortunately, FairBot isn't what I'd consider an ideal program to write: it happily cooperates with CooperateBot, when it could do better by defecting. This is problematic because in real life, the world isn't separated into agents and non-agents, and any natural phenomenon that doesn't predict your actions can be thought of as a CooperateBot (or a DefectBot). You don't want your agent to be making concessions to rocks that happened not to fall on them. (There's an important caveat: some things have utility functions that you care about, but don't have sufficient ability to predicate their actions on yours. In that case, though, it wouldn't be a true Prisoner's Dilemma if your values actually prefer the outcome (C,C) to (D,C).)

However, FairBot belongs to a promising class of algorithms: those that decide on their action by looking for short proofs of logical statements that concern their opponent's actions. In fact, there's a really convenient mathematical structure that's analogous to the class of such algorithms: the modal logic of provability (known as GL, for Gödel-Löb).

So that's the subject of this preprint: what can we achieve in decision theory by considering agents defined by formulas of provability logic?

## Tiling Agents for Self-Modifying AI (OPFAI #2)

53 06 June 2013 08:24PM

An early draft of publication #2 in the Open Problems in Friendly AI series is now available:  Tiling Agents for Self-Modifying AI, and the Lobian Obstacle.  ~20,000 words, aimed at mathematicians or the highly mathematically literate.  The research reported on was conducted by Yudkowsky and Herreshoff, substantially refined at the November 2012 MIRI Workshop with Mihaly Barasz and Paul Christiano, and refined further at the April 2013 MIRI Workshop.

Abstract:

We model self-modication in AI by introducing 'tiling' agents whose decision systems will approve the construction of highly similar agents, creating a repeating pattern (including similarity of the offspring's goals).  Constructing a formalism in the most straightforward way produces a Godelian difficulty, the Lobian obstacle.  By technical methods we demonstrate the possibility of avoiding this obstacle, but the underlying puzzles of rational coherence are thus only partially addressed.  We extend the formalism to partially unknown deterministic environments, and show a very crude extension to probabilistic environments and expected utility; but the problem of finding a fundamental decision criterion for self-modifying probabilistic agents remains open.

Commenting here is the preferred venue for discussion of the paper.  This is an early draft and has not been reviewed, so it may contain mathematical errors, and reporting of these will be much appreciated.

The overall agenda of the paper is introduce the conceptual notion of a self-reproducing decision pattern which includes reproduction of the goal or utility function, by exposing a particular possible problem with a tiling logical decision pattern and coming up with some partial technical solutions.  This then makes it conceptually much clearer to point out the even deeper problems with "We can't yet describe a probabilistic way to do this because of non-monotonicity" and "We don't have a good bounded way to do this because maximization is impossible, satisficing is too weak and Schmidhuber's swapping criterion is underspecified."  The paper uses first-order logic (FOL) because FOL has a lot of useful standard machinery for reflection which we can then invoke; in real life, FOL is of course a poor representational fit to most real-world environments outside a human-constructed computer chip with thermodynamically expensive crisp variable states.

As further background, the idea that something-like-proof might be relevant to Friendly AI is not about achieving some chimera of absolute safety-feeling, but rather about the idea that the total probability of catastrophic failure should not have a significant conditionally independent component on each self-modification, and that self-modification will (at least in initial stages) take place within the highly deterministic environment of a computer chip.  This means that statistical testing methods (e.g. an evolutionary algorithm's evaluation of average fitness on a set of test problems) are not suitable for self-modifications which can potentially induce catastrophic failure (e.g. of parts of code that can affect the representation or interpretation of the goals).  Mathematical proofs have the property that they are as strong as their axioms and have no significant conditionally independent per-step failure probability if their axioms are semantically true, which suggests that something like mathematical reasoning may be appropriate for certain particular types of self-modification during some developmental stages.

Thus the content of the paper is very far off from how a realistic AI would work, but conversely, if you can't even answer the kinds of simple problems posed within the paper (both those we partially solve and those we only pose) then you must be very far off from being able to build a stable self-modifying AI.  Being able to say how to build a theoretical device that would play perfect chess given infinite computing power, is very far off from the ability to build Deep Blue.  However, if you can't even say how to play perfect chess given infinite computing power, you are confused about the rules of the chess or the structure of chess-playing computation in a way that would make it entirely hopeless for you to figure out how to build a bounded chess-player.  Thus "In real life we're always bounded" is no excuse for not being able to solve the much simpler unbounded form of the problem, and being able to describe the infinite chess-player would be substantial and useful conceptual progress compared to not being able to do that.  We can't be absolutely certain that an analogous situation holds between solving the challenges posed in the paper, and realistic self-modifying AIs with stable goal systems, but every line of investigation has to start somewhere.

Parts of the paper will be easier to understand if you've read Highly Advanced Epistemology 101 For Beginners including the parts on correspondence theories of truth (relevant to section 6) and model-theoretic semantics of logic (relevant to 3, 4, and 6), and there are footnotes intended to make the paper somewhat more accessible than usual, but the paper is still essentially aimed at mathematically sophisticated readers.

## Reflection in Probabilistic Logic

62 24 March 2013 04:37PM

Paul Christiano has devised a new fundamental approach to the "Löb Problem" wherein Löb's Theorem seems to pose an obstacle to AIs building successor AIs, or adopting successor versions of their own code, that trust the same amount of mathematics as the original.  (I am currently writing up a more thorough description of the question this preliminary technical report is working on answering.  For now the main online description is in a quick Summit talk I gave.  See also Benja Fallenstein's description of the problem in the course of presenting a different angle of attack.  Roughly the problem is that mathematical systems can only prove the soundness of, aka 'trust', weaker mathematical systems.  If you try to write out an exact description of how AIs would build their successors or successor versions of their code in the most obvious way, it looks like the mathematical strength of the proof system would tend to be stepped down each time, which is undesirable.)

Paul Christiano's approach is inspired by the idea that whereof one cannot prove or disprove, thereof one must assign probabilities: and that although no mathematical system can contain its own truth predicate, a mathematical system might be able to contain a reflectively consistent probability predicate.  In particular, it looks like we can have:

∀a, b: (a < P(φ) < b)          ⇒  P(a < P('φ') < b) = 1
∀a, b: P(a ≤ P('φ') ≤ b) > 0  ⇒  a ≤ P(φ) ≤ b

Suppose I present you with the human and probabilistic version of a Gödel sentence, the Whitely sentence "You assign this statement a probability less than 30%."  If you disbelieve this statement, it is true.  If you believe it, it is false.  If you assign 30% probability to it, it is false.  If you assign 29% probability to it, it is true.

Paul's approach resolves this problem by restricting your belief about your own probability assignment to within epsilon of 30% for any epsilon.  So Paul's approach replies, "Well, I assign almost exactly 30% probability to that statement - maybe a little more, maybe a little less - in fact I think there's about a 30% chance that I'm a tiny bit under 0.3 probability and a 70% chance that I'm a tiny bit over 0.3 probability."  A standard fixed-point theorem then implies that a consistent assignment like this should exist.  If asked if the probability is over 0.2999 or under 0.30001 you will reply with a definite yes.

## Second-Order Logic: The Controversy

22 04 January 2013 07:51PM

Followup to: Godel's Completeness and Incompleteness Theorems

"So the question you asked me last time was, 'Why does anyone bother with first-order logic at all, if second-order logic is so much more powerful?'"

Right. If first-order logic can't talk about finiteness, or distinguish the size of the integers from the size of the reals, why even bother?

"The first thing to realize is that first-order theories can still have a lot of power. First-order arithmetic does narrow down the possible models by a lot, even if it doesn't narrow them down to a single model. You can prove things like the existence of an infinite number of primes, because every model of the first-order axioms has an infinite number of primes. First-order arithmetic is never going to prove anything that's wrong about the standard numbers. Anything that's true in all models of first-order arithmetic will also be true in the particular model we call the standard numbers."

Even so, if first-order theory is strictly weaker, why bother? Unless second-order logic is just as incomplete relative to third-order logic, which is weaker than fourth-order logic, which is weaker than omega-order logic -

"No, surprisingly enough - there's tricks for making second-order logic encode any proposition in third-order logic and so on. If there's a collection of third-order axioms that characterizes a model, there's a collection of second-order axioms that characterizes the same model. Once you make the jump to second-order logic, you're done - so far as anyone knows (so far as I know) there's nothing more powerful than second-order logic in terms of which models it can characterize."

Then if there's one spoon which can eat anything, why not just use the spoon?

"Well... this gets into complex issues. There are mathematicians who don't believe there is a spoon when it comes to second-order logic."

Like there are mathematicians who don't believe in infinity?

"Kind of. Look, suppose you couldn't use second-order logic - you belonged to a species that doesn't have second-order logic, or anything like it. Your species doesn't have any native mental intuition you could use to construct the notion of 'all properties'. And then suppose that, after somebody used first-order set theory to prove that first-order arithmetic had many possible models, you stood around shouting that you believed in only one model, what you called the standard model, but you couldn't explain what made this model different from any other model -"

Well... a lot of times, even in math, we make statements that genuinely mean something, but take a while to figure out how to define. I think somebody who talked about 'the numbers' would mean something even before second-order logic was invented.

"But here the hypothesis is that you belong to a species that can't invent second-order logic, or think in second-order logic, or anything like it."

Then I suppose you want me to draw the conclusion that this hypothetical alien is just standing there shouting about standardness, but its words don't mean anything because they have no way to pin down one model as opposed to another one. And I expect this species is also magically forbidden from talking about all possible subsets of a set?

"Yeah. They can't talk about the largest powerset, just like they can't talk about the smallest model of Peano arithmetic."

Then you could arguably deny that shouting about the 'standard' numbers would mean anything, to the members of this particular species. You might as well shout about the 'fleem' numbers, I guess.

"Right. Even if all the members of this species did have a built-in sense that there was a special model of first-order arithmetic that was fleemer than any other model, if that fleem-ness wasn't bound to anything else, it would be meaningless. Just a floating word. Or if all you could do was define fleemness as floobness and floobness as fleemness, you'd have a loop of floating words; and that might give you the impression that each particular word had a meaning, but the loop as a whole wouldn't be connected to reality. That's why it doesn't help to say that the standard model of numbers is the smallest among all possible models of Peano arithmetic, if you can't define 'smallest possible' any more than you can define 'connected chain' or 'finite number of predecessors'."

But second-order logic does seem to have consequences first-order logic doesn't. Like, what about all that Godelian stuff? Doesn't second-order arithmetic semantically imply... its own Godel statement? Because the unique model of second-order arithmetic doesn't contain any number encoding a proof of a contradiction from second-order arithmetic? Wait, now I'm confused.

"No, that's correct. It's not paradoxical, because there's no effective way of finding all the semantic implications of a collection of second-order axioms. There's no analogue of Godel's Completeness Theorem for second-order logic - no syntactic system for deriving all the semantic consequences. Second-order logic is sound, in the sense that anything syntactically provable from a set of premises, is true in any model obeying those premises. But second-order logic isn't complete; there are semantic consequences you can't derive. If you take second-order logic at face value, there's no effectively computable way of deriving all the consequences of what you say you 'believe'... which is a major reason some mathematicians are suspicious of second-order logic. What does it mean to believe something whose consequences you can't derive?"

But second-order logic clearly has some experiential consequences first-order logic doesn't. Suppose I build a Turing machine that looks for proofs of a contradiction from first-order Peano arithmetic. If PA's consistency isn't provable in PA, then by the Completeness Theorem there must exist nonstandard models of PA where this machine halts after finding a proof of a contradiction. So first-order logic doesn't tell me that this machine runs forever - maybe it has nonstandard halting times, i.e., it runs at all standard N, but halts at -2* somewhere along a disconnected chain. Only second-order logic tells me there's no proof of PA's inconsistency and therefore this machine runs forever. Only second-order logic tells me I should expect to see this machine keep running, and not expect - note falsifiability - that the machine ever halts.

"Sure, you just used a second-order theory to derive a consequence you didn't get from a first-order theory. But that's not the same as saying that you can only get that consequence using second-order logic. Maybe another first-order theory would give you the same prediction."

Like what?

"Well, for one thing, first-order set theory can prove that first-order arithmetic has a model. Zermelo-Fraenkel set theory can prove the existence of a set such that all the first-order Peano axioms are true about that set. It follows within ZF that sound reasoning on first-order arithmetic will never prove a contradiction. And since ZF can prove that the syntax of classical logic is sound -"

What does it mean for set theory to prove that logic is sound!?

"ZF can quote formulas as structured, and encode models as sets, and then represent a finite ZF-formula which says whether or not a set of quoted formulas is true about a model. ZF can then prove that no step of classical logic goes from premises that are true inside a set-model, to premises that are false inside a set-model. In other words, ZF can represent the idea 'formula X is semantically true in model Y' and 'these syntactic rules never produce semantically false statements from semantically true statements'."

Wait, then why can't ZF prove itself consistent? If ZF believes in all the axioms of ZF, and it believes that logic never produces false statements from true statements -

"Ah, but ZF can't prove that there exists any set which is a model of ZF, so it can't prove the ZF-axioms are consistent. ZF shouldn't be able to prove that some set is a model of ZF, because that's not true in all models. Many models of ZF don't contain any individual set well-populated enough for that one set to be a model of ZF all by itself."

I'm kind of surprised in a Godelian sense that ZF can contain sets as large as the universe of ZF. Doesn't any given set have to be smaller than the whole universe?

"Inside any particular model of ZF, every set within that model is smaller than that model. But not all models of ZF are the same size; in fact, models of ZF of every size exist, by the Lowenheim-Skolem theorem. So you can have some models of ZF - some universes in which all the elements collectively obey the ZF-relations - containing individual sets which are larger than other entire models of ZF. A set that large is called a Grothendieck universe and assuming it exists is equivalent to assuming the existence of 'strongly inaccessible cardinals', sizes so large that you provably can't prove inside set theory that anything that large exists."

Whoa.

(Pause.)

But...

"But?"

I agree you've shown that one experiential consequence of second-order arithmetic - namely that a machine looking for proofs of inconsistency from PA, won't be seen to halt - can be derived from first-order set theory. Can you get all the consequences of second-order arithmetic in some particular first-order theory?

"You can't get all the semantic consequences of second-order logic, taken at face value, in any theory or any computable reasoning. What about the halting problem? Taken at face value, it's a semantic consequence of second-order logic that any given Turing machine either halts or doesn't halt -"

Personally I find it rather intuitive to imagine that a Turing machine either halts or doesn't halt. I mean, if I'm walking up to a machine and watching it run, telling me that its halting or not-halting 'isn't entailed by my axioms' strikes me as not describing any actual experience I can have with the machine. Either I'll see it halt eventually, or I'll see it keep running forever.

"My point is that the statements we can derive from the syntax of current second-order logic is limited by that syntax. And by the halting problem, we shouldn't ever expect a computable syntax that gives us all the semantic consequences.  There's no possible theory you can actually use to get a correct advance prediction about whether an arbitrary Turing machine halts."

Okay. I agree that no computable reasoning, on second-order logic or anything else, should be able to solve the halting problem. Unless time travel is possible, but even then, you shouldn't be able to solve the expanded halting problem for machines that use time travel.

"Right, so the syntax of second-order logic can't prove everything. And in fact, it turns out that, in terms of what you can prove syntactically using the standard syntax, second-order logic is identical to a many-sorted first-order logic."

Huh?

"Suppose you have a first-order logic - one that doesn't claim to be able to quantify over all possible predicates - which does allow the universe to contain two different sorts of things. Say, the logic uses lower-case letters for all type-1 objects and upper-case letters for all type-2 objects. Like, '∀x: x = x' is a statement over all type-1 objects, and '∀Y: Y = Y' is a statement over all type-2 objects. But aside from that, you use the same syntax and proof rules as before."

Okay...

"Now add an element-relation x∈Y, saying that x is an element of Y, and add some first-order axioms for making the type-2 objects behave like collections of type-1 objects, including axioms for making sure that most describable type-2 collections exist - i.e., the collection X containing just x is guaranteed to exist, and so on. What you can prove syntactically in this theory will be identical to what you can prove using the standard syntax of second-order logic - even though the theory doesn't claim that all possible collections of type-1s are type-2s, and the theory will have models where many 'possible' collections are missing from the type-2s."

Wait, now you're saying that second-order logic is no more powerful than first-order logic?

"I'm saying that the supposed power of second-order logic derives from interpreting it a particular way, and taking on faith that when you quantify over all properties, you're actually talking about all properties."

But then second-order arithmetic is no more powerful than first-order arithmetic in terms of what it can actually prove?

"2nd-order arithmetic is way more powerful than first-order arithmetic. But that's because first-order set theory is more powerful than arithmetic, and adding the syntax of second-order logic corresponds to adding axioms with set-theoretic properties. In terms of which consequences can be syntactically proven, second-order arithmetic is more powerful than first-order arithmetic, but weaker than first-order set theory. First-order set theory can prove the existence of a model of second-order arithmetic - ZF can prove there's a collection of numbers and sets of numbers which models a many-sorted logic with syntax corresponding to second-order logic - and so ZF can prove second-order arithmetic consistent."

But first-order logic, including first-order set theory, can't even talk about the standard numbers!

"Right, but first-order set theory can syntactically prove more statements about 'numbers' than second-order arithmetic can prove. And when you combine that with the semantic implications of second-order arithmetic not being computable, and with any second-order logic being syntactically identical to a many-sorted first-order logic, and first-order logic having neat properties like the Completeness Theorem... well, you can see why some mathematicians would want to give up entirely on this whole second-order business."

But if you deny second-order logic you can't even say the word 'finite'. You would have to believe the word 'finite' was a meaningless noise.

"You'd define finiteness relative to whatever first-order model you were working in. Like, a set might be 'finite' only on account of the model not containing any one-to-one mapping from that set onto a smaller subset of itself -"

But that set wouldn't actually be finite. There wouldn't actually be, like, only a billion objects in there. It's just that all the mappings which could prove the set was infinite would be mysteriously missing.

"According to some other model, maybe. But since there is no one true model -"

How is this not crazy talk along the lines of 'there is no one true reality'? Are you saying there's no really smallest set of numbers closed under succession, without all the extra infinite chains? Doesn't talking about how these theories have multiple possible models, imply that those possible models are logical thingies and one of them actually does contain the largest powerset and the smallest integers?

"The mathematicians who deny second-order logic would see that reasoning as invoking an implicit background universe of set theory. Everything you're saying makes sense relative to some particular model of set theory, which would contain possible models of Peano arithmetic as sets, and could look over those sets and pick out the smallest in that model. Similarly, that set theory could look over a proposed model for a many-sorted logic, and say whether there were any subsets within the larger universe which were missing from the many-sorted model. Basically, your brain is insisting that it lives inside some particular model of set theory. And then, from that standpoint, you could look over some other set theory and see how it was missing subsets that your theory had."

Argh! No, damn it, I live in the set theory that really does have all the subsets, with no mysteriously missing subsets or mysterious extra numbers, or denumerable collections of all possible reals that could like totally map onto the integers if the mapping that did it hadn't gone missing in the Australian outback -

"But everybody says that."

Okay...

"Yeah?"

Screw set theory. I live in the physical universe where when you run a Turing machine, and keep watching forever in the physical universe, you never experience a time where that Turing machine outputs a proof of the inconsistency of Peano Arithmetic. Furthermore, I live in a universe where space is actually composed of a real field and space is actually infinitely divisible and contains all the points between A and B, rather than space only containing a denumerable number of points whose existence can be proven from the first-order axiomatization of the real numbers. So to talk about physics - forget about mathematics - I've got to use second-order logic.

"Ah. You know, that particular response is not one I have seen in the previous literature."

Yes, well, I'm not a pure mathematician. When I ask whether I want an Artificial Intelligence to think in second-order logic or first-order logic, I wonder how that affects what the AI does in the actual physical universe. Here in the actual physical universe where times are followed by successor times, I strongly suspect that we should only expect to experience standard times, and not experience any nonstandard times. I think time is connected, and global connectedness is a property I can only talk about using second-order logic. I think that every particular time is finite, and yet time has no upper bound - that there are all finite times, but only finite times - and that's a property I can only characterize using second-order logic.

"But if you can't ever tell the difference between standard and nonstandard times? I mean, local properties of time can be described using first-order logic, and you can't directly see global properties like 'connectedness' -"

But I can tell the difference. There are only nonstandard times where a proof-checking machine, running forever, outputs a proof of inconsistency from the Peano axioms. So I don't expect to experience seeing a machine do that, since I expect to experience only standard times.

"Set theory can also prove PA consistent. If you use set theory to define time, you similarly won't expect to see a time where PA is proven inconsistent - those nonstandard integers don't exist in any model of ZF."

Why should I anticipate that my physical universe is restricted to having only the nonstandard times allowed by a more powerful set theory, instead of nonstandard times allowed by first-order arithmetic? If I then talk about a nonstandard time where a proof-enumerating machine proves ZF inconsistent, will you say that only nonstandard times allowed by some still more powerful theory can exist? I think it's clear that the way you're deciding which experimental outcomes you'll have to excuse, is by secretly assuming that only standard times exist regardless of which theory is required to narrow it down.

"Ah... hm. Doesn't physics say this universe is going to run out of negentropy before you can do an infinite amount of computation? Maybe there's only a bounded amount of time, like it stops before googolplex or something. That can be characterized by first-order theories."

We don't know that for certain, and I wouldn't want to build an AI that just assumed lifespans had to be finite, in case it was wrong. Besides, should I use a different logic than if I'd found myself in Conway's Game of Life, or something else really infinite? Wouldn't the same sort of creatures evolve in that universe, having the same sort of math debates?

"Perhaps no universe like that can exist; perhaps only finite universes can exist, because only finite universes can be uniquely characterized by first-order logic."

You just used the word 'finite'! Furthermore, taken at face value, our own universe doesn't look like it has a finite collection of entities related by first-order logical rules. Space and time both look like infinite collections of points - continuous collections, which is a second-order concept - and then to characterize the size of that infinity we'd need second-order logic. I mean, by the Lowenheim-Skolem theorem, there aren't just denumerable models of first-order axiomatizations of the reals, there's also unimaginably large cardinal infinities which obey the same premises, and that's a possibility straight out of H. P. Lovecraft. Especially if there are any things hiding in the invisible cracks of space."

"How could you tell if there were inaccessible cardinal quantities of points hidden inside a straight line? And anything that locally looks continuous each time you try to split it at a describable point, can be axiomatized by a first-order schema for continuity."

That brings up another point: Who'd really believe that the reason Peano arithmetic works on physical times, is because that whole infinite axiom schema of induction, containing for every Φ a separate rule saying...

(Φ(0) ∧ (∀x: Φ(x) → Φ(Sx))) → (∀n: Φ(n))

...was used to specify our universe? How improbable would it be for an infinitely long list of rules to be true, if there wasn't a unified reason for all of them? It seems much more likely that the real reason first-order PA works to describe time, is that all properties which are true at a starting time and true of the successor of any time where they're true, are true of all later times; and this generalization over properties makes induction hold for first-order formulas as a special case. If my native thought process is first-order logic, I wouldn't see the connection between each individual formula in the axiom schema - it would take separate evidence to convince me of each one - they would feel like independent mathematical facts. But after doing scientific induction over the fact that many properties true at zero, with succession preserving truth, seem to be true everywhere - after generalizing the simple, compact second-order theory of numbers and times - then you could invent an infinite first-order theory to approximate it.

"Maybe that just says you need to adjust whatever theory of scientific induction you're using, so that it can more easily induct infinite axiom schemas."

But why the heck would you need to induct infinite axiom schemas in the first place, if Reality natively ran on first-order logic? Isn't it far more likely that the way we ended up with these infinite lists of axioms was that Reality was manufactured - forgive the anthropomorphism - that Reality was manufactured using an underlying schema in which time is a connected series of events, and space is a continuous field, and these are properties which happen to require second-order logic for humans to describe? I mean, if you picked out first-order theories at random, what's the chance we'd end up inside an infinitely long axiom schema that just happened to look like the projection of a compact second-order theory? Aren't we ignoring a sort of hint?

"A hint to what?"

Well, I'm not that sure myself, at this depth of philosophy. But I would currently say that finding ourselves in a physical universe where times have successor times, and space looks continuous, seems like a possible hint that the Tegmark Level IV multiverse - or the way Reality was manufactured, or whatever - might look more like causal universes characterizable by compact second-order theories than causal universes characterizable by first-order theories.

"But since any second-order theory can just as easily be interpreted as a many-sorted first-order theory with quantifiers that can range over either elements or sets of elements, how could using second-order syntax actually improve an Artificial Intelligence's ability to handle a reality like that?"

Good question. One obvious answer is that the AI would be able to induct what you would call an infinite axiom schema, as a single axiom - a simple, finite hypothesis.

"There's all sorts of obvious hacks to scientific induction of first-order axioms which would let you assign nonzero probability to computable infinite sequences of axioms -"

Sure. So beyond that... I would currently guess that the basic assumption behind 'behaving as if' second-order logic is true, says that the AI should act as if only the 'actually smallest' numbers will ever appear in physics, relative to some 'true' mathematical universe that it thinks it lives in, but knows it can't fully characterize. Which is roughly what I'd say human mathematicians do when they take second-order logic at face value; they assume that there's some true mathematical universe in the background, and that second-order logic lets them talk about it.

"And what behaviorally, experimentally distinguishes the hypothesis, 'I live in the true ultimate math with fully populated powersets' from the hypothesis, 'There's some random model of first-order set-theory axioms I happen to be living in'?"

Well... one behavioral consequence is suspecting that your time obeys an infinitely long list of first-order axioms with induction schemas for every formula. And then moreover believing that you'll never experience a time when a proof-checking machine outputs a proof that Zermelo-Fraenkel set theory is inconsistent - even though there's provably some models with times like that, which fit the axiom schema you just inducted. That sounds like secretly believing that there's a background 'true' set of numbers that you think characterizes physical time, and that it's the smallest such set. Another suspicious behavior is that as soon as you suspect Zermelo-Fraenkel set theory is consistent, you suddenly expect not to experience any physical time which ZF proves isn't a standard number. You don't think you're in the nonstandard time of some weaker theory like Peano arithmetic. You think you're in the minimal time expressible by any and all theories, so as soon as ZF can prove some number doesn't exist in the minimal set, you think that 'real time' lacks such a number. All of these sound like behaviors you'd carry out if you thought there was a single 'true' mathematical universe that provided the best model for describing all physical phenomena, like time and space, which you encounter - and believing that this 'true' backdrop used the largest powersets and smallest numbers.

"How exactly do you formalize all that reasoning, there? I mean, how would you actually make an AI reason that way?"

Er... I'm still working on that part.

"That makes your theory a bit hard to criticize, don't you think? Personally, I wouldn't be surprised if any such formalized reasoning looked just like believing that you live inside a first-order set theory."

I suppose I wouldn't be too surprised either - it's hard to argue with the results on many-sorted logics. But if comprehending the physical universe is best done by assuming that real phenomena are characterized by a 'true' mathematics containing the powersets and the natural numbers - and thus expecting that no mathematical model we can formulate will ever contain any larger powersets or smaller numbers than those of the 'true' backdrop to physics - then I'd call that a moral victory for second-order logic. In first-order logic we aren't even supposed to be able to talk about such things.

"Really? To me that sounds like believing you live inside a model of first-order set theory, and believing that all models of any theories you can invent must also be sets in the larger model. You can prove the Completeness Theorem inside ZF plus the Axiom of Choice, so ZFC already proves that all consistent theories have models which are sets, although of course it can't prove that ZFC itself is such a theory. So - anthropomorphically speaking - no model of ZFC expects to encounter a theory that has fewer numbers or larger powersets than itself. No model of ZFC expects to encounter any quoted-model, any set that a quoted theory entails, which contains larger powersets than the ones in its own Powerset Axiom. A first-order set theory can even make the leap from the finite statement, 'P is true of all my subsets of X', to believing, 'P is true of all my subsets of X that can be described by this denumerable collection of formulas' - it can encompass the jump from a single axiom over 'all my subsets', to a quoted axiom schema over formulas. I'd sum all that up by saying, 'second-order logic is how first-order set theory feels from the inside'."

Maybe. Even in the event that neither human nor superintelligent cognition will ever be able to 'properly talk about' unbounded finite times, global connectedness, particular infinite cardinalities, or true spatial continuity, it doesn't follow that Reality is similarly limited in which physics it can privilege.

Part of the sequence Highly Advanced Epistemology 101 for Beginners

Previous post: "Godel's Completeness and Incompleteness Theorems"

## Godel's Completeness and Incompleteness Theorems

30 25 December 2012 01:16AM

Followup to: Standard and Nonstandard Numbers

So... last time you claimed that using first-order axioms to rule out the existence of nonstandard numbers - other chains of numbers besides the 'standard' numbers starting at 0 - was forever and truly impossible, even unto a superintelligence, no matter how clever the first-order logic used, even if you came up with an entirely different way of axiomatizing the numbers.

"Right."

How could you, in your finiteness, possibly know that?

"Have you heard of Godel's Incompleteness Theorem?"

Of course! Godel's Theorem says that for every consistent mathematical system, there are statements which are true within that system, which can't be proven within the system itself. Godel came up with a way to encode theorems and proofs as numbers, and wrote a purely numerical formula to detect whether a proof obeyed proper logical syntax. The basic trick was to use prime factorization to encode lists; for example, the ordered list <3, 7, 1, 4> could be uniquely encoded as:

23 * 37 * 51 * 74

And since prime factorizations are unique, and prime powers don't mix, you could inspect this single number, 210,039,480, and get the unique ordered list <3, 7, 1, 4> back out. From there, going to an encoding for logical formulas was easy; for example, you could use the 2 prefix for NOT and the 3 prefix for AND and get, for any formulas Φ and Ψ encoded by the numbers #Φ and #Ψ:

¬Φ = 22 * 3

Φ ∧ Ψ = 23 * 3 * 5

It was then possible, by dint of crazy amounts of work, for Godel to come up with a gigantic formula of Peano Arithmetic [](p, c) meaning, 'P encodes a valid logical proof using first-order Peano axioms of C', from which directly followed the formula []c, meaning, 'There exists a number P such that P encodes a proof of C' or just 'C is provable in Peano arithmetic.'

Godel then put in some further clever work to invent statements which referred to themselves, by having them contain sub-recipes that would reproduce the entire statement when manipulated by another formula.

And then Godel's Statement encodes the statement, 'There does not exist any number P such that P encodes a proof of (this statement) in Peano arithmetic' or in simpler terms 'I am not provable in Peano arithmetic'. If we assume first-order arithmetic is consistent and sound, then no proof of this statement within first-order arithmetic exists, which means the statement is true but can't be proven within the system. That's Godel's Theorem.

"Er... no."

No?

"No. I've heard rumors that Godel's Incompleteness Theorem is horribly misunderstood in your Everett branch. Have you heard of Godel's Completeness Theorem?"

Is that a thing?

"Yes! Godel's Completeness Theorem says that, for any collection of first-order statements, every semantic implication of those statements is syntactically provable within first-order logic. If something is a genuine implication of a collection of first-order statements - if it actually does follow, in the models pinned down by those statements - then you can prove it, within first-order logic, using only the syntactical rules of proof, from those axioms."

## Standard and Nonstandard Numbers

28 20 December 2012 03:23AM

Followup toLogical Pinpointing

"Oh! Hello. Back again?"

Yes, I've got another question. Earlier you said that you had to use second-order logic to define the numbers. But I'm pretty sure I've heard about something called 'first-order Peano arithmetic' which is also supposed to define the natural numbers. Going by the name, I doubt it has any 'second-order' axioms. Honestly, I'm not sure I understand this second-order business at all.

"Well, let's start by examining the following model:"

"This model has three properties that we would expect to be true of the standard numbers - 'Every number has a successor', 'If two numbers have the same successor they are the same number', and '0 is the only number which is not the successor of any number'.  All three of these statements are true in this model, so in that sense it's quite numberlike -"

And yet this model clearly is not the numbers we are looking for, because it's got all these mysterious extra numbers like C and -2*.  That C thing even loops around, which I certainly wouldn't expect any number to do.  And then there's that infinite-in-both-directions chain which isn't corrected to anything else.

"Right, so, the difference between first-order logic and second-order logic is this:  In first-order logic, we can get rid of the ABC - make a statement which rules out any model that has a loop of numbers like that.  But we can't get rid of the infinite chain underneath it.  In second-order logic we can get rid of the extra chain."

## Logical Pinpointing

59 02 November 2012 03:33PM

Followup to: Causal Reference, Proofs, Implications and Models

The fact that one apple added to one apple invariably gives two apples helps in the teaching of arithmetic, but has no bearing on the truth of the proposition that 1 + 1 = 2.

-- James R. Newman, The World of Mathematics

Previous meditation 1: If we can only meaningfully talk about parts of the universe that can be pinned down by chains of cause and effect, where do we find the fact that 2 + 2 = 4? Or did I just make a meaningless noise, there? Or if you claim that "2 + 2 = 4"isn't meaningful or true, then what alternate property does the sentence "2 + 2 = 4" have which makes it so much more useful than the sentence "2 + 2 = 3"?

Previous meditation 2: It has been claimed that logic and mathematics is the study of which conclusions follow from which premises. But when we say that 2 + 2 = 4, are we really just assuming that? It seems like 2 + 2 = 4 was true well before anyone was around to assume it, that two apples equalled two apples before there was anyone to count them, and that we couldn't make it 5 just by assuming differently.

Speaking conventional English, we'd say the sentence 2 + 2 = 4 is "true", and anyone who put down "false" instead on a math-test would be marked wrong by the schoolteacher (and not without justice).

But what can make such a belief true, what is the belief about, what is the truth-condition of the belief which can make it true or alternatively false? The sentence '2 + 2 = 4' is true if and only if... what?

In the previous post I asserted that the study of logic is the study of which conclusions follow from which premises; and that although this sort of inevitable implication is sometimes called "true", it could more specifically be called "valid", since checking for inevitability seems quite different from comparing a belief to our own universe. And you could claim, accordingly, that "2 + 2 = 4" is 'valid' because it is an inevitable implication of the axioms of Peano Arithmetic.

And yet thinking about 2 + 2 = 4 doesn't really feel that way. Figuring out facts about the natural numbers doesn't feel like the operation of making up assumptions and then deducing conclusions from them. It feels like the numbers are just out there, and the only point of making up the axioms of Peano Arithmetic was to allow mathematicians to talk about them. The Peano axioms might have been convenient for deducing a set of theorems like 2 + 2 = 4, but really all of those theorems were true about numbers to begin with. Just like "The sky is blue" is true about the sky, regardless of whether it follows from any particular assumptions.

So comparison-to-a-standard does seem to be at work, just as with physical truth... and yet this notion of 2 + 2 = 4 seems different from "stuff that makes stuff happen". Numbers don't occupy space or time, they don't arrive in any order of cause and effect, there are no events in numberland.

MeditationWhat are we talking about when we talk about numbers? We can't navigate to them by following causal connections - so how do we get there from here?