|Computational class||Turing complete|
Entrance is an advanced, fully automatic, first-order logic theorem prover.
- 1 Overview
- 2 Basic examples
- 3 Advanced examples
- 4 Applications
- 5 Interpreters
Source code contains one or more function definitions.
Expression can be one of:
- Function call
Constant is represented as a non-negative integer. Constants are not related to each other and they cannot be compared or sorted. We cannot implicitly find the successor of
0 for example. Constants are used as unique identifiers. Two constants are equal iff they have the same representation in the source code (represent the same integer). Example of a constant:
Pair contains two expressions. Two pairs are equal iff their first elements are equal and their second elements are equal. Example of a pair:
Variable is a placeholder that can contain any expression. A variable can be substituted by any other expression as long as it is done consistently in that function definition. Example of a variable:
Function call is a transformation of an expression. Example of a function call:
f 5 (it means that function
f is applied to expression
Statement is a top-level expression (not nested in a pair or a function call).
Source code contains function definitions. Each function definition consists of left-hand-side, then an equal sign, then right-hand-side and ends with a semicolon. Left-hand-side is a function call and right-hand-side is any expression. For example:
f x = (x, x);
This is a function that takes any variable
x and produces a pair containing
x as both elements. Multiple definitions of the same function are allowed.
Input is a single statement that is to be proved. Output is the input statement with all function calls eliminated by applying function definitions.
If the statement is provable, the interpreter will find and output a proof (does not need to be the shortest proof). If the statement is unprovable within the system, the interpreter may or may not be able to detect that, so it may never halt.
The definitions above may not be clear, but it should be more obvious how the prover works once we see the examples.
Given the following source code that we posted before:
f x = (x, x);
and the following input statement:
The output will be:
f 0 is transformed into
(0, 0) by applying the first function definition for
x: 0. So far, one may think that Entrance is a simple functional language. However, in the next examples we will show how to actually implement a formal mathematical system.
Reversed function application
f x = (x, x); g f x = x;
g (0, 0)
Explanation: now we see a reversed function application. Function
g takes the output of
f applied to some variable
x and then returns that
x. In our example,
(0, 0) must be the output of
f called with something. Function
g finds that something and returns it.
If we tried to prove
g 0 or
g (0, 1), we would get the "No solution exists" message, because neither
(0, 1) can be an output of
f. If we tried to prove
g ((3, 3), (3, 3)), we would get
(3, 3) as the output.
f x = y;
In this example, output can be any expression, because
y is not related to
x in any way.
Recursive expression construction
f 0 = (0, 0); f g x = (x, x); g f x = x;
Here we have three function definitions.
f when called with
(0, 0). When called with something that is the return value of
g called with some
x, then returns
(x, x). In other words, function
f asserts that the argument that is passed to it is either
0, or is obtained by applying
f to something (because
g is an inverse of
In this system, statements
g (0, 0),
g ((0, 0), (0, 0)), and similar are provable, while, for example,
g 0 is not provable (because
0 cannot be an output of
f (x, x) = x;
f takes a pair of two identical elements. Therefore, we assert that both elements must be the same. Statements like
f (0, 0),
f (1, 1),
f ((5, 5), (5, 5)) are provable, while
f (1, 2),
f ((1, 1), (2, 2)) are not provable.
Now it is time to show how to implement some real mathematical systems. We first define inference rules that exist in the system. Each inference rule has zero or more premises and a conclusion. Axioms (or axiom schemas) are inference rules that have no premises.
In this example we will use a simplified version of Łukasiewicz system. We define the following inference rules (the first two are axioms because they have no premises and the third one is Modus ponens):
Our goal is to prove that . However, because there are no quantifiers (we did not define them in this system), instead of proving that for any , it is enough to prove that it is true for a single unique constant, for example .
Now, the question is how to represent implication in our program. Given that the implication is the only operator in this system and given that it has exactly two operands, we can use a pair to denote implication. For example, can be represented in our program as
When we talk about proving a statement in this system, we need to define what we expect as the output. Not only that we want to know whether the statement is provable, but we also want to know which inference rules are applied and in which order. Keeping in mind that the output will contain only pairs and constants, we need to encode inference rules as unique constants, so that we can recognize them in the output. For example, we can say that the first inference rule has identifier
10, the second one has identifier
20 and the third one (Modus ponens) has identifier
In the output, we want
(10, (x, y)) (where
y have concrete values) to represent an application of the first inference rule (the first axiom) to expressions
y. Similarly, we want
(20, (x, (y, z))) to represent an application of the second inference rule to expressions
z. Finally, we want
(30, (A, B)) to represent an application of Modus ponens to
A is the proof of some
B is the proof of the implication
(x, y) for some
This is our program:
f (10, (x, y)) = (x, (y, x)); f (20, (x, (y, z))) = ((x, (y, z)), ((x, y), (x, z))); f (30, (g x, g (x, y))) = y; g f x = x;
f represents inference rule application, while
g is an inverse of
g returns a proof of its argument. Now, if we look closer at function
f, we can see that it strictly follows our definition from the previous paragraph. Rule
10 (the first axiom) can be applied to any expressions
20 (the second axiom) can be applied to any expressions
30 (Modus ponens) can be applied to proofs of
(x, y), yielding
g (5, 5)
5 is just a random identifier, because we have not defined any quantifiers (for simplicity), so it is enough to prove the statement for some unique identifier. If we run the program, we would get the following output:
(30, ((10, (5, 0)), (30, ((10, (5, (0, 5))), (20, (5, ((0, 5), 5)))))))
It may seem a bit complicated, but let's analyze it and rewrite the obtained proof in a mathematical syntax. First, we can add spacing and format it better for readability:
(30, ( // Modus ponens (10, (5, 0)), // Axiom 1 (30, ( // Modus ponens (10, (5, (0, 5))), // Axiom 1 (20, (5, ((0, 5), 5))) // Axiom 2 )) ))
The first thing we may notice is the identifier
0 appearing out of nowhere. That is because there are more than one possible proof and the prover decided to use
0 for expressions that can be anything. It could decide to use any other expression, as long as it does not violate inference rules.
What we can see from the above proof is that we apply five inference rules. It is easier to read from the end, because that is how you would prove it manually. We first apply the first axiom to
x: 5 and
y: (5, 0). Then we apply the second axiom to
y: (0, 5) and
z: 5. Then we apply Modus ponens to the two obtained expressions. Then we again apply the first axiom, but this time to
x: 5 and
y: 0. Finally, we apply the Modus ponens again, obtaining the expression that we wanted to prove. This proof can be written using mathematical syntax:
The next step would to be introduce negation and prove some statements involving negation. However, since we would have two different operators (implication and negation), we could no longer use a simple pair to represent implication. We would need to introduce some unique identifiers for implication and negation (for example
0 for implication and
1 for negation). Then, we would represent as
(0, (A, B)) and as
(1, A). Operators cannot be confused with other identifiers, because operators require a pair, while identifiers are just literal constants.
Proving commutativity of equality
In this example we show how to define equality as an operator and how to prove the commutative property of equality. Since equality is an operator and since it is the only operator in this example, we can use a simple pair to denote it, meaning that can be represented as
First, we need to define what equality actually means. We can say that two expressions are equal iff all statements that are true for the first expression are also true for the second expression. However, that would require us to define quantifiers, which are out of scope for this example. So, we only define the equality in one direction, meaning that if two expressions
y are equal and some statement
P parametrized with
y is provable, then we can conclude that
P parametrized with
x is also provable (we basically swap the parameters).
The question now is how to define a parametrized statement. What we actually want is a statement containing some expressions, but which also can contain two placeholders that can be substituted with concrete values. Therefore, we can define parametrized statement in the following way:
0- Represents the first parameter
1- Represents the second parameter
(0, m)- means that
mis an expression that is not parametrized
(1, (m, n))- means that
(m, n)is a pair of two parametrized statements
Then, we need a function that will take a parametrized statements and two expressions and return the statement with the expressions substituted into it. We call that function
Finally, we need to define inference rules. We want to prove that from we can conclude . However, since we do not have implication now, we can define as an axiom. So, we have two inference rules:
and we want to prove that . Of course, it is trivial, but we show this example to demosntrate substitution. We use identifier
5 to denote
7 to denote
B. This is our program:
f 10 = (5, 7); f (20, ((P, (x, y)), (g (x, y), g subst (P, (x, y))))) = subst (P, (y, x)); g f x = x; subst (0, (x, y)) = x; subst (1, (x, y)) = y; subst ((0, m), xy) = m; subst ((1, (m, n)), xy) = (subst (m, xy), subst (n, xy));
Explanation: the first inference rule is denoted by identifier
10, while the second inference rule is denoted by a pair containing identifier
20 and a proof of the premises. Function
subst follows the algorithm explained above for substituting expressions into a parametrized statement. The
(x, y), but since we do not need to extract any of them, we can use a single variable
When we run this program with input statement
g (7, 5), we will get the following proof:
(20, (((1, (0, 1)), (5, 7)), (10, 10)))
Let's analyze it in details. We have three inference rule applications:
(20, ( // Second rule ((1, (0, 1)), (5, 7)), // P, x and y (10, 10) // Proofs for x = y and Px,y ))
First, the prover has proved that (remember that
5 denotes and
7 denotes ) by applying the first axiom (which literally says exactly that). Then the prover constructed a parametrized statement defined as . Therefore, is true. Then the prover used the second inference rule to conclude that is also true. That is the end of the proof.
Zermelo–Fraenkel set theory
It is certainly possible to model the ZFC system. We showed how to implement implication, equality, parametrized statements and substitutions. We also showed assertions and expression transformation via inference rules.
However, it is not so easy to implement ZFC, because the nine axioms of the ZFC are not enough. Entrance does not know anything about quantifiers, equivalence operator and logical operators. For each logical operator we need to define inference rules. For universal and existential quantifiers we need to also define at least two inference rules to specify how they behave and we would need to use parametrized statements to model bound variables. For each operator, we would need to introduce a new unique identifier and we would probably need another program which would transform the Entrance proof to something humans can easily read and understand.
Also, the axiom of choice would be problematic, because it does not state anything about how the choice function is to be constructed. It simply states that such a function exists. The axiom of choice can be formally represented in many different ways, but if the ZFC is inconsistent, the way we formally represent the axiom of choice may influence the consistency of ZFC.
Entrance can be used for a lot of different tasks. For example, it can be used to make an interpreter for Halt halt halt. It can be used to make a program that searches (not guaranteed to halt) for a solution to any NP-hard problem, such as
- Determine whether a given Turing-machine halts
- Determine whether two lambda expressions are equivalent
- Determine whether a given Post correspondence problem has a solution
- Determine whether two given programs give identical outputs for all inputs
- Determine whether two given function in ƎↃИAЯT are equivalent