3. FOL algebra example

Consider the following FOL theory. The axioms specify a commutative operation (*) and a left inverse for element a. The conjecture is that a has a right inverse. Notice that the 3rd and 4th axioms have "coherent" mode declarations, so coherent form will be preserved when translating to geolog, without having to use the "preserve coherent axioms" load option. Also note that binary operators (like *) need to appear in operator notation in FOL inputs but can appear as parenthesized infix expressions in geolog. Clip the following code and save in file inverseA.fol in order to repeat the following experiments.
% inverseA.fol

axiom:fol:commutativity_of_*:
![X,Y]: *(X,Y) = *(Y,X).

axiom:fol:b_is_left_inverse_for_a:
*(b,a) = 1.

axiom:coherent:equal_is_symmetric:
![X,Y]: ( X = Y => Y = X).

axiom:coherent:equal_is_transitive:
![X,Y,Z]: ( (X = Y & Y = Z) => X= Z).

conjecture:fol:b_is_right_inverse_for_a:
?[Z]:*(a,Z) = 1.

The following snapshot captures a refutation (proof of conjecture) for this theory.

inverseA.jpg
Figure 1. Refutation for inverseA -- Controls OFF

If we hit the proof button we get the following proof.

proof.jpg
Figure 2. Proof for inverseA -- Controls OFF

The proof is extracted from the refutation tree in Figure 1. Notice that the proof discovers that b is indeed a right inverse for a.

Now let us modify the theory a little.

% inverseB.fol

axiom:fol:commutativity_of_*:
![X,Y]: *(X,Y) = *(Y,X).

axiom:fol:existence_of_left_inverses:
![X]:?[Z]:*(Z,X) = 1.

axiom:coherent:equal_is_symmetric:
![X,Y]: ( X = Y => Y = X).

axiom:coherent:equal_is_transitive:
![X,Y,Z]: ( (X = Y & Y = Z) => X= Z).

conjecture:fol:existence_of_right_inverses:
![X]:?[Z]:*(X,Z) = 1.

This theory inverseB states more generally that if left inverses exist (2nd axiom) then right inverses exist (conjecture).

Load inverseB.fol. Stepping through the inferences produces evidence that the geolog rules will generate an indefinite number of left inverses of left inverses (geolog rule 10) before using other rules involving those already created.

inverseB_1.jpg
Figure 3. Stepping through inverseB ...

Experimenting with ?.. (∃ for new version) produces the following succesful refutation. If we limit to 3 new skolem constants (minimum) we get the following refutation.

inverseB_2.jpg
Figure 3. Refutation using ?..(3)

The extracted proof is instructive. Let the reader extract the corresponding proof. Careful inspection of the proof reveals the detailed role of the 3 skolem constants.