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.
In what way do they exceed the expressive power of first-order logic?
Do we have completeness & soundness theorems for Lambda/Combinatory Logic?
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.
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:
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.
