A Limit of First Order Logic
A limit of first order logic concerning function definitions
Sam Buss is a logician who works in proof theory, and is one of the world’s experts on bounded arithmetic. He has proved some quite neat theorems—I will discuss his work in more detail in the future, since proof theory is closely related to the P=NP question.
Today I want to talk about a much simpler problem from logic. I hit upon it while trying to prove a theorem. I failed in proving my theorem—so far at least—but I discovered an interesting limitation of first order logic. This limit is not new, but I do not think it is as widely known as it should be.
I have always loved mathematical logic. I took undergraduate courses with two famous logicians, and was lucky to work with two other famous ones. Richard Vesley taught my first logic course; I took an advanced course, also as an undergraduate, from Helena Rasiowa. Later, as a graduate student I worked with Don Loveland. Finally, as a young assistant professor at Yale, I talked to Angus Macintyre a great deal about logic. He was kind enough to explain how the famous Paris-Harrington Theorem worked—among many other things.
Those I took courses from—Vesley and Rasiowa—each had their own unique styles of teaching. Since, my last discussion was on my current class on complexity theory I thought I might say something about their different styles of teaching.
Vesley read from our textbook, which was Elliott Mendelson’s famous book on logic. He would read a bit, and then we would discuss what he had just read. He often seemed to be confused, and we had to help him out. I think this was a great way to make us listen very carefully to his every word. I do not remember what I thought then, but my guess now is he knew the material very well. My guess is that his “confused” method was just his way to teach the material. A great course.
Rasiowa lectured, without any notes, without a textbook, and without any motivation. Yet it was one of the best courses I have ever had. She was a visiting professor at Case, where I got my undergraduate degree, who taught a course on advanced topics in logic. She had a way of presenting the material that made it hard to ask questions: there was almost no motivation, just definitions, theorems, and proofs. One time we started a new topic on proof tableaux’s. We had no idea why we were starting to discuss this topic. None. One brave soul raised his hand, she called on him, and he asked “why are we studying this?” She answered with a stern voice, You will understand. That ended the discussion of motivation, and we moved back to definitions, theorems, and proofs. We did eventually understand, but not for many weeks.
Let’s turn now to a problem in first order logic.
A Problem With First Order Logic
First order logic is well known to be extremely powerful, yet also to have strong limitations. For example, first order logic cannot in general define the transitive closure of a relation.
I know about these limits, but recently ran into another limitation that I was unaware of. The limit has to do with defining functions implicitly with first order statements.
The problem I ran into was simple: Consider a statement of the form,
What this says is: For each and , there are and , so that is true. For example, could be the formula:
The situation I ran into was that I wanted to express the following:
- That depends only on .
- That depends only on .
makes only a function of , but is still a function of both and . Of course re-ordering variables to form
makes only depend on , but again depends on both.
I tried for a while to express what I wanted in various ways by some more complex tricks. None worked. No matter what I did one of and wound up depending on both and .
I finally got to the point where I could actually prove that there is no way to do this. By then, I guessed that this was known. Perhaps, well known, but not well known to me.
Sam Buss to the rescue. I asked him about the issue, and he answered immediately:
This is a well-known construction, known as a Henkin quantifier or branching quantifier (after Leon Henkin). It is usually denoted as a rectangular block:
The meaning of (1) is just what I needed: the notation means that for each and there are and so that is true. Further, the value of only depends on , and the value of only depends on .
Sam added: “Statement (1) is known not to be expressible in first-order logic, so you are correct that it cannot be encoded in standard first-order logic.”
If there had been a way to encode this I would have had a neat result. Oh well.
I still am interested in situations where you can get around this problem. I believe that for certain statements it may be possible to define what I wanted in first order logic. I conjecture that there should be some property that will allow the branching quantifier to be defined for such statements.