Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >

Examplessmall logo

Examples -> Algebra -> lagrange3.html

This example is the algebraic part of Lagrange's theorem.

Theorem: Let G be a group and H a subgroup of G. Let a be a member of G. Then there is a one-one correspondence between H and the coset Ha.

This file constructs a map from a subgroup H of a group G to the coset Ha, and also constructs its inverse. The map in question takes x to x*a, and the inverse takes z to z*i(a), where i(a) denotes the inverse of a. Otter-lambda uses lambda-unification to construct these maps, which are given by the lambda terms lambda(x,x*a) and lambda(z,z*i(a)) respectively.

Answer literals (which use the symbol $ANS) are used in Otter and Otter-lambda just to provide information to the user. By using $ANS in the input file, we cause Otter-lambda to show us the lambda terms it constructed in find a proof.

We do not use a unary predicate for G(x). This is not an error or oversight. For an explanation of why we do not need G(x), see Implicit Typing

The first axiom is always used when equality is involved: 1 [] x=x.

The next axiom is one way of formulating the axiom for group inverse, without a symbol for the identity element: 2 [] u*x=v|u!=v*i(x).

The next axiom defines the existential quantifier. It says "If the predicate Z holds of any object w then there exists an x such that Z(x)". Here "exists" is treated as a constant that applies to a predicate; predicates are given by lambda-terms. What we would usually write as "there exists an x such that P(x)" is written here in the form exists(lambda(x,Ap(P,x))). 3 [] -Ap(Z,w)|exists(lambda(x,Ap(Z,x))).

We now define f to be the characteristic function of the coset Ha: 4 [] f(w)=exists(lambda(x,and(H(x),x*a=w))).

Now, the theorem in question is that there exists an X such that X maps H into Ha, and an inverse map Y such that for a in H, we have Y(X(a)) = a. Using Ap to express function application, this would be "for all z in H, Ap(X,z) is in H and Ap(Y,Ap(X,u)) = z". As usual in a clause-based prover, we negate the goal, so the first z becomes a Skolem term g(X) and the second z becomes another Skolem term r(X,Y). We could equally well have made both occurrences of z into r(X,Y), but we didn't do that. X and Y are variables, and the negated goal says that g(X) is in H, and "either Ap(X,g(X)) is not in the coset H(g(X)), or it's not the case that Ap(Y,Ap(X,r(X,Y))) = r(X,Y)." But of course we use f(z) to express that z belongs to the coset Hz. Our negated goal then is expressed by the next two clauses:

5 [] H(g(X)).

6 [] -f(Ap(X,g(X)))|$ANS(X)|Ap(X,Ap(Y,r(X,Y)))!=r(X,Y)|$ANS(Y).

We put the answer literals in, as explained above, so we can see the values produced for X and Y.

Otter-lambda begins the proof by starting with line 6 and using line 4 to expand the definition of f:

9 [6,demod,4] -exists(lambda(x,and(H(x),x*a=Ap(y,g(y)))))|$ANS(y)|Ap(y,Ap(z,r(z)))!=r(z)|$ANS(z).

Then it uses the definition of "exists" from line 3. The variable Z in line 3 gets instantiated to lambda(x,and(H(x),x*a = Ap(X,g(X)))), and the first literal in line 3, which was -Ap(Z,w), then beta-reduces, now that Z is a lambda-term, to -and(H(w),w*a = Ap(X,g(X))). Otter-lambda renames the variables when producing a new clause, so in the following line, what was w becomes z and what was X becomes x:

21 [binary,9.1,3.2,demod,beta] $ANS(x)|Ap(x,Ap(y,r(y)))!=r(y)|$ANS(y)| -and(H(z),z*a=Ap(x,g(x))).

Now the literal containing a negated "and" is split into two literals. This is an inference rule that belongs to Otter-lambda, but not to Otter. It is activated by the set(lambda) command.

22 [split -and,21] $ANS(x)|Ap(x,Ap(y,r(y)))!=r(y)|$ANS(y)| -H(z)|z*a!=Ap(x,g(x)).

The literal -H(z) resolves with line 5, making z = g(X). The last literal in 22 then would become g(X) *a != Ap(x,g(x)). Otter-lambda tries to resolve this with the equality axiom 1, so it has to unify Ap(x,g(x)) with g(X)*a. Lambda-unification succeeds, taking x = lambda(u,u*a) and X = x. With that value of x, Ap(x,g(x)) beta-reduces to g(x)*a = g(lambda(u,u*a)) *a. So the last two literals of 22 disappear and x gets the value lambda(u,u*a). That leaves only one literal in 22 besides the answer literals, and since x has been instantiated to lambda(u,u*a), the left-hand side of that literal, namely Ap(x,Ap(y,r(y))), will now beta-reduce, becoming Ap(y,r(y))*a. As usual variables are renamed in the new clause:

25 [binary,22.3,1.1,demod,beta,unit_del,5] $ANS(lambda(x,x*a))|Ap(y,r(y))*a!=r(y)|$ANS(y).

Now, that last literal is resolved with first literal of axiom 2, the axiom for group inverse. Otter-lambda has to resolve Ap(y,r(y))*a = r(y) with u *x = v. This succeeds with the assignments u:= Ap(y,r(y)), x:= a, v:=r(y). The second literal of 2, u != v*i(x), then becomes Ap(y,r(y)) != r(y)*i(a) as seen in the next line of the proof: 27 [binary,25.1,2.1] $ANS(lambda(x,x*a))|$ANS(y)|Ap(y,r(y))!=r(y)*i(a). Using the equality axiom again, Otter-lambda unifies the two sides of this equality to reach the final contradiction, producing the map y := lambda(z,z*i(a)) as shown in the answer literal.

28 [binary,27.1,1.1] $ANS(lambda(x,x*a))|$ANS(lambda(z,z*i(a))). Since this clause contains only answer literals, it represents a contradiction, completing the proof.