一个十分有意思的脑力锻炼小游戏（并不小）。
00:18
dousha99：
tldw: 一个游戏；首先我们定义某种数学结构，然后轮流给出一个命题
dousha99：
如果这个命题无法通过已有的公理推出，那么这个命题就作为新的公理加入
dousha99：
如果这个命题可以通过已有的公理推出，那么这个命题就是一个定理，然后给出定理的人就输了
dousha99：
那么这个就不算数，你得再想一个新的命题
Bird：
在构建的过程中，如果新的公理加入后可以推出旧的公理呢？
Bird：
那你最好能脑内渲染 TeX\TeX 公式
Bird：
啥时候微信支持 TeX\TeX 渲染了？？
00:24
dousha99：
定义集合上封闭的二元运算 ×\times 和常量 aa
dousha99：
let the game begin, you go first
Bird：
∀x,y:x×y=y×x\forall x, y: x \times y = y \times x
00:25
dousha99：
∀x:∃y:x×y=a\forall x: \exists y: x \times y = a
Bird：
∀x:x×a≠a\forall x: x \times a \neq a
00:27
dousha99：
因为 ∀x:∃y:x×y=a\forall x: \exists y: x \times y = a 所以存在一个 yy 使得 a×y=aa \times y = a
dousha99：
然后又有 ∀x,y:x×y=y×x\forall x, y: x \times y = y \times x 所以 y×a=ay \times a = a
Bird：
那就改成 ∀x:x×a=a\forall x: x \times a = a
00:29
dousha99：
好，现在我们有交换律、逆和幺元了
dousha99：
∀x,y,z:x×(y×z)=(x×y)×z\forall x, y, z: x \times (y \times z) = (x \times y) \times z
Bird：
∃u,v,w:∀x:x=u∨x=v∨x=w\exists u, v, w: \forall x: x = u \vee x = v \vee x = w
00:31
00:33
dousha99：
满足这些公理的结构只有 {1,x,x−1} \{1, x, x^{-1}\}
Bird：
所以还能再凹一个：∀x,y:x×y=x \forall x, y: x \times y = x
Bird：
这样就会让它进一步退化成 {1} \{1\}
Bird：
如果一句话就能把结构退化成 {1} \{1\} ，那就没意思了
dousha99：
或者我们可以从某个更开放的结构开始
Bird：
我觉得就我们目前的数学功底不太能支持我们这么干