Define the biconditional connective.

Also clean up the coverage script and include metavariables. Metamath-style definitions can only define logical constants; in order to express a variable, we must treat it as a sort of floating hole which weaves through logical structure, and this means that it is declared $f instead of $a. So, I wrote a regex to match $f and another to match $a. This definition of the biconditional is almost directly from iset.mm, and I think it's worth noting that I only prefer it because it allows for reduction of axioms. In general, I want few axioms, because I want the amount of certainty to be maximized; I'm willing to eat a few long {ganai} and {ge} and {go} in order to get there.
MostAwesomeDude · Jul 30, 2023 · 038b89d · 038b89d
1 parent 09f5025
commit 038b89d
Show file tree

Hide file tree

Showing 4 changed files with 147 additions and 64 deletions.
diff --git a/coverage.py b/coverage.py
@@ -1,9 +1,20 @@
 from collections import Counter
-import json
+import json, re
+
+VALSI = r"[\w']+"
+DF = re.compile(rf"df-({VALSI}) +\$a")
+F = re.compile(rf"\$f +{VALSI} ({VALSI})")
+
 with open("valsi-class.json") as handle: vc = json.load(handle)
-with open("mm/jbobau.mm") as handle:
-    dfs = [l.split(" ")[0][3:] for l in handle.readlines() if l.startswith("df-")]
-c = Counter(vc[v] for v in dfs)
-print("Grammatical class | # of formal definitions"); print("---|---")
-for cls in c: print(cls, "|", c[cls])
-print("total", "|", sum(c.values()))
+with open("mm/jbobau.mm") as handle: db = handle.read()
+
+dfc = Counter(vc[v] for v in DF.findall(db))
+dff = Counter(vc[v] for v in F.findall(db))
+count = sum(dfc.values()) + sum(dff.values())
+
+print("Grammatical class | Metamath class | # of formal definitions")
+print("---|---|---")
+lines = [f"{cls} | metavariable | {dff[cls]}" for cls in dff]
+lines.extend(f"{cls} | constant | {dfc[cls]}" for cls in dfc)
+for line in sorted(lines): print(line)
+print("total", "| - |", count, "%0.2f%%" % (count * 100 / 2529))
diff --git a/mm/jbobau.mm b/mm/jbobau.mm
@@ -12,6 +12,7 @@
 * inferences of {go} have same theorem name, but end with "i"
 * reverse inferences end with "ri"
 * deductions where everything starts {ganai broda gi} end with "d"
+* Operators commute, relations are symmetric
 $)
 
 $( $t
@@ -210,6 +211,52 @@
       sbb1 sbb3 mp2.0 sbb2 sbb1 sbb3 mp2.1 mp2.2 mpi ax-mp $.
 $}
 
