Propositional logic is perfect for people who like to automate things like computer scientists. If you have a theory that can be described using only propositional logic, you can prove every theorem (true statement) in your theory using an algorithm in finite time. Moreover, you can also debunk any non-theorem in finite time, too. In logic jargon, this means that propositional logic has a proof system or mechanism that is sound (will never produce junks) and complete (produce all possible truths). In fact, SAT-solver is all you need. SAT-solver has entered industry for long time of course and a prestigious competition is running every year to make the algorithm faster.

Mathematicians like to argue using wild and abstract imaginations. They invent and talk about numbers, infinity, and what not. The proof of a theorem by a mathematician, including contemporary ones, can read controversial to other expert mathematicians due to its abstract nature; not only the objects in question, but also the way each step in the argument is carried.

Logic in mathematics usually comes later only to verify the arguments used. Unfortunately, many mathematicians will be frustrated if only propositional logic is allowed. They will be very limited when talking about properties of natural numbers, for example, which first order logic needs to come in play; probably equipped with mathematical induction to support their arguments. Sometimes, one even needs to lift the background logic to the second-order logic or even higher-order logic when the arguments are too complicated. For those who are not familiar, these are some kinds of logic which allow more expressive statements and sophisticated arguments to produce new truths.

The problem is, once a theory is already expressive enough to allow us to talk about natural number systems (e.g. Robinson Arithmetic is the most minimal such theory I can think of), there must be a true statement, true according to that theory, that we can never prove under some sound mechanism. This is a phenomenal result in mathematical logic by Kurt Gödel called Gödel’s Incompleteness Theorem in 1931. Many philosophical discussions arise about the limitation of mathematics in our search for truths; some exaggerates this result, too, sometimes based on a misinterpretation of the results.

Anyway, the remaining of this post will not be about the interpretation of Kurt Gödel’s work and its philosophical implication. It is interesting, but in this post, the goal would be to convey that we can still escape from this limitation by designing a new logic that is expressive enough to talk about complex stuff, yet still has sound and complete proof mechanism. Modal logic is probably favorites of many and I will probably post about it some day if time permits, but here I want to describe a mechanism to decide whether a statement is true or not in **first order logic limited with unary predicate** **only**.

First of all, propositional logic allows us to form a sentence composed of propositions and connect them with *and*, *or*, *if*–*then*, and *not*. By proposition, I mean a sentence which simply describes a property of one or more objects, for example “*Donald Trump is evil*” and can be either true or false; a compound sentence then will be like “*Donald Trump is evil and my mom hates him.*“

In first order sentence, we can introduce variables in our sentence such as “Someone is evil” or “Everyone is evil”. This sentence uses variables since we do not mention who exactly is evil. Using mathematical notations, we can write “Someone is evil” as where is read “* is evil*” and is read “*there exists an *“; the full sentence is read “There is an such that is evil”. “Everyone is evil” can be written as where is read “*for every *“. The is called variable and is a predicate (or, a property) that we want to attach to some objects.

A predicate can involve more than one objects. One can define a binary predicate as “ *hates* ” which is a predicate involving two objects, or a ternary predicate such as defined as “ is a mutual friend of and “. It can also involve more that two objects. A sentence such as “Someone is evil and hated by everybody” can be written as first order sentence using our logic symbols that we have described above.

This post tries to convince you that the fragment of of first order logic that only allows unary predicates has a sound and complete proof mechanism. More concretely, predicates that involve two or more objects such as , and so on are not allowed in a sentence in our theory.

An example of a sentence in a first-order sentence which consists of only unary predicate is

which can be read “Everything is or everything is , but there is something that is neither nor “, for any meaning we attach to and . In first order logic, this can never be true, for whatever the meaning of and we use and any objects in place of . This kind of sentence is called contradiction in logic. If you are not convinced yet, replace and with “rich” and “beautiful”, respectively, and reflect about what the reading above tries to state when “everything” is changed to “everyone”.

To decide any first-order sentence with only unary predicate, the key idea is based on the following fact proved by Löwenheim-Skolem in 1915, which I rephrase frivorously:

If a first-order sentence can expressed using

Löwenheim-Skolem, 1915unary predicatesand variables, and ifeveris a true statement, there will be a world consisting of only objects such that is alsotrue in this (finite) world.

(Readers might have noticed and be disappointed that this theorem is proved way before Gödel proved his extraordinary results. But I would like to mention that the endeavor to find a decidable logic for more and more fragments of mathematics are still alive until today.)

The fact that $\mathbb{T}$ will be true in a finite world with only objects, when it can be true, is so important that a computer can just focus on these finite worlds and brute-force on all possible interpretations of the predicates on each of the objects (whether each object satisfies a certain predicate) and terminate eventually once it finishes traversing all the possibilities of these interpretations, which are also finite.

