#metamath — Public Fediverse posts on home.social

Richard Penner @[email protected] · 2026-07-21 · 16:43 UTC

Still working on ways to do and illustrate #CondensedDetachment but I have taken a detour in performance enhancing my Rust port of the #Metamath proof assistance and theorem verification tool.

#metamath #condenseddetachment

Richard Penner @[email protected] · 2026-07-21 · 16:43 UTC

Still working on ways to do and illustrate #CondensedDetachment but I have taken a detour in performance enhancing my Rust port of the #Metamath proof assistance and theorem verification tool.

#metamath #condenseddetachment

Richard Penner @[email protected] · 2026-06-08 · 05:44 UTC

Since 2026/05/11 I have been massaging the output of #c2rust run on the #metamath source code into increasingly idiomatic #Rust. Right now verification of large databases of theorems runs in about 80% of the time of the C binary but I'm haven't yet converted all the IO away from stdio routines which want NUL-terminated CStrings (and the super unsafe *const u8). I've stripped out the idiosyncratic private memory management in favor of pre-allocating vectors and string buffers which is an improvement in performance and maintaining my sanity.

#rust #metamath #c2rust

Richard Penner @[email protected] · 2026-06-08 · 05:44 UTC

Since 2026/05/11 I have been massaging the output of #c2rust run on the #metamath source code into increasingly idiomatic #Rust. Right now verification of large databases of theorems runs in about 80% of the time of the C binary but I'm haven't yet converted all the IO away from stdio routines which want NUL-terminated CStrings (and the super unsafe *const u8). I've stripped out the idiosyncratic private memory management in favor of pre-allocating vectors and string buffers which is an improvement in performance and maintaining my sanity.

#rust #metamath #c2rust

Richard Penner @[email protected] · 2026-04-27 · 06:36 UTC

Notation guide (adapted from Metamath):

• 𝜑, a metavariable standing for any logical formula, abbreviates the conjunction of all hypotheses listed for a given proposition; writing each line as ⊢ (𝜑 → …) puts the theorem in "deduction form," which can be easier to apply in #Metamath.

• ⊢ 𝜑 asserts that 𝜑 is true; the turnstile is descended from #Frege's own Urteilsstrich (judgment stroke).

• 𝐴𝑅𝐵 means the ordered pair ⟨𝐴, 𝐵⟩ is an element of 𝑅, or we could say 𝐵 immediately follows 𝐴

• 𝐵 = (𝑅‘𝐴) means 𝐵 is the unique set such that 𝐴𝑅𝐵 is true (when such a 𝐵 exists) which means 𝑅 is function-like when restricted to operating on the singleton {𝐴}

• (𝑅”𝐴) is the image of 𝐴

• dom 𝑅 is the domain of 𝑅, the class of all sets 𝑥 such that there is a set 𝑦 that would make 𝑥𝑅𝑦 true.

• Fun 𝑅 is true when 𝑅 is function-like for all sets in its domain.

• ◡𝑅 is the converse of 𝑅 so 𝐴◡𝑅𝐵 iff 𝐵𝑅𝐴

• (tc‘𝑅) is the #TransitiveClosure of 𝑅 (Metamath uses (t+‘𝑅) which can be awkward.) Whitehead and Russell use the term ancestral to describe how 𝐴(tc‘𝑅)𝐵 means 𝐴 is some “ancestor” of 𝐵. Alternately, we can say 𝐵 eventually follows 𝐴.

• V is the universal class, every set is a member, and only sets may be members of any class. After Frege’s later work ran into Russell’s Paradox, it was discovered that not every class {𝑥 | 𝜑} makes sense as a set and so we need the hypothesis ⊢ (𝜑 → 𝐴 ∈ V) before we can talk about the function value of 𝐴 or the ordered pair ⟨𝐴, 𝐵⟩ being an element of 𝑅. V is not italic because it is a constant symbol, like tc, dom, and Fun.

#transitiveclosure #frege #metamath

Richard Penner @[email protected] · 2026-04-27 · 06:33 UTC

Begriffsschrift (1879), is one of the first manuscripts on #SymbolicLogic. As such, it literally invents a new language to describe the subjects the author, #GottlobFrege, wants to introduce. And this notation is very unlike what we see in math before or after this.

So I will list some theorems adapted (by me, circa 2020) from #Frege with proper set-theoretical bounds.

#SetTheory #Logic #Metamath

#metamath #logic #settheory #frege #gottlobfrege #symboliclogic

Corbin @[email protected] · 2026-04-05 · 15:37 UTC

So, just double-checking how #Lean4 and #Mathlib work:

* Lean takes 3GiB of RAM and a minute to open Mathlib
* Lean requires about 10min to build itself in CI, only verifying required theorems
* Verifying all of Mathlib is measured in hours
* Lean's kernel is untrustworthy due to junk theorems

And yet I'm a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.

#mathlib #metamath #lean4

Richard Penner @[email protected] · 2026-02-20 · 14:22 UTC

Every well-ordered set is isomorphic to an ordinal. Common notion, for example see Introduction to https://arxiv.org/abs/2409.07352

⊢((𝐴∈V∧𝑅We𝐴)↔∃𝑓(dom𝑓∈On∧𝑓IsomE,𝑅(dom𝑓,𝐴)))

\[ \vdash ( ( A \in \mathrm{V} \wedge R \mathrm{We} A ) \leftrightarrow \exists f ( \mathrm{dom} f \in \mathrm{On} \wedge f \mathrm{Isom} \mathrm{E} , R ( \mathrm{dom} f , A ) ) ) \]

