◀ ▲ ▶Branches / Logic / Chapter: The Proving Machine - an Automation of Logical Reasoning

Chapter: The Proving Machine - an Automation of Logical Reasoning

The ultimate goal of the formal concepts we have introduced so far is to develop a formal system, in which it is possible to draw logical conclusions from assumptions. Humans can do so but our logical system should be capable to derive logical arguments more or less automatically, e.g. by an imaginary computer, which we will call in this section the Proving Machine (PM). We will summarize all concepts introduced so far and check, whether we have all components necessary to get our PM working.

1. First of all, our PM is given an alphabet of finitely many letters $\Sigma.$ We assume that it cconcatenate the letters to strings $s$. In principle, the PM can create infinitely many different strings $s$ out of the alphabet $\Sigma.$ We denote this infinite set $\Sigma^*.$
2. Next, from all the infinitely many strings $s\in\Sigma^*,$ we choose only some strings and call this subset $L\subset \Sigma^*$ a language. You can think of $L$ as the set of all (finitely or infinitely many) words, which the PM should ever be able to use.
3. To enable our PM to decide, whether a given string $s \in\Sigma^*$ belongs to a language $L$, we have to restrict the language to some grammar. In other words, we restrict the language $L$ to be a formal language. The syntax can be compared to a computer program that enables the PM to accept only strings $s$ belonging to the language $L$ as its input. It should reject any other input.
4. Besides, we want the PM to give us answers about a set $U$ of mathematical objects we want to study. We call $U$ the domain of discourse $U$ is completely independent of the language $L.$ However, we have chosen the alphabet $\Sigma$ and the syntax in a way that the resulting language $L$ is powerful enough to let the PM give us answers about $U.$
5. "Giving us answers about $U$ in a formal language $L$" means in fact that the PM should be able to prove statements formulated in $L$ about $U$. Ideally, given a statement $s\in L$ as input, the PM should return us "true", if the statement is true or "false" if the statement is false. Also, if the PM is not able to decide if a statement is true or false, it should return us "undefined". For this purpose, we have provided the PM with two other computer programs, one we denote by $I$ which interprets a given string $s$. Once $s$ is interpreted, the second program $[[]]_I$, called the "truth function" of interpretation gives us the answer, whether the interpreted string is true or false.

Are we done? You might say, in principle, yes, we are. We have constructed a PM, which can interpret any syntactically correct string $s\in L,$ which we might feed it with. We might even feed it with strings representing statements about all yet unproven conjectures stated about mathematical objects in the domain of our discourse $U$, and the PM will give us the awaited answers "true", "false" or "undefined". So are we are done with building our PM? Not quite.

Note that the interpretation $I$ and its truth function $[[]]_I$ must be very complex computer programs that somehow tell the PM how to "think logically." Thus, we only have shifted the problem to another level, creating black boxes - the functions $I$ and $[[]]_I$. Enabling the PM to give us all the awaited answers about $U$ means that we have to tell it a priori which answers are correct and which not.

Therefore, we will still need some tuning of the PM to get it working. Maybe we need even more components? These components are axioms, rules of inference, and the derivability property.

Table of Contents

1. Definition: Axioms
2. Definition: Rules of Inference
3. Definition: Logical Calculus
4. Definition: Proofs and Theorems in a Logical Calculus

Mentioned in:

Chapters: 1

Thank you to the contributors under CC BY-SA 4.0!

Github: