From 576b713e0392a029e3b69135ce8a5b5eca75fd3b Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 08:09:04 +0530 Subject: [PATCH 1/2] Enable matching for the cancellation law so it can be used in 24.8 The inverse axiom is existential, which the matcher cannot unify. A proxy template keeps identity, associativity, and the equality, matching the pattern already used for the syllogism laws. --- docs/index.html | 2 +- docs/js/main.js | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/docs/index.html b/docs/index.html index a0319f0..6b353cc 100644 --- a/docs/index.html +++ b/docs/index.html @@ -2599,7 +2599,7 @@

This is
  • The third is inverse: for every group element X, there is a group element Y such that Y*X=1.
  • This is a relatively easy exercise in group theory when written out in informal mathematical language, but turns out to be somewhat lengthy when one tries to formalise it in first-order logic. More generally, first-order logic tends to be too "low-level" of a proof system to be convenient for advanced mathematics; most proofs in mathematics are instead written in a more "high-level" fashion, using less formal, but more expressive, sentences in English (or in other languages) in place of the very limited sentences available to first-order logic.
  • Thanks to Gesse Roure for a short proof, and Anders Kaseorg for a shorter proof.
    • -
  • Technical note: matching for this exercise has not yet been implemented.
    • +
  • Matching uses a proxy template that omits the inverse axiom (whose existential quantifier the matcher cannot yet unify), so the law can be applied in later group-theory exercises such as 24.8.
      • diff --git a/docs/js/main.js b/docs/js/main.js index 7ce63ff..39c178b 100644 --- a/docs/js/main.js +++ b/docs/js/main.js @@ -329,7 +329,8 @@ var exerciseData = { "24.1(b)": [[equals(alpha,beta), equals(beta,gamma)], equals(alpha,gamma)], "24.2": [[equals(alpha,beta)], equals(fa,fb)], "24.3": [[forAll(equals(multiply(alpha,X),X),X), forAll(equals(multiply(X,beta),X),X)], equals(alpha,beta)], - "24.4": [[forAll(equals(multiply(one,X),X),X), forAll(forAll(forAll(equals(multiply(X,multiply(Y,Z)),multiply(multiply(X,Y),Z)), Z), Y), X), forAll(thereExists(equals(multiply(Y,X),one),Y),X), equals(multiply(alpha,beta),multiply(alpha,gamma))], equals(beta,gamma)], + "24.4": [[forAll(equals(multiply(one,X),X),X), forAll(forAll(forAll(equals(multiply(X,multiply(Y,Z)),multiply(multiply(X,Y),Z)), Z), Y), X), forAll(thereExists(equals(multiply(Y,X),one),Y),X), equals(multiply(alpha,beta),multiply(alpha,gamma))], equals(beta,gamma), + [forAll(equals(multiply(one,X),X),X), forAll(forAll(forAll(equals(multiply(X,multiply(Y,Z)),multiply(multiply(X,Y),Z)), Z), Y), X), equals(multiply(alpha,beta),multiply(alpha,gamma))], equals(beta,gamma)], "24.5": [[forAll(equals(multiply(one,X),X),X), forAll(forAll(forAll(equals(multiply(X,multiply(Y,Z)),multiply(multiply(X,Y),Z)), Z), Y), X), thereExists(equals(multiply(X,alpha),one),X), thereExists(equals(multiply(X,beta),one),X)], thereExists(equals(multiply(X,multiply(alpha,beta)),one),X)], "24.6": [[forAll(equals(multiply(one,X),X),X), forAll(equals(multiply(X,one),X),X), forAll(forAll(forAll(equals(multiply(X,multiply(Y,Z)),multiply(multiply(X,Y),Z)), Z), Y), X), forAll(equals(multiply(fX,X),one),X)], forAll(equals(ffX,X),X)], "24.7": [[forAll(forAll(forAll(equals(power(power(X,Y),Z), power(X,multiply(Y,Z))),Z),Y),X), forAll(equals(multiply(sqrtX, sqrtX),X),X), forAll(equals(power(sqrtX,two),X),X), predicateSentence(R,[two]), NOT(predicateSentence(R,[sqrt2]))], thereExists(thereExists(AND(AND(NOT(RX),NOT(RY)), predicateSentence(R,[power(X,Y)])), Y), X)], From 4ccc1a7f0e638b0cb1becd2dcc27cd2ee4cbeb98 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 08:18:48 +0530 Subject: [PATCH 2/2] Note that 24.8 can now match against the cancellation law MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The previous note said matching was unimplemented; 24.4's proxy template is what 24.8 needs after deriving x*(α*1)=x*α. --- docs/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/index.html b/docs/index.html index 6b353cc..beb764c 100644 --- a/docs/index.html +++ b/docs/index.html @@ -2752,7 +2752,7 @@

      This is
    1. Thanks to Martin Epstein for suggesting this exercise.
    2. Stuck? Hover over this sentence.
    3. Thanks to Anders Kaseorg for a short proof, Martin Epstein for a shorter proof, and Anders Kaseorg for an even shorter proof.
      4. -
    4. Technical note: matching for this exercise has not yet been implemented.
      5. +
    5. Technical note: matching for the cancellation law (24.4) is now available via a proxy template, so this exercise can apply it after deriving x*(α*1) = x*α.