Every well-ordered set is isomorphic to
a unique ordinal.

⊢((𝐴∈V∧𝑅We𝐴)↔∃!𝑜∈On∃𝑓∈(𝐴↑ₘ𝑜)𝑓IsomE,𝑅(𝑜,𝐴))

\[ \vdash ( ( A \in \mathrm{V} \wedge R \mathrm{We} A ) \leftrightarrow \exists{!} o \in \mathrm{On} \exists f \in ( A \uparrow_\mathrm{m} o ) f \mathrm{Isom} \mathrm{E} , R ( o , A ) ) \]

We can phrase the Axiom of Choice as "Every set injects into an ordinal."

⊢(CHOICE↔∀𝑥∃𝑜∈On𝑥≼𝑜)

\[ \vdash ( \mathrm{CHOICE} \leftrightarrow \forall x \exists o \in \mathrm{On} x \preccurlyeq o ) \]

#math #metamath #SetTheory #WellOrdering #OrdinalNumbers

#ordinalnumbers #wellordering #settheory #metamath #math

Richard Penner @[email protected] · 2026-02-17 · 08:52 UTC

@FishFace Update:

What I refer to as EScbO is usually called #LO the #LinearOrdering principle.

⊢ ∃y ∀a ∈ x ∀b ∈ x ∀c ∈ x (¬ aya ∧ ((ayb ∧ byc) → ayc) ∧ (ayb ∨ a = b ∨ bya))
or using abbreviations in #Metamath
⊢ ∃y y Or x

I think AC implies LO, but LO is independent of DC and CC.

#metamath #linearordering #lo

Richard Penner @[email protected] · 2026-02-16 · 11:52 UTC

So we have { 1, 2 } ∈ Fin₁ ⊆ Fin₁ₐ ⊆ Fin₂ ⊆ Fin₃ ⊆ Fin₄ ⊆ Fin₅ ⊆ Fin₆ ⊆ Fin₇

If a set is in Fin₁ then it is considered finite by all the other definitions.

But since the axiom of choice is equivalent to saying every set can be well-ordered, if we accept it VII-finite sets are equinumerous with a finite ordinal and so Fin₇ ⊆ Fin₁ and so the differences between these definitions collapse and ZF becomes ZFC, which is a widely accepted basis for Set Theory.

My consultation with math resources was inspired by a blog post:

https://www.infinitelymore.xyz/p/what-is-the-infinite

#Metamath #ZFC #SetTheory #AxiomOfChoice #FiniteSet #Infinity

#infinity #finiteset #axiomofchoice #settheory #zfc #metamath

Richard Penner @[email protected] · 2026-02-16 · 11:52 UTC

So we have { 1, 2 } ∈ Fin₁ ⊆ Fin₁ₐ ⊆ Fin₂ ⊆ Fin₃ ⊆ Fin₄ ⊆ Fin₅ ⊆ Fin₆ ⊆ Fin₇

If a set is in Fin₁ then it is considered finite by all the other definitions.

But since the axiom of choice is equivalent to saying every set can be well-ordered, if we accept it VII-finite sets are equinumerous with a finite ordinal and so Fin₇ ⊆ Fin₁ and so the differences between these definitions collapse and ZF becomes ZFC, which is a widely accepted basis for Set Theory.

My consultation with math resources was inspired by a blog post:

https://www.infinitelymore.xyz/p/what-is-the-infinite

#Metamath #ZFC #SetTheory #AxiomOfChoice #FiniteSet #Infinity

#infinity #finiteset #axiomofchoice #settheory #zfc #metamath

Richard Penner @[email protected] · 2026-02-16 · 11:43 UTC

Also from #Metamath I learned #infinity is hard to think about.

A . Lévy in "The independence of various definitions of finiteness" Fundamenta Mathematicae, 46:1-13 (1958) established 8 distinct set-theoretic definitions of a #finiteSet which in ZF cannot be equated without the #AxiomOfChoice

I-finite -- equinumerous with a finite ordinal. // i.e. admits a finite well-order (Numerically Finite) ⟺ the powerset of its powerset is Dedekind finite ⟺ every collection of its subsets has a maximum element ⟺ every collection of subsets has a minimal element

Ia-finite -- not the union of two sets which are not I-finite

II-finite -- every possible way of finding within the set a chain of nested subsets always contains a maximum element (Tarski finite) ⟺ equivalently every such chain contains its intersection ⟺ (Linearly Finite) ⟺ (Stäckel Finite)

|||-finite -- It's powerset is |V-finite finite, (weakly Dedekind finite) ⟺ cannot be mapped onto ordinal ω ⟺ doesn't contain a chain of subsets which can be placed in order with ω

|V-finite -- doesn't have a proper subset which is equinumerous to itself. (Dedekind finite) ⟺ there is no 1-1 map from ordinal ω to it ⟺ it is strictly dominated by the disjoint sum of it and a singleton (acts finite under successor)

V-finite -- it is either empty or strictly dominated by the disjoint sum of it with itself (acts finite under addition)

VI-finite -- it is either empty, a singleton or strictly dominated by the Cartesian product of it with itself (acts finite under multiplication)

VII-finite -- it cannot be infinitely well-ordered (not equiinumerous with the ordinal ω or any larger ordinal)

#axiomofchoice #finiteset #infinity #metamath