metamath meta variables

Question

I'm reading https://us.metamath.org/mpeuni/mmzfcnd.html and it says

Each "axiom" in Metamath's version of ZFC set theory is not an actual axiom in the language of first-order logic but is a scheme or template that represents an infinite number of actual axioms. From the point of view of first-order logic, the setvar and wff "variables" are metavariables that range over the individual variables and wffs of the language of the actual logic.

Is there an example that can illustrate the difference between textbook ZFC formulation from Metamath ZFC formulation and Isabelle/ZFC formulation and Mizar formulation? Why is Metamath using metavariables?

Answer 1

I'm not an expert in any of Metamath, Isabelle (Isabelle/ZFC or otherwise) or Mizar, but I did some research on this topic when Hamster asked me essentially the same question a couple of days ago. So here's an attempt at an answer, to get the ball rolling.

The use of meta-variables in Metamath is the fundamental concept that enables it to verify proofs, and it is independent of the "object logic" with respect to which you want to prove theorems. So Metamath's architecture (meta-variables, substitution) is not a formulation of ZFC or any other logic. It's just a business of substituting well-formed formulae for metavariables, and applying axioms.

As Thierry Arnoux pointed out, the use of meta-variables makes it possible to define axiom schemas AKA axiom schemes.

In Isabelle, meta-variables are referred to as "schematic variables". This is a generic term, not restricted to Isabelle: https://en.wiktionary.org/wiki/schematic_variable (The Isabelle manual notes that schematic variables are called "logical variables" in Prolog.) Now, unlike in Metamath, a proof in Isabelle doesn't proceed by substitution of terms for meta-variables, so while meta-variables are available, they aren't the foundation of the system.

In Mizar, the problem of expressing axiom schemas arises as well. The approach taken in that system is to support free second-order variables, in addition to the first-order logic that the system manipulates.

Freek Wiedijk writes:

Mizar is based on first order predicate logic. However first order logic is slightly too weak to do ZF-style set theory. With first order logic ZF-style set theory needs infinitely many axioms. That’s because ZF set theory contains an axiom scheme, the axiom of replacement.

(From https://www.cs.ru.nl/~freek/mizar/mizman.pdf)

In practice these second-order variables are written as letters followed by terms in square brackets (for predicates) or parentheses (for functions).

So Mizar and Isabelle both make it possible to express axiom schemas, using schematic variables or second-order variables, respectively, whereas Metamath is entirely founded on the principle of meta-variables and substitution: that's Metamath's trick.

According to Raph Levien, the minimalistic Metamath style works out in practice to be similar to the "Little Theories" approach. https://www.researchgate.net/publication/2614291_Little_Theories That doesn't explain why Metamath's approach is powerful enough to do what it does, but maybe it sheds some light on the philosophy behind it.

Answer 2

I can make a few comments about Mizar's axiomatic set theory compared to ZFC, and give pointers to the code where it is stated.

The ZF Axioms in Mizar are contained in tarski_0 and the others (powerset and infinity) are derived from the axiom of the universe found in tarski_a. Specifically, we have:

• Extensionality :: for $X,Y$ being set st (for $x$ being object holds ($x\in X \iff x\in Y$)) holds $X = Y$

• Regularity :: for $x_{1}$ being object for $X$ being set st $x_{1}\in X$ holds exists $Y$ being set st ($Y\in X$ & (for $x_{2}$ being object holds ($x_{2}\notin X$ or $x_{2}\notin Y$)))

• Pair :: for $X,Y$ being any object exists $Z$ being a set such that for any object $a$ holds $a\in Z$ if and only if $a=X$ or $a=Y$.

• Union :: for $X$ being set exists $Z$ being set st for $x$ being object holds ($x\in Z$ iff exists $Y$ being set st ($x\in Y$ & $Y\in X$))

• Schema of Replacement :: exists $X$ being set st for $x$ being object holds ($x\in X$ iff exists $y$ being object st ($y\in F_{1}()$ & $P_{1}[y,x]$))

  provided

  for $x, y, z$ being object st $P_{1}[x,y]$ & $P_{1}[x,z]$ holds $y = z$

Remarks.

1. The axiom of regularity may look a little strange, but remember: if we have $\forall X((\exists x, P[x,X])\implies Q[X])$, then this is logically equivalent to $\forall X\forall x(P[x,X]\implies Q[X])$.
2. The axiom of separation is missing! Not so, it can actually be derived from the axiom scheme of replacement, and may be found in xboole_0 (and indeed, inspecting its proof, we find it is derived from the scheme of replacement).

The two missing ZF axioms are the axiom of infinity, and the axiom of the power set. The power set in Mizar notation is bool X for $\mathcal{P}(X)$ and is defined in ZFMISC_1:def 1, its existence follows from the Universe axiom:

• Tarski Universe Axiom :: for $N$ being set exists $M$ being set st

  ($N\in M$

  & (for $X$, $Y$ being set st $X\in M$ & $Y\subset X$ holds $Y\in M$)

  & (for $X$ being set st $X\in M$ holds exists $Z$ being set st ($Z \in M$ & (for $Y$ being set st $Y\subset X$ holds $Y\in Z$)))

  & (for $X$ being set holds ($X\not\subset M$, or $X$ and $M$ are equipotent, or $X\in M$)))

The other axioms may be derived from the axiom of the universe. It gives us the powerset exists (it's the third condition).

The generalized axiom of infinity is derived as Ordinal_1:Th32. Of course, working our way backwards, this uses Theorem ZfMisc_1:112 which depends on the axiom of the universe.

There is also the well-ordering theorem (which Wikipedia includes in the ZF axioms, but I do not believe it's actually needed --- it should be included for ZFC, though). Mizar proves this in WELLORD2:Th17.

However, this axiom of universe makes Mizar's set theory more powerful than ZFC, since it's equivalent to assuming a collection of inaccessible cardinals. It is well known that the axiom of the universe is equivalent to: For each cardinal $\kappa$, there is a strongly inaccessible cardinal $\lambda$ that is strictly larger than $\kappa$.