Our sentence has predicates, viz. and , and variables, viz. , so if can be true, it must be true too in some world that has objects in it. More concretely, imagine a world that only has 12 people in it where each person is named A, B, C, D, E, F, G, H, I, J, K, and L. Next, some of these people might have property and . Again, without loss of generality, take for example, predicate is “rich” and is “beautiful”. Under this interpretation, some of these 12 people are rich and some are beautiful. For example, a possible scenario would be A, B, C, F, and G being rich while the rest is poor and B , C, H, and L, are beautiful and the rest is ugly. Of course there are many more possible scenarios in this world about who’s rich and beautiful.

The Löwenheim-Skolem theorem states that if is ever true (in any world and any interpretation of and ), there must be a scenario in this world of 12 people that we have described above where is true. Thus, a computer can just search over all possible scenarios to find out whether is true in at least one scenario: that there is a scenario where “every one of A, B, C, D, E, F, G, H, I, J, K, L is rich, or every one of A, B, C, D, E, F, G, H, I, J, K, L is beautiful, but at least one of them is neither rich nor beautiful”. If none of these scenarios in this world of only 12 people make true, then can never be true for any meaning we attach to and and any objects with assign to from any possible worlds, i.e. is guaranteed to be a contradiction; it will be never true whatsoever. Indeed, it is also easier for us to check our intuition about whether can be true in this world of 12 people. We can imagine that if all these 12 people are rich, then none of them can be not-rich, since everybody is rich; contradicting the last premise about someone being not rich. Similarly, if the 12 people are beautiful, then the last premise, about someone being not beautiful, cannot also be satisfied since everybody is beautiful. The main weapon is this reduction to the world of only 12 people; we can just focus the checking on this world of 12 people. The finiteness entails that the number of states/scenarios that the computer needs to check is finite too and hence it just needs to check one by one and will eventually finish them all. If this reduction does not exist, the computer might need to run indefinitely and no guarantee that the procedure will ever give us an answer. In our example, the computer will finally check all scenarios and find out that none of them makes true, hence we can be sure that can never be true no matter what the context is.

Now, one may ask: Is there a first-order statement that is ever true and how can we check it? The answer is yes and the following example will demonstrate it. Consider the following sentence :

.

If we agree to interpret as “rich” and as “beautiful”, then the statement will read “Somebody is rich and somebody is beautiful but nobody is both rich and beautiful.” The sentence has predicates and variables, so our decision algorithm would consider a world consisting objects (or people) again, let’s say A, B, C, D, E, F, G, H, I, J, K, L. Our computer can try to check all the possible scenarios who’s rich and who’s beautiful and see if at least one of makes true. The computer will eventually find, for example, that a scenario where the A, B, C, D, E, F are beautiful but not-rich, while G, H, I, J, K, L are rich but not-beautiful, is an instance of the world of 12 people where is true! Thus the computer will say: “Yes, can be true.” This is not the only possible scenario that makes true though, but the Löwenheim-Skolem theorem guarantees that it will find at least one scenario in this world of 12 people; no need to check the other infinite possibilities.

The proof of the theorem will not be contained here but I hope this post has convinced you how limiting the expressiveness of logic can give us power to effectively separate what is right and wrong in a logical system. I would not say that we should drop the whole number system for example; to escape Gödel’s theorem. I think numbers are useful and beautiful and many mathematical objects are. But for many real-life problems, I believe, the general discussion in mathematics will automatically reduce to finite domains hence allowing us to brute-force using computer; if we are not constrained with efficiency issue.

One possible simple take on Gödel’s Incompleteness Theorem is thus as follows. Gödel’s Incompleteness Theorem shall not stop people doing mathematics to invent more truths, even though not all, in the mathematical universes, and possibly develop us with new languages to speak about the physical nature and other complex phenomena. Probably some of the truths that are not provable in the platonic world of mathematics do not really matter in real world when there is an urgency to deal with the relevant mathematics. In addition to it, hopefully, in real world, their theory will be reducible to something that is more tangible, be it immediately or after some amount of work on simplification and/or modification. This might be true since there is a big chance that in real world, the mathematics is forced to fit into discrete and finite domains. There is probably a chance that in such case, we might not need to use the full theory to solve the real-world problems, but simply just a fragment of it. Indeed, this is what many logicians are trying to do. Many logicians around the world, especially those who are motivated with computational aspect of truths, are absorbed and enthusiastic into finding fragments of logic that allow us to effectively and probably efficiently decide truths, but are expressive enough to talk about complex problems they need to tackle. Check out the development of modal logic and description logic, for example.

Do you agree with this view of Gödel’s Incompleteness Theorem? What do you think are the issues of this approach? Let me know what you think.