# In what way is the lambda calculus stronger than first-order logic?

This wikipedia article on combinatory logic says that Combinatory Logic, Lambda Logic and Turing Machines are equivalent computationally, but that both of these exceed the expressive power of first-order logic.

1. In what way do they exceed the expressive power of first-order logic?

2. Do we have completeness & soundness theorems for Lambda/Combinatory Logic?

• You probably know this already: anyway, note that first-order logic is Turing-complete, at least according to this article. – goblin Aug 12 '13 at 10:00
• I think FOL and other types of logic are better suited to represent knowledge and Turing machines and lambda calculus to represent computation. For instance I think the normalization property is more important for (typed) lambda calculus than completeness, which... is defined in terms of the Turing Machine? Anything Turing complete will have the halting problem, hence undecidability. I don't even know what is completeness anymore. Good question. – Trylks Aug 12 '13 at 14:34

1: In what way do they exceed the expressive power of first-order logic?

I don't know whether the untyped lambda calculus and first-order logic can be compared directly, but the Simple Type Theory is a typed lambda calculus and at the same time a formalization of higher-order logic. According to wikipedia:

The lambda calculus was introduced by mathematician Alonzo Church in the 1930s [...]. The original system was shown to be logically inconsistent in 1935 [...] in 1936 Church isolated and published just the portion relevant to computation, what is now called the untyped lambda calculus. In 1940, he also introduced a computationally weaker, but logically consistent system, known as the simply typed lambda calculus.

As I learned from "The seven virtues of simple type theory", the commonly used proof system for Simple Type Theory is equiconsistent to Mac Lane set theory. This in turn is considered to be a "good model" of "predicative mathematics". There are rumors that Randall Holmes has a proof that also Quine's New Foundations is equiconsistent to Mac Lane set theory.

2: Do we have completeness & soundness theorems for Lambda/Combinatory Logic?

The paper which introduced Henkin semantics for higher-order logic explicitly treated Simple Type Theory and contained Henkin's theorem. So completeness & soundness are similar to first-order logic in a certain sense. However, being equiconsistent with Mac Lane set theory means that consistency of Simple Type Theory cannot be proven in an absolute sense.

• Also, the rumors are no longer rumors. Holmes presented a proof sketch at a Cambridge gathering. His proof has yet to be confirmed (I believe the sketch is about 40 pages), but people seem optimistic that he was successful. – Dennis Aug 12 '13 at 20:21
• @Dennis Perhaps, but the connection to Mac Lane set theory depends on the interpretation of the available tidbits. As Aatu Koskensilta said on the linked page: "TST + Infinity has the same consistency strength as bounded Zermelo set theory." However, later tidbits talked about ZFU instead of TST, so these are still rumors for me. Of course, the goal must be to prove NF equiconsistent with a "predicative mathematics" system, because the idea behind stratification is that it should lead to predicativity. – Thomas Klimpel Aug 13 '13 at 0:25
• It was definitely TST+Inf that I've read Holmes claiming it was equiconsistent with. I can't find what I was reading recently, so I'm stepping back from the "people are optimistic" claim. I vaguely remember it being on the logic matters blog but a quick search didn't turn up anything. Thomas Forster is working through the proof with some students, I believe. The only recent mention I could find is here. – Dennis Aug 14 '13 at 0:36
• Ah! Here it is. I think what I was remembering was the "I see why the strategy should work" and the "I believe I will believe it" bits. I definitely overstated the claim, though. – Dennis Aug 14 '13 at 0:39

The article actually says that they "typically" exceed the power of first-order logic. First-order logic over a language of arithmetic that includes addition and multiplication is Turing complete, as you can arithmetically define every recursive function:

http://www.cogsci.rpi.edu/~heuveb/teaching/Logic/CompLogic/Web/Presentations/Arithmetical%20Definability.pdf

Another way you could compare untyped lambda calculus and first-order logic though is to consider what you can build with first-order functions vs. higher-order functions vs. functions in untyped lambda calculus which are essentially infinite-order.

I don't want to give any offense here. I can only comment as a lay person who has only a lay understanding of university maths.

It is noteworthy that not everyone here believes that first order logic is not Turing complete. A Turing machine is a finite state machine with an infinite tape. It is only an elementary (i.e. doable) computer coding exercise to implement this.

Only a tiny subset of Dartmouth Basic or Applesoft Basic is required for a Turing complete system. In recent years, Terry Tao asked (possibly on this site)if there was a group that was turing complete. Perhaps we could go through a box ticking exercise, noting that any one of the objects we encounter in introductory maths course at university, suffices by itself to build a Turing complete system.

The wikipedia entry for first order logic is quite detailed (many hundreds of lines).

It says: First-order logic is able to formalize many simple quantifier constructions in natural language, such as "every person who lives in Perth lives in Australia". But there are many more complicated features of natural language that cannot be expressed in (single-sorted) first-order logic. "Any logical system which is appropriate as an instrument for the analysis of natural language needs a much richer structure than first-order predicate logic" (Gamut 1991, p. 75).

The wikipedia article also says:

Ordinary first-order interpretations have a single domain of discourse over which all quantifiers range. Many-sorted first-order logic allows variables to have different sorts, which have different domains. ... When there are only finitely many sorts in a theory, many-sorted first-order logic can be reduced to single-sorted first-order logic. One introduces into the single-sorted theory a unary predicate symbol for each sort in the many-sorted theory, and adds an axiom saying that these unary predicates partition the domain of discourse.

From the above, I am far from convinced that first order logic is unsuitable for a full treatment of natural language. If we follow the Turing doctrine, aren't we forced to agree that we can code a full treatment of natural language using any Turing complete system which I am guessing from the wikipedia article, certainly includes first order logic.

I will follow up the Gamut article in an attempt to shed light on this. But prima facie the Gamut article is incorrect because it begs the question - it says you can't express natural language in single-sorted predicate calculus. But the Wikipedia article makes it clear that this may not be a limitation - at least it shows that a multi-sorted predicate calculus can be coded in single sorted predicate calculus.

• How do you account for the idea of 'strength'? – Mitch Oct 14 '16 at 17:01