"Mathematical logic is the science of algorithm evaluating algorithms."

Do you think that this is an overly generalizing, far fetched proposition or an almost trivial statement? Wait, don't cast your vote before the end of this short essay!

It is hard to dispute that logic is the science of drawing correct conclusions. It studies theoretically falsifiable rules the lead to derivations which are verifiable in a finite amount of mechanical steps, even by machines.

Let's dig a bit deeper by starting to focusing on the "drawing correct conclusions" part, first. It implies the logic deals both with abstract rules: "drawing" and their meaning: "conclusions".

Logic is not just about mindless following of certain rules (that's algebra :P) its conclusions must have truth values that refer to some "model". Take for example De Morgan's law:

not (a and b) = (not a) or (not  b).

It can be checked for each four possible substitutions of boolean values: a = false, b = false; a = false, b = true; .... If we agreed upon the standard meaning of the logical not, or and and operators, then we must conclude that the De Morgan's rule is perfect. On the other hand: the similar looking rule

not (a and b) = (not a) and (not b)

can be easily refuted by evaluating for the counterexample a = false, b = true.

Generally: in any useful mathematical system, logical conclusions should work in some interesting model.

However, in general, total verifiability is way too much to ask. As Karl Popper pointed out: often one must be satisfied with falsifiability of scientific statements as a criterion. For example, the following logical rule

not (for each x: F(x)) <=> exists x : not F(x)

is impossible to check for every formula F.  Not directly checkable statements include all those where the set of all possible substitutions is (potentially) infinite.

This observation could be formalized by saying that a mapping from abstract to concrete is required. This thinking can be made precise by formalizing further: logicians study the connection between axiom systems and their models.

But wait a minute: is not there something fishy here? How could the process of formalization be formalized? Is not this so kind of circular reasoning? In fact, it is deeply circular on different levels. The most popular way of dealing with this Gordian knot is simply by cutting it using some kind of naive set theory in which the topmost level of arguments are concluded.

This may be good enough for educational purposes, but if one in the following questions should always be asked: What is the basis of those top level rules? Could there be any mistake there? Falsifiability always implies an (at least theoretical) possibility of our rules being wrong even at the topmost level. Does using a meta-level set theory mean that there is some unquestionable rule we have to accept as God given, at least there?

Fortunately, the falsifiability of axioms has another implication: it requires only a simple discrete and finite process to refute them: an axiom or rule is either falsified or not. Checking counterexamples is like experimental physics: any violation must be observable and reproducable. There are no fuzzy, continuous measurements, here. There are only discrete manipulations. If no mistakes were made and some counterexample is found, then one of the involved logical rules or axioms had to be wrong.

Let's squint our eyes a bit and look the at whole topic from a different perspective: In traditional view, axiom systems are considered to be sets of rules that allow for drawing conclusions. This can also be rephrased as: Axiom systems can be cast into programs that take chains of arguments as parameter and test them for correctness.

This seems good enough for the the formal rules, but what about the semantics (their meaning)?

In order to define the semantics, there need to be map to something else formally checkable, ruled by symbolics, which is just information processing, again. Following that path, we end up with with the answer: A logical system is a program that checks that certain logical statements hold for the behavior of another program (model).

This is just the first simplification and we will see how the notions of "check", "logical statement", and "holds" can also be dropped and replaced by something more generic and natural, but first let's get concrete and let us look at the two most basic examples:

1. Logical Formulas: The model is the set of all logical formulas given in terms of binary and, or and the not function. The axiom system consists of a few logical rules like the commutativity, associativity and distributivity of and and or, the De Morgan laws as well as not rule not (not a)=a. (The exact choice of the axiom system is somewhat arbitrary and is not really important here.) This traditional description can be turned into: The model is a program that takes a boolean formulas as input and evaluates them on given (input) substitutions. The axiom system can be turned as a program that given a chain of derivations of equality of boolean formulas checks that each step some rewritten in terms of one of the predetermined axioms, "proving" the equality of the formulas at the beginning and end of the conclusion chain. Note that given two supposedly equal boolean formulas ("equality proven using the axioms"), a straightforward loop around the model could check that those formulas are really equivalent and therefore our anticipated semantic relationship between the axiom system and its model is clearly falsifiable.
2. Natural numbers: Our model is the set of all arithmetic expressions using +, *, - on natural numbers, predicates using < and = on arithmetic expressions and any logical combination of predicates. For the axiom system, we can choose the set of Peano axioms. Again: We can turn the model into a program by evaluating any valid formula in the model. The axiom system can again be turned into a program that checks the correctness of logic chains of derivations. Although we can not check verify the correctness of every Peano formula in the model by substituting each possible value, we still can have an infinite loop where we could arrive at every substitution within a finite amount of steps. That is: falsifiability still holds.

The above two examples can be easily generalized to saying that: "A logical system is a program that checks that certain kinds of logical statements can be derived for the behavior of another program (model)."

Let us simplify this a bit further. We can easily replace the checking part altogether by noticing that given a statement, the axiom system checker program can loop over all possible chains of derivations for the statement and its negation. If that program stops then the logical correctness of the statement (or its negation) was established, otherwise it is can neither be proven nor refuted by those axioms. (That is: it was independent of those axioms.)

Therefore, we end up just saying: "A logical system is program that correctly evaluates whether a certain logical statement holds for the behavior of another program, (whenever the evaluator program halts.)"

Unfortunately, we still have the relatively fuzzy "logical statement" term in our description. Is this necessary?

In fact, quantifiers in logical statements can be easily replaced by loops around the evaluating program that check for the corresponding substitutions. Functions and relations can be resolved similarly. So we can extend the model program from a simply substitution method to one searching for some solution by adding suitable loops around it. The main problem is that those loops may be infinite. Still, they always loop over a countable set. Whenever there is a matching substitution, the search program will find it. We have at least falsifiability, again. For example, the statement of Fermat's Last Theorem is equivalent to the statement that program the searches for its solution never stops.

In short: the statement "logical statement S holds for a program P" can always be replaced by either "program P' stops" or "program P' does not stop" (where P' is a suitable program using P as subroutine, depending on the logical statement). That is we finally arrive at our original statement:

"Mathematical logic is the science of algorithm evaluating algorithms [with the purpose making predictions on their (stopping) behavior.]"

Simple enough, isn't it? But can this be argued backward? Can the stopping problem always be re-cast as a model theoretic problem on some model? In fact, it can. Logic is powerful and the semantics of the the working of a programs is easily axiomatized. There really is a relatively straightforward  one-to-one correspondence between model theory and algorithms taking the programs as arguments to predict their (stopping) behavior.

Still, what can be gained anything by having such an algorithmic view?

First of all: it has a remarkable symmetry not explicitly apparent by the traditional view point: It is much less important which program is the model and which is the "predictor". Prediction goes both ways: the roles of the programs are mostly interchangeable. The distinction between concrete and abstract vanishes.

Another point is the conceptual simplicity: the need for a assuming a meta-system vanishes. We treat the algorithmic behavior as the single source of everything and look for symmetric correlations between the behavior of programs instead of postulating higher and higher levels of meta-theories.

Also, the algorithmic view has quite a bit of simplifying power due to its generality:

Turing's halting theorem is conceptually very simple. (Seems almost too simple to be interesting.) Goedel's theorem, on the other hand, looks more technical and involved. Still, by the above correspondence, Turing's halting theorem is basically just a more general version Goedel's theorem. By the correspondence between the algorithmic and logical view, Turing's theorem can be translated to: every generic enough axiom system (corresponding to a Turing complete language) has at least one undecidable statement (input program, for which the checking program does not stop.) The only technically involved part of Goedel's theorem is to check that its corresponding program is Turing complete. However, having the right goal in mind, it is not hard to check at all.

First order arithmetic is incomplete. Except that it's also complete. Second order arithmetic is more expressive - except when it's not - and is also incomplete and also complete, except when it means something different. Oh, and full second order-logic might not really be a logic at all. But then, first order logic has no idea what the reals and natural numbers are, especially when it tries to talk about them.

That was about the state of my confusion, and I set out to try and clear it up. Here I'll try and share an understanding of what is really going on with first and second order logic and why they differ so radically. It will be deliberately informal, so I won't be distinguishing between functions, predicates and subsets, and will be using little notation. It'll be exactly what I wish someone had told me before I started looking into the whole field. 

Meaningful Models

An old man starts talking to you about addition, subtraction and multiplication, and how they interact. You assume he was talking about the integers; turns out he means the rational numbers. The integers and the rationals are both models of addition, subtraction and multiplication, in that they obey all the properties that the old man set out. But notice though he had the rationals in mind, he didn't mention them at all, he just listed the properties, and the rational numbers turned out, very non-coincidentally, to obey them.

These models are generally taken to give meaning to the abstract symbols in the axioms - to give semantics to the syntax. In this view, "for all x,y xy=yx" is a series of elegant squiggles, but once we have the model of the integers (or the rationals) in mind, we realise that this means that multiplication is commutative.

The White House says there will be a temporary ban on new deep-water drilling, and BP will have to pay the salaries of oilmen who have no work during that ban.  I scratched my head trying to figure out the logic behind this.  This was my first attempt:

1. BP caused an oil spill.
2. The oil spill caused a ban on drilling.
3. The ban on drilling caused oilmen to be out of work.
4. Therefore, BP caused oilmen to be out of work.
5. Therefore, BP should pay these oilmen.

This logic works equally well in this case:

1. Rachel Carson wrote Silent Spring.
2. Silent Spring caused a ban on DDT use.
3. The ban on DDT use caused factory workers to be out of work.
4. Therefore, Rachel Carson caused factory workers to be out of work.
5. Therefore, Rachel Carson should pay these workers.

But "everyone" would agree that the second example is fallacious.  Are people so angry at BP that they can't think at all?

"...90116633393348054920083..."

He paused for a moment, and licked his recently reconstructed lips. He was nearly there. After seventeen thousand subjective years of effort, he was, finally, just seconds away from the end. He slowed down as the finish line drew into sight, savouring and lengthening the moment where he stood there, just on the edge of enlightenment.

"...4...7...7...0...9...3..."

Those years had been long; longer, perhaps, in the effects they had upon him, than they could ever be in any objective or subjective reality. He had been human; he had been frozen, uploaded, simulated, gifted with robotic bodies inside three different levels of realities, been a conscript god, been split into seven pieces (six of which were subsequently reunited). He had been briefly a battle droid for the army of Orion, and had chanted his numbers even as he sent C-beams to glitter in the dark to scorch Formic worlds.

He had started his quest at the foot of a true Enlightened One, who had guided him and countless other disciples on the first step of the path. Quasi-enlightened ones had guided him further, as the other disciples fell to the wayside all around him, unable to keep their purpose focused. And now, he was on the edge of total Enlightenment. Apparently, there were some who went this far, and deliberately chose not to take the last step. But these were always friends of a friend of an acquaintance of a rumour. He hadn't believed they existed. And now that he had come this far, he knew these folk didn't exist. No-one could come this far, this long, and not finish it.

This example (and the whole method for modelling blackmail) are due to Eliezer. I have just recast them in my own words.

We join our friends, the Countess of Rectitude and Baron Chastity, in bed together. Having surmounted their recent difficulties (she paid him, by the way), they decide to relax with a good old game of prisoner's dilemma. The payoff matrix is as usual:

Were they both standard game theorists, they would both defect, and the payoff would be (1,1). But recall that the baron occupies an epistemic vantage over the countess. While the countess only gets to choose her own action, he can choose from among four more general tactics:

1. (Countess C, Countess D)→(Baron D, Baron C)   "contrarian" : do the opposite of what she does
   
2. (Countess C, Countess D)→(Baron C, Baron C)   "trusting soul" : always cooperate
   
3. (Countess C, Countess D)→(Baron D, Baron D)   "bastard" : always defect
   
4. (Countess C, Countess D)→(Baron C, Baron D)   "copycat" : do whatever she does

Recall that he counterfactually considers what the countess would do in each case, while assuming that the countess considers his decision a fixed fact about the universe. Were he to adopt the contrarian tactic, she would maximise her utility by defecting, giving a payoff of (0,5). Similarly, she would defect in both trusting soul and bastard, giving payoffs of (0,5) and (1,1) respectively. If he goes for copycat, on the other hand, she will cooperate, giving a payoff of (3,3).

Thus when one player occupies a superior epistemic vantage over the other, they can do better than standard game theorists, and manage to both cooperate.

"Isn't it wonderful," gushed the Countess, pocketing her 3 utilitons and lighting a cigarette, "how we can do such marvellously unexpected things when your position is over mine?"

This is Eliezer's model of blackmail in decision theory at the recent workshop at SIAI, filtered through my own understanding. Eliezer help and advice were much appreciated; any errors here-in are my own.

The mysterious stranger blackmailing the Countess of Rectitude over her extra-marital affair with Baron Chastity doesn't have to run a complicated algorithm. He simply has to credibly commit to the course of action:

"If you don't give me money, I will reveal your affair."

And then, generally, the Countess forks over the cash. Which means the blackmailer never does reveal the details of the affair, so that threat remains entirely counterfactual/hypothetical. Even if the blackmailer is Baron Chastity, and the revelation would be devastating for him as well, this makes no difference at all, as long as he can credibly commit to Z. In the world of perfect decision makers, there is no risk to doing so, because the Countess will hand over the money, so the Baron will not take the hit from the revelation.

Indeed, the baron could replace "I will reveal our affair" with Z="I will reveal our affair, then sell my children into slavery, kill my dogs, burn my palace, and donate my organs to medical science while boiling myself in burning tar" or even "I will reveal our affair, then turn on an unfriendly AI", and it would only matter if this changed his pre-commitment to Z. If the Baron can commit to counterfactually doing Z, then he never has to do Z (as the countess will pay him the hush money), so it doesn't matter how horrible the consequences of Z are to himself.

To get some numbers in this model, assume the countess can either pay up or not do so, and the baron can reveal the affair or keep silent. The payoff matrix could look something like this:

In the post Outlawing Anthropics, there was a brief and intriguing scrap of reasoning, which used the principle of reflective inconsistency, which so far as I know is unique to this community:

If your current system cares about yourself and your future, but doesn't care about very similar xerox-siblings, then you will tend to self-modify to have future copies of yourself care about each other, as this maximizes your expectation of pleasant experience over future selves.

This post expands upon and attempts to formalize that reasoning, in hopes of developing a logical framework for reasoning about reflective inconsistency.

J. Y. Girard, et al. (1989). Proofs and types. Cambridge University Press, New York, NY, USA. (PDF)

I found introductory description of a number of ideas given in the beginning of this book very intuitively clear, and these ideas should be relevant to our discussion, preoccupied with the meaning of meaning as we are. Though the book itself is quite technical, the first chapter should be accessible to many readers.

From the beginning of the chapter:

Let us start with an example. There is a standard procedure for multiplication, which yields for the inputs 27 and 37 the result 999. What can we say about that?

A first attempt is to say that we have an equality

27 × 37 = 999

This equality makes sense in the mainstream of mathematics by saying that the two sides denote the same integer and that × is a function in the Cantorian sense of a graph.

This is the denotational aspect, which is undoubtedly correct, but it misses the essential point:

There is a finite computation process which shows that the denotations are equal. It is an abuse (and this is not cheap philosophy — it is a concrete question) to say that 27 × 37 equals 999, since if the two things we have were the same then we would never feel the need to state their equality. Concretely we ask a question, 27 × 37, and get an answer, 999. The two expressions have different senses and we must do something (make a proof or a calculation, or at least look in an encyclopedia) to show that these two senses have the same denotation.

You've all seen it. Sentences like "this sentence is false": if they're false, they're true, and vice versa, so they can't be either true or false. Some people solve this problem by doing something really complicated: they introduce infinite type hierarchies wherein every sentence you can express is given a "type", which is an ordinal number, and every sentence can only refer to sentences of lower type. "This sentence is false" is not a valid sentence there, because it refers to itself, but no ordinal number is less than itself. Eliezer Yudkowsky mentions but says little about such things. What he does say, I agree with: ick!

In addition to the sheer icky factor involved in this complicated method of making sure sentences can't refer to themselves, we have deeper problems. In English, sentences can refer to themselves. Heck, this sentence refers to itself. And this is not a flaw in English, but something useful: sentences ought to be able to refer to themselves. I want to be able to write stuff like "All complete sentences written in English contain at least one vowel" without having to write it in Spanish or as an incomplete sentence.¹ How can we have self-referential sentences without having paradoxes that result in the universe doing what cheese does at the bottom of the oven? Easy: use fuzzy logic.