Here is the claimed Gorard’s “alien logic system” in the linked tweet
I had Claude chew on this for a bit, and Claude determined that this proof system was the trivial one (ie ∀a,b:a=b) by writing a script in SPASS (an automatic theorem prover) to try to prove this statement.
Here is the SPASS proof
--------------------------SPASS-START-----------------------------
Input Problem:
1[0:Inp] || equal(skc2,skc3)** -> .
2[0:Inp] || -> equal(op(op(u,v),op(v,u)),v)**.
3[0:Inp] || -> equal(op(op(u,v),v),op(v,op(v,u)))**.
4[0:Inp] || -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
This is a unit equality problem.
This is a problem that has, if any, a non-trivial domain model.
The conjecture is ground.
Axiom clauses: 3 Conjecture clauses: 1
Inferences: IEqR=1 ISpR=1 ISpL=1
Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1
Extras : Input Saturation, No Selection, No Splitting, Full Reduction, Ratio: 5, FuncWeight: 1, VarWeight: 1
Precedence: op > skc3 > skc2 > skc1 > skc0
Ordering : KBO
Processed Problem:
Worked Off Clauses:
Usable Clauses:
1[0:Inp] || equal(skc3,skc2)** -> .
2[0:Inp] || -> equal(op(op(u,v),op(v,u)),v)**.
3[0:Inp] || -> equal(op(op(u,v),v),op(v,op(v,u)))**.
4[0:Inp] || -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
Given clause: 1[0:Inp] || equal(skc3,skc2)** -> .
Given clause: 2[0:Inp] || -> equal(op(op(u,v),op(v,u)),v)**.
Given clause: 3[0:Inp] || -> equal(op(op(u,v),v),op(v,op(v,u)))**.
Given clause: 15[0:Rew:3.0,14.0,2.0,14.0] || -> equal(op(u,op(u,v)),op(v,op(v,u)))*.
Given clause: 4[0:Inp] || -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
Given clause: 11[0:SpR:3.0,2.0] || -> equal(op(op(u,op(u,v)),op(u,op(v,u))),u)**.
Given clause: 16[0:SpR:15.0,2.0] || -> equal(op(op(op(u,v),u),op(v,op(v,u))),u)**.
SPASS V 3.9
SPASS beiseite: Proof found.
Problem: collapse.dfg
SPASS derived 171 clauses, backtracked 0 clauses, performed 0 splits and kept 96 clauses.
SPASS allocated 85510 KBytes.
SPASS spent 0:00:00.08 on the problem.
0:00:00.03 for the input.
0:00:00.02 for the FLOTTER CNF translation.
0:00:00.00 for inferences.
0:00:00.00 for the backtracking.
0:00:00.01 for the reduction.
Here is a proof with depth 3, length 23 :
1[0:Inp] || equal(skc3,skc2)** -> .
2[0:Inp] || -> equal(op(op(u,v),op(v,u)),v)**.
3[0:Inp] || -> equal(op(op(u,v),v),op(v,op(v,u)))**.
4[0:Inp] || -> equal(op(op(u,op(v,w)),w),op(v,op(u,op(w,u))))*.
14[0:SpR:2.0,3.0] || -> equal(op(op(u,v),op(op(u,v),op(v,u))),op(u,op(u,v)))**.
15[0:Rew:3.0,14.0,2.0,14.0] || -> equal(op(u,op(u,v)),op(v,op(v,u)))*.
16[0:SpR:15.0,2.0] || -> equal(op(op(op(u,v),u),op(v,op(v,u))),u)**.
17[0:SpR:15.0,2.0] || -> equal(op(op(u,op(u,v)),op(op(v,u),v)),op(v,u))**.
34[0:SpR:4.0,2.0] || -> equal(op(op(u,op(v,op(w,u))),op(w,op(v,op(u,v)))),op(v,op(w,u)))**.
49[0:SpR:4.0,2.0] || -> equal(op(op(u,op(op(op(v,u),u),v)),v),u)**.
63[0:Rew:3.0,49.0] || -> equal(op(op(u,op(op(u,op(u,v)),v)),v),u)**.
128[0:SpR:16.0,3.0] || -> equal(op(op(u,op(u,v)),op(op(u,op(u,v)),op(op(v,u),v))),op(v,op(u,op(u,v))))**.
145[0:SpR:3.0,16.0] || -> equal(op(op(op(u,op(u,v)),op(v,u)),op(u,op(u,op(v,u)))),op(v,u))**.
168[0:Rew:17.0,128.0] || -> equal(op(op(u,op(u,v)),op(v,u)),op(v,op(u,op(u,v))))**.
171[0:Rew:168.0,145.0] || -> equal(op(op(u,op(v,op(v,u))),op(v,op(v,op(u,v)))),op(u,v))**.
173[0:Rew:34.0,171.0] || -> equal(op(u,op(u,v)),op(v,u))**.
174[0:Rew:173.0,15.0] || -> equal(op(u,op(u,v)),op(u,v))**.
194[0:Rew:173.0,63.0] || -> equal(op(op(u,op(op(v,u),v)),v),u)**.
209[0:Rew:173.0,174.0] || -> equal(op(u,v),op(v,u))*.
228[0:Rew:173.0,194.0,209.0,194.0,173.0,194.0,173.0,194.0,209.0,194.0] || -> equal(op(u,v),u)**.
229[0:Rew:228.0,2.0] || -> equal(op(u,v),v)**.
234[0:Rew:228.0,229.0] || -> equal(u,v)*.
235[0:UnC:234.0,1.0] || -> .
Formulae used in the proof : conjecture0 axiom1 axiom0 axiom2
--------------------------SPASS-STOP------------------------------
Here is Claude’s proof summary
Proof sketch (from SPASS, depth 3, length 23):
Axioms 1 & 2 ⟹ a ⊕ (a ⊕ b) = b ⊕ (b ⊕ a) [step 15: “symmetrized absorption”]
Substitutions into Axiom 3 + rewrites ⟹ a ⊕ (a ⊕ b) = b ⊕ a [step 173: “double apply = flip”]
(1) + (2) ⟹ a ⊕ (a ⊕ b) = a ⊕ b [step 174: idempotent-like]
(2) + (3) ⟹ a ⊕ b = b ⊕ a [step 209: commutativity]
(4) + earlier lemmas ⟹ a ⊕ b = a [step 228: left absorption]
Rewrite Axiom 2 with (5) ⟹ a ⊕ b = b [step 229: right absorption]
(5) + (6) ⟹ a = b ∀ a,b ∎
Therefore I think its quite likely that many of the supposedly rich alien axiom systems Gorard found are actually just trivial almost-contradictory systems which are hard to prove the triviality of. It also explains why he couldn’t “make sense” of the system. There is nothing to make sense of.
Here is the claimed Gorard’s “alien logic system” in the linked tweet
I had Claude chew on this for a bit, and Claude determined that this proof system was the trivial one (ie ∀a,b:a=b) by writing a script in SPASS (an automatic theorem prover) to try to prove this statement.
Here is the SPASS proof
Here is Claude’s proof summary
Proof sketch (from SPASS, depth 3, length 23):
Axioms 1 & 2 ⟹ a ⊕ (a ⊕ b) = b ⊕ (b ⊕ a) [step 15: “symmetrized absorption”]
Substitutions into Axiom 3 + rewrites ⟹ a ⊕ (a ⊕ b) = b ⊕ a [step 173: “double apply = flip”]
(1) + (2) ⟹ a ⊕ (a ⊕ b) = a ⊕ b [step 174: idempotent-like]
(2) + (3) ⟹ a ⊕ b = b ⊕ a [step 209: commutativity]
(4) + earlier lemmas ⟹ a ⊕ b = a [step 228: left absorption]
Rewrite Axiom 2 with (5) ⟹ a ⊕ b = b [step 229: right absorption]
(5) + (6) ⟹ a = b ∀ a,b ∎
Therefore I think its quite likely that many of the supposedly rich alien axiom systems Gorard found are actually just trivial almost-contradictory systems which are hard to prove the triviality of. It also explains why he couldn’t “make sense” of the system. There is nothing to make sense of.