+$(
+#*#*#
+Conjunctions I: {ge}
+#*#*#
+$)
+
+$c ge $.
+bge $a bridi ge broda gi brode $.
+
+$( Elimination of {` ge `} on the left. Known as "ax-ia1" in iset.mm. Curry
+   of the left-hand projection. $)
+ax-ge-le $a |- ganai ge broda gi brode gi broda $.
+
+$( Elimination of {` ge `} on the right. Known as "ax-ia2" in iset.mm. Curry
+   of the right-hand projection. $)
+ax-ge-re $a |- ganai ge broda gi brode gi brode $.
+
+$( Introduction of {` ge `}. Known as "ax-ia3" in iset.mm. Curry of the I
+   combinator. $)
+ax-ge-in $a |- ganai broda gi ganai brode gi ge broda gi brode $.
+
+${
+    ge-lei.0 $e |- ge broda gi brode $.
+    $( Inference form of ~ax-ge-le
+       (Contributed by la korvo, 27-Jul-2023.) $)
+    ge-lei $p |- broda $=
+      sbb1 sbb2 bge sbb1 ge-lei.0 sbb1 sbb2 ax-ge-le ax-mp $.
+$}
+
+${
+    ge-rei.0 $e |- ge broda gi brode $.
+    $( Inference form of ~ax-ge-re
+       (Contributed by la korvo, 27-Jul-2023.) $)
+    ge-rei $p |- brode $=
+      sbb1 sbb2 bge sbb2 ge-rei.0 sbb1 sbb2 ax-ge-re ax-mp $.
+$}
+
+${
+    ge-ini.0 $e |- broda $.
+    ge-ini.1 $e |- brode $.
+    $( Inference form of ~ax-ge-in
+       (Contributed by la korvo, 27-Jul-2023.) $)
+    ge-ini $p |- ge broda gi brode $=
+      sbb1 sbb2 sbb1 sbb2 bge ge-ini.0 ge-ini.1 sbb1 sbb2 ax-ge-in mp2 $.
+$}
+
 $(
 #*#*#
 Biconditionals I: {go}
@@ -221,8 +268,61 @@
 $( If {` broda `} and {` brode `} are bridi, then so is {` go broda gi brode `}. $)
 bgo $a bridi go broda gi brode $.
 
-$( {` go `} is reflexive. $)
-ax-go-refl $a |- go broda gi broda $.
+$( Definition of {` go `} in terms of {` ganai `} and {` ge `}. This is the
+   standard definition of the biconditional connective in higher-order
+   intuitionistic logic. This can be justified intuitionistically; see
+   "df-bi" and "bijust" in iset.mm. $)
+df-go $a |-
+  ge
+    ganai go broda gi brode
+    gi ge ganai broda gi brode gi ganai brode gi broda
+  gi
+    ganai ge ganai broda gi brode gi ganai brode gi broda
+    gi go broda gi brode $.
+
+${
+    goli.0 $e |- go broda gi brode $.
+    $( Inference form of left side of ~df-go
+       (Contributed by la korvo, 29-Jul-2023.) $)
+    goli $p |- ge ganai broda gi brode gi ganai brode gi broda $=
+      sbb1 sbb2 bgo sbb1 sbb2 bgan sbb2 sbb1 bgan bge goli.0 sbb1 sbb2 bgo sbb1
+      sbb2 bgan sbb2 sbb1 bgan bge bgan sbb1 sbb2 bgan sbb2 sbb1 bgan bge sbb1
+      sbb2 bgo bgan sbb1 sbb2 df-go ge-lei ax-mp $.
+$}
+
+${
+    golili.0 $e |- go broda gi brode $.
+    $( Biconditional implication may be weakened to unidirectional implication.
+       Inference form of left side of ~goli
+       (Contributed by la korvo, 17-Jul-2023.)
+       (Shortened by la korvo, 29-Jul-2023.) $)
+    golili $p |- ganai broda gi brode $=
+      sbb1 sbb2 bgan sbb2 sbb1 bgan sbb1 sbb2 golili.0 goli ge-lei $.
+$}
+
+${
+    gori.0 $e |- ge ganai broda gi brode gi ganai brode gi broda $.
+    $( Inference form of right side of ~df-go
+       (Contributed by la korvo, 30-Jul-2023.) $)
+    gori $p |- go broda gi brode $=
+      sbb1 sbb2 bgan sbb2 sbb1 bgan bge sbb1 sbb2 bgo gori.0 sbb1 sbb2 bgo sbb1
+      sbb2 bgan sbb2 sbb1 bgan bge bgan sbb1 sbb2 bgan sbb2 sbb1 bgan bge sbb1
+      sbb2 bgo bgan sbb1 sbb2 df-go ge-rei ax-mp $.
+$}
+
+${
+    gorii.0 $e |- ganai broda gi brode $.
+    gorii.1 $e |- ganai brode gi broda $.
+    $( Inference form of right side of ~gori
+       (Contributed by la korvo, 30-Jul-2023.) $)
+    gorii $p |- go broda gi brode $=
+      sbb1 sbb2 sbb1 sbb2 bgan sbb2 sbb1 bgan gorii.0 gorii.1 ge-ini gori $.
+$}
+
+$( {` go `} is reflexive.
+   (Contributed by la korvo, 30-Jul-2023.) $)
+go-refl $p |- go broda gi broda $=
+  sbb1 sbb1 sbb1 id sbb1 id gorii $.
 
 ${
     ax-go-sym.0 $e |- go broda gi brode $.
@@ -237,24 +337,13 @@
     ax-go-trans $a |- go broda gi brodi $.
 $}
 
-df-ganai $a |- ganai go broda gi brode gi ganai broda gi brode $.
-
-${
-    ganaii.0 $e |- go broda gi brode $.
-    $( Biconditional implication may be weakened to unidirectional implication.
-       Inference form of ~df-ganai
-       (Contributed by la korvo, 17-Jul-2023.) $)
-    ganaii $p |- ganai broda gi brode $=
-      sbb1 sbb2 bgo sbb1 sbb2 bgan ganaii.0 sbb1 sbb2 df-ganai ax-mp $.
-$}
-
 ${
     bi.0 $e |- broda $.
     bi.1 $e |- go broda gi brode $.
-    $( Provable version of (now removed) ax-bi, using ~ax-mp and ~df-ganai as a basis.
+    $( Like modus ponens ~ax-mp but for biconditionals.
        (Contributed by la korvo, 16-Jul-2023.) $)
     bi $p |- brode $=
-      sbb1 sbb2 bi.0 sbb1 sbb2 bi.1 ganaii ax-mp $.
+      sbb1 sbb2 bi.0 sbb1 sbb2 bi.1 golili ax-mp $.
 $}
 
 ${
@@ -271,58 +360,20 @@
     $( The right-hand side of a {` go `} may also be weakened to a {` ganai `}.
        (Contributed by la korvo, 10-Jul-2023.) $)
     bi-rev-syl $p |- ganai brode gi broda $=
-      sbb2 sbb1 sbb1 sbb2 bi-rev-syl.0 ax-go-sym ganaii $.
+      sbb2 sbb1 sbb1 sbb2 bi-rev-syl.0 ax-go-sym golili $.
 $}
 
 $(
 #*#*#
-Conjunctions: {.e}, {je}, {ge}
+Conjunctions II: {.e}, {je}
 #*#*#
 $)
 
-$c je ge $.
+$c je $.
 
 $c .e $.
 sje $a sumti ko'a .e ko'e $.
 sbje $a selbri bu'a je bu'e $.
-bge $a bridi ge broda gi brode $.
-
-$( Elimination of {` ge `} on the left. Known as "ax-ia1" in iset.mm. Curry
-   of the left-hand projection. $)
-ax-ge-le $a |- ganai ge broda gi brode gi broda $.
-
-$( Elimination of {` ge `} on the right. Known as "ax-ia2" in iset.mm. Curry
-   of the right-hand projection. $)
-ax-ge-re $a |- ganai ge broda gi brode gi brode $.
-
-$( Introduction of {` ge `}. Known as "ax-ia3" in iset.mm. Curry of the I
-   combinator. $)
-ax-ge-in $a |- ganai broda gi ganai brode gi ge broda gi brode $.
-
-${
-    ge-lei.0 $e |- ge broda gi brode $.
-    $( Inference form of ~ax-ge-le
-       (Contributed by la korvo, 27-Jul-2023.) $)
-    ge-lei $p |- broda $=
-      sbb1 sbb2 bge sbb1 ge-lei.0 sbb1 sbb2 ax-ge-le ax-mp $.
-$}
-
-${
-    ge-rei.0 $e |- ge broda gi brode $.
-    $( Inference form of ~ax-ge-re
-       (Contributed by la korvo, 27-Jul-2023.) $)
-    ge-rei $p |- brode $=
-      sbb1 sbb2 bge sbb2 ge-rei.0 sbb1 sbb2 ax-ge-re ax-mp $.
-$}
-
-${
-    ge-ini.0 $e |- broda $.
-    ge-ini.1 $e |- brode $.
-    $( Inference form of ~ax-ge-in
-       (Contributed by la korvo, 27-Jul-2023.) $)
-    ge-ini $p |- ge broda gi brode $=
-      sbb1 sbb2 sbb1 sbb2 bge ge-ini.0 ge-ini.1 sbb1 sbb2 ax-ge-in mp2 $.
-$}
 
 $( Definition of {` .e `} in terms of {` ge `}. Forethought version of
    example 12.2-5 from [CLL] p. 14. $)
@@ -544,7 +595,7 @@
     $( Biconditional modus ponens under {` ro bu'a `}.
        (Contributed by la korvo, 16-Jul-2023.) $)
     ro-bi $p |- ro bu'a zo'u brode $=
-      sbb1 sbb2 sbba ro-bi.0 sbb1 sbb2 ro-bi.1 ganaii ax-ro-mp $.
+      sbb1 sbb2 sbba ro-bi.0 sbb1 sbb2 ro-bi.1 golili ax-ro-mp $.
 $}
 
 $(

diff --git a/src/foreword.md b/src/foreword.md
@@ -47,11 +47,16 @@ selbri which did not previously exist.
 Theorem | Formalized | Proved
 ---|---|---
 cei'i | yes | yes: [ceihi](ceihi.html)
+ganai broda gi broda | yes | yes: [id](id.html)
+go broda gi broda | yes | yes: [go-refl](go-refl.html)
 ko'a du ko'a | yes | no; [du-refl](du-refl.html) is incomplete
 lo broda ku broda | somewhat (prose, not Metamath) | no
 
 ### Formal coverage
 
+Put another way, there are around 2529 baseline valsi to consider, and the
+following table shows how many valsi have been formalized.
+
 {{#include coverage.md}}
 
 ## Credits

diff --git a/valsi-class.json b/valsi-class.json
@@ -1,6 +1,14 @@
 {
+    "da": "KOhA",
+    "de": "KOhA",
+    "di": "KOhA",
+    "ko'a": "KOhA",
+    "ko'e": "KOhA",
+    "ko'i": "KOhA",
     "ga": "GA",
     "ganai": "GA",
+    "ge": "GA",
+    "go": "GA",
     "a": "A",
     "e": "A",
     "o": "A",
@@ -9,8 +17,16 @@
     "jo": "JA",
     "se": "SE",
     "te": "SE",
+    "bu'a": "GOhA",
+    "bu'e": "GOhA",
+    "bu'i": "GOhA",
     "ceihi": "GOhA",
     "du": "GOhA",
+    "broda": "gismu",
+    "brode": "gismu",
+    "brodi": "gismu",
+    "brodo": "gismu",
+    "brodu": "gismu",
     "ckaji": "gismu",
     "ckini": "gismu",
     "dugri": "gismu",