Logic

Logic is concerned with thinking as a form of inference by reason. To use logic means to represent—to model—situations in logical terms and then to infer conclusions.

Nowadays modelling in logical terms means to use formal languages with a rigorous mathematical meaning, which allows for a rigorous mathematical notion of logical inference. But not only this, a rigorous notion of logical inference also offers an algorithmic perspective.

Here is an example for the entire process, including modelling and inference. Suppose we stipulate that a barber is someone who shaves all and only those people who don't shave themselves and we ask whether barbers shave themselves.

When you think about it for a while you will come to the conclusion that there cannot be any barber. So the question asked is void.

Here is the reason why there is no barber. Assume, by way of contradiction, there is some barber. Let \(b\) be such a barber. We proceed by a case distinction.

First case, \(b\) shaves \(b\). Then \(b\) is not a barber, because \(b\) would not shave him(her)self. A contradiction.

Second case, \(b\) does not shave \(b\). Then \(b\) is not a barber, because \(b\) would shave \(b\). A contradiction.

In mathematical logic, one can model the statement that defines barbers by a formula of so-called first-order logic: \[\forall x (\text{Barber}(x) \leftrightarrow \forall y (\text{Shaves}(x,y) \leftrightarrow \neg \text{Shaves}(y, y))) \enspace.\] Similarly, the statement that everyone is no barber can be paraphrased as a formula in mathematical logic: \[\forall x \neg \text{Barber}(x) \enspace.\]

What is even more important is that the second formula can be inferred from the first formula in a strict mathematical sense. The proper way to write this is: \[\forall x (\text{Barber}(x) \leftrightarrow \forall y (\text{Shaves}(x,y) \leftrightarrow \neg \text{Shaves}(y, y))) \models \forall x \neg \text{Barber}(x) \enspace.\]

In addition, there is also a formal proof of this statement:

$$ \begin{array}{rll} 1 & \forall x (\text{Barber}(x) \leftrightarrow \forall y (\text{Shaves}(x,y) \leftrightarrow \neg \text{Shaves}(y, y))) & \text{premise}\\ 2.0 & & x_0 \text{fresh}\\ 2.1 & \text{Barber}(x_0) & \text{assumption}\\ 2.2 & \text{Barber}(x_0) \leftrightarrow \forall y (\text{Shaves}(x_0, y) \leftrightarrow \neg \text{Shaves}(y, y)) & {\forall}\text{e from 1}\\ 2.3 & \text{Barber}(x_0) \rightarrow \forall y (\text{Shaves}(x_0, y) \leftrightarrow \neg \text{Shaves}(y, y)) & {\leftrightarrow}\text{e0 from 2.2} \\ 2.4 & \forall y (\text{Shaves}(x_0, y) \leftrightarrow \neg \text{Shaves}(y, y)) \rightarrow \text{Barber}(x_0) & {\leftrightarrow}\text{e1 from 2.2} \\ 2.5 & \forall y (\text{Shaves}(x_0, y) \leftrightarrow \neg \text{Shaves}(y, y)) & {\rightarrow}\text{e from 2.1 and 2.3}\\ 2.6 & \text{Shaves}(x_0, x_0) \leftrightarrow \neg \text{Shaves}(x_0, x_0) & {\forall}\text{e from 2.5}\\ 2.7 & \text{Shaves}(x_0, x_0) \rightarrow \neg \text{Shaves}(x_0, x_0) & {\leftrightarrow}\text{e0 from 2.6}\\ 2.8 & \neg \text{Shaves}(x_0, x_0) \rightarrow \text{Shaves}(x_0, x_0) & {\leftrightarrow}\text{e1 from 2.6}\\ 2.9.1 & \text{Shaves}(x_0, x_0) & \text{assumption}\\ 2.9.2 & \neg \text{Shaves}(x_0, x_0) & {\rightarrow}\text{e from 2.7 and 2.9.1}\\ 2.9.3 & \bot & {\bot}\text{i from 2.9.1 and 2.9.2}\\ 2.10 & \neg \text{Shaves}(x_0, x_0) & {\neg}\text{i from 2.9}\\ 2.11 & \text{Shaves}(x_0, x_0) & {\rightarrow}\text{e from 2.8 and 2.10}\\ 2.12 & \bot & {\bot}\text{i from 2.10 and 2.11}\\ 2.13 & \neg \text{Barber}(x_0) & {\neg}\text{i from 2.1 and 2.12}\\ 3 & \forall x \neg \text{Barber}(x) & {\forall}\text{i from 2} \end{array} $$

It would be too much to explain this in detail right now ... As you see this proof is quite long, but it is a formal proof in the sense that only syntactic rules are applied from one line to the next, which means a computer can check and even carry out the individual steps. As a consequence, a computer could check the entire proof or could even come up with it. This is the starting point for automated and semi-automated theorem proving.

But let's get back to the original question: do barbers shave themselves?

This question is ambiguous, because there are at least two different ways of interpreting the question:

• Does every barber shave him(her)self?
• Does there exist a barber who shaves him(her)self?

The corresponding statements give rise to different logical formulas. The first one gives rise to \[\forall x (\text{Barber}(x) \rightarrow \text{Shaves}(x,x)) \enspace.\] The second one gives rise to \[\exists x (\text{Barber}(x) \wedge \text{Shaves}(x,x)) \enspace.\]

Clearly, the answer to the first question is "yes", because there is no barber. In fact, the above formula is a consequence (in a strict sense) of the formula defining barbers: \[\forall x (\text{Barber}(x) \leftrightarrow \forall y (\text{Shaves}(x,y) \leftrightarrow \neg \text{Shaves}(y, y))) \models \forall x (\text{Barber}(x) \rightarrow \text{Shaves}(x,x)) \enspace.\]

On the other hand, the answer to the second question is "no". In fact, the negation of the corresponding formula is a consequence (in a strict sense) of the formula defining barbers: \[\forall x (\text{Barber}(x) \leftrightarrow \forall y (\text{Shaves}(x,y) \leftrightarrow \neg \text{Shaves}(y, y))) \models \neg \exists x (\text{Barber}(x) \wedge \text{Shaves}(x,x)) \enspace.\]