How to encode first-order logic without equality in Metamath

[Brian Nguyen]

Metamath uses disjoint variables instead of proper substitution as a primitive notion, and as stated in the Metamath book, "substitution and equality are intimately tied to each other" in Tarski's system for first-order logic with equality. The book also claims that "the traditional approach is also possible", so how do I encode traditional first-order logic without equality in Metamath? I tried something like this (added to set.mm):

$c NFQ $.

$v S S_1 S_2 v $.

${

$f setvar v $.

$f wff S $.

$a wff NFQ v S $.

$d v S $.

$a |- NFQ v S $.

$}

${

$f setvar v $.

$f wff S_1 S S_2 $.

$f |- NFQ v S $.

$d v S_1 $.

$d v S_2 $.

$a |- NFQ x S_1 S S_2 $.

$}

but this doesn't work because Metamath requires every variable to have a typecode. There are many other stupid restrictions in Metamath, for example that the typecode of variables are global, that label tokens may not collide with math symbol tokens, or that dummy disjoint variable restrictions are required. How do I encode the traditional notion of free variables and proper substitution in Metamath? And why do these useless restrictions exist even though they have nothing to do with proof validity?

[Norman Megill]

Tarski's paper "A Simplified Formalization of Predicate Logic with Identity" shows how to do this on p. 78, last 2 paragraphs.

Essentially he assumes that there is at least one binary predicate (say e.) and defines a pseudo-equality x ~ y as A. z ( ( x e. z <-> y e. z ) /\ ( z e. x <-> z e. y ) ).  He then adds additional axioms for x ~ y, see paper for details.

A link to the paper is provided in the Tarski entry of the bibliography at
http://us.metamath.org/mpeuni/mmset.html#bib

Disclaimer:  I haven't pursued this any further than what is stated in Tarski's paper.

Norm

[Brian Nguyen]

Tarski's paper "A Simplified Formalization of Predicate Logic with Identity" shows how to do this on p. 78, last 2 paragraphs.

Essentially he assumes that there is at least one binary predicate (say e.) and defines a pseudo-equality x ~ y as A. z ( ( x e. z <-> y e. z ) /\ ( z e. x <-> z e. y ) ).  He then adds additional axioms for x ~ y, see paper for details.

A link to the paper is provided in the Tarski entry of the bibliography at
http://us.metamath.org/mpeuni/mmset.html#bib

Disclaimer:  I haven't pursued this any further than what is stated in Tarski's paper.

Norm

Which doesn't solve the actual problem: encoding exactly traditional first-order logic without equality in Metamath. Whether it is a "conservative extension" does not matter. Is it possible to encode traditional first-order logic without equality with no additional symbols in Metamath?

[Norman Megill]

It seems you are asking several things, let's back up a little.

It might help if you explain a little more what your application is, and why equality is not desirable, since you have to go through some hoops to eliminate it and still have a complete FOL.  In most systems of practical interest, you're going to be adding in equality axioms anyway, so usually there's no reason not to include it from the start.

But aside from that, with or without equality, if you are asking for a system that has primitive notions of free variable and proper substitution exactly as stated in textbooks, it can be done in Metamath with a significantly more complex foundation (discussed in the Google Group thread I'm linking to below) that offers no advantages.  These notions are usually stated informally in English as side conditions in textbooks and accompanied in the text with verbal descriptions of the algorithms to check that a variable is free etc.

Tarski's paper I mentioned, on pp. 63-67, shows how to formalize these informal notions of the traditional system.  Their significant complexity, when formalized, led him to the simplified system that we use.

Keep in mind that both our (Tarski's) and the traditional system are expressed with axiom schemes.  Each scheme represents (can be instantiated with) an infinite number of actual axioms (the object language).  The important thing is that both Tarski's system and the traditional system generate exactly the same set of object language axioms.  This is discussed here, which also shows the traditional schemes and how we can approximate them in in Tarski's system:

http://us.metamath.org/mpeuni/mmset.html#traditional

As for understanding axiom schemes vs. the object language axioms, this might be helpful:

http://us.metamath.org/mpeuni/mmset.html#axiomnote

The 2017 thread starting below is somewhat long, but I think it addresses some of the things you are asking and might be worth reading or at least skimming through in its entirety:

"learning formal logic, feature request"
https://groups.google.com/d/msg/metamath/hOo18rTwUBM/dASE79_qAAAJ

---

As for the language restrictions you mention:

> the typecode of variables are global

This was recently added to the spec at the request of Mario Carneiro I believe, but I can't locate the message right now, perhaps he can refresh my memory.  All of our databases did that anyway so it had no effect on any existing work.

> label tokens may not collide with math symbol tokens

I agree this is somewhat silly, but at least one and perhaps two writers of early verifiers requested this because they used a single name space to make parsing faster or something.  It seems relatively harmless since a violation can be detected and fixed instantly.  If in the future there is a pressing need not to have it, the requirement can always be dropped (at the expense of those verifiers), but once dropped we can never go back without possibly having to fix multiple databases.

> dummy disjoint variable restrictions are required

This has been debated off and on and is discussed here:

http://us.metamath.org/mpeuni/mmset.html#dvnote2

Essentially it simplifies the language slightly and makes it more transparent (no hidden implicit distinct variables).

Norm

[Mario Carneiro]

On Sun, Oct 20, 2019 at 1:31 PM Brian Nguyen <musicde...@gmail.com> wrote:

Metamath uses disjoint variables instead of proper substitution as a primitive notion, and as stated in the Metamath book, "substitution and equality are intimately tied to each other" in Tarski's system for first-order logic with equality. The book also claims that "the traditional approach is also possible", so how do I encode traditional first-order logic without equality in Metamath? I tried something like this (added to set.mm):

$c NFQ $.

$v S S_1 S_2 v $.

${

$f setvar v $.

$f wff S $.

$a wff NFQ v S $.

$d v S $.

$a |- NFQ v S $.

$}

${

$f setvar v $.

$f wff S_1 S S_2 $.

$f |- NFQ v S $.

$d v S_1 $.

$d v S_2 $.

$a |- NFQ x S_1 S S_2 $.

$}

but this doesn't work because Metamath requires every variable to have a typecode.

It doesn't really make sense for a variable to not have a typecode, as that defines what the variable is supposed to range over. FOL has two types, "setvar" and "wff", (or just "var" and "wff" in this case), denoting variables that range over the universe of discourse, and well formed formulas containing those variables.

The issue with your example, aside from the lack of labels on $f/$a statements, is that $f |- NFQ v S $. should be a $e statement, because it is a logical hypothesis, not a variable declaration. Moreover, $a |- NFQ x S_1 S S_2 $. doesn't make sense because "S_1 S S_2" is not a wff (it is the concatenation of three wffs). You write $f wff S_1 S S_2 $. but I don't know what this is supposed to mean. If you intend for the concatenation of three wffs to be a wff, then this would be written $a wff S_1 S S_2 $. instead, but I don't know what operation this is intended to denote, and this isn't likely to achieve the goal because it's ambiguous.

What I'm trying to say is that the syntax errors make it difficult to guess what you are trying to express here. That's not your fault, but perhaps it might be more fruitful if you express yourself using words instead (or symbols in a more familiar notation).

 

There are many other stupid restrictions in Metamath, for example that the typecode of variables are global, that label tokens may not collide with math symbol tokens, or that dummy disjoint variable restrictions are required. ... And why do these useless restrictions exist even though they have nothing to do with proof validity?

These are all there to make verification, automated processing, and similar actions simpler. None of them affect expressivity, and when faced with the choice between simplicity of the language and ergonomics for theorem writers, metamath comes solidly on the side of simplicity. This is not a choice that everyone is willing to make, but it makes Metamath rather unique in the space of theorem provers. (You could also put mandatory spaces and one letter keywords in this category.)

 

How do I encode the traditional notion of free variables and proper substitution in Metamath?

...

Which doesn't solve the actual problem: encoding exactly traditional first-order logic without equality in Metamath. Whether it is a "conservative extension" does not matter. Is it possible to encode traditional first-order logic without equality with no additional symbols in Metamath?

Not "with no additional symbols", because you at least need symbols to represent the functions and judgments that encode proper substitution and not-free checking. This question is related to a recent thread on github: https://github.com/metamath/set.mm/issues/1183 , so you can get some additional reading, but I will try to answer your exact question here.

In order to encode *exactly* traditional FOL without equality, we first need a definition of what that is. I will suppose for now that there is one non-logical relation, but to make it clear that this doesn't have to be set theory I will use the notation "R x y" for it. I will use https://people.math.ethz.ch/~halorenz/4students/LogikML/Nutshell.pdf as the guide for the quantifier axioms, although they have a silly number of propositional axioms so I will use the Lukasiewicz axioms instead.

Every rule in metamath acts like a pattern, that does a syntactic match and does a local manipulation. All recursive functions can be recast as axiomatic judgments with clauses given by axioms, so we will do that here for the relations of "substitution" and "not-free". Besides that, we only need the core judgments of FOL: provability, with the types "var" and "wff" giving us the necessary syntactic classes.

$( "silly boilerplate" section $)
$c var term wff |- -> ( ) -. A. F/ subst substT = / $.
$v x $. vx $f var x $. $( x denotes a variable. $)
$v y $. vy $f var y $. $( y denotes a variable. $)
$v ph $. wph $f wff ph $. $( ph denotes a wff. $)
$v ps $. wps $f wff ps $. $( ps denotes a wff. $)
$v ch $. wch $f wff ch $. $( ch denotes a wff. $)
$v th $. wth $f wff th $. $( th denotes a wff. $)

$( I assume the Lukasiewicz axioms for propositional logic are non-controversial. $)
wi $a wff ( ph -> ps ) $.
wn $a wff -. ph $.
ax-1 $a |- ( ph -> ( ps -> ph ) ) $.
ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $.
ax-3 $a |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) $.
${
  ax-mp.1 $e |- ( ph -> ps ) $.
  ax-mp.2 $e |- ph $.
  ax-mp $a |- ps $.
$}

wal $a wff A. x ph $. $( forall is a wff if x is a variable and ph is a wff $)

$( A and B denote terms. Since there are no function symbols,
  this is a bit silly since terms are the same as variables, but this is how
  FOL does it and it makes it clearer how to extend the language, so
  let's stick with the distinction. $)
$v A $. tA $f term A $.
$v B $. tB $f term B $.
$v C $. tC $f term C $.
$v D $. tD $f term D $.
$v E $. tE $f term E $.

tv $a term x $. $( A variable is a term. $)

$( We will use the judgments

    substT B ( x / A ) = C
    subst ph ( x / A ) = ps

  to denote that the substitution is admissible, and the result of substituting x
  for A in ph is ps. Almost all the notation here is superfluous; the real content
  is the typecodes substT and subst that indicate the new judgments. In particular,
  despite the use of an equality sign, this defines no relation called equality,
  indeed no new wffs at all, just a new judgment. In a more traditional database we
  would probably define these as new wffs, so that we could write |- B ( x / A ) = C
  instead, but I want to keep everything clean and separate here, so that we get
  "exactly traditional first-order logic without equality in Metamath". $)
$( Metamath doesn't require that you declare these in advance, so there is nothing
  to write here. $)

$( Substitution on terms is trivial: $)
sbcv1 $a substT x ( x / A ) = A $. $( substitution when the variable matches $)
${
  $d x y $.
  $( substitution when the variable doesn't match $)
  sbcv $a substT y ( x / A ) = y $.
$}

${
  $( Substitution into a negation $)
  sbn.1 $a subst ph ( x / A ) = ps $.
  sbn $a subst -. ph ( x / A ) = -. ps $.
$}

${
  $( Substitution into an implication $)
  sbim.1 $a subst ph ( x / A ) = ch $.
  sbim.2 $a subst ps ( x / A ) = th $.
  sbim $a subst ( ph -> ps ) ( x / A ) = ( ch -> th ) $.
$}

$( Substitution into a forall that binds the variable. $)
sbal1 $a subst A. x ph ( x / A ) = A. x ph $.

${
  $d x y $. $d y A $.
  $( Substitution into a forall that doesn't bind the variable.
    For the substitution to be admissible, A must not contain
    any occurrences of y, that is, they are disjoint variables. $)
  sbal.1 $e subst ph ( x / A ) = ps $.
  sbal $a subst A. y ph ( x / A ) = A. y ps $.
$}

$( Similarly, we need to define the judgment x e/ free(ph), that is,
  x is not a free variable in ph. You might wonder why we are negating
  the judgment here, and the reason is because it has a natural inductive
  characterization, and also this is the polarity we actually need for
  axiom L12. We notate it by F/ x ph by analogy to set.mm, but again,
  this is not a wff, so it does not enlarge the collection of wffs with
  these auxiliary meta-predicates.

  We could declare not-free for terms as well, but in FOL terms never have
  binders in them, so not-free and disjoint coincide. Therefore we can
  save some trouble and use $d instead. $)

${
  $( Not free for a negation $)
  nfn.1 $e F/ x ph $.
  nfn $a F/ x -. ph $.
$}

${
  $( Not free for an implication $)
  nfim.1 $e F/ x ph $.
  nfim.2 $e F/ x ps $.
  nfim $a F/ x ( ph -> ps ) $.
$}

$( Not free for a forall when the variables match $)
nfal1 $a F/ x A. x ph $.

${
  $d x y $.
  $( Not free for a forall when the variables don't match $)
  nfal.1 $e F/ x ph $.
  nfal $a F/ x A. y ph $.
$}

${
  $( Axiom L10: A. x ph(x) -> ph(x/A), if ph(x/A) is admissible. $)
  ax-L10.1 $e subst ph ( x / A ) = ps $.
  ax-L10 $a |- ( A. x ph -> ps ) $.
$}

${
  $( Axiom L12: A. x (ps -> ph(x)) -> (ps -> A. x ph(x)), if x is not free in ps $)
  ax-L12.1 $e F/ x ps $.
  ax-L12 $a |- ( A. x ( ps -> ph ) -> ( ps -> A. x ph ) ) $.
$}

$( We're done! Let's show how to add a relation symbol and a function symbol to this: $)

$c R , $.
$( The relation R(A, B) applied to two terms is a wff.
  This is using a lot of superfluous notation; A R B or R A B would both work as well. $)
wr $a wff R ( A , B ) $.

${
  $d x A $. $d x B $.
  $( The inductive definition for NF needs a new case for R.  Note that we wouldn't
    normally need this theorem, if we had the equivalent of ax-16, but again I'm
    sticking to the classical rules, not the admissible extensions to that
    that are natural for Metamath. $)
  nfr $a F/ x R ( A , B ) $.
$}

${
  $( The inductive definition for substitution also needs a new case. $)
  sbr.1 $e substT B ( x / A ) = D $.
  sbr.2 $e substT C ( x / A ) = E $.
  sbr $a subst R ( B , C ) ( x / A ) = R ( D , E ) $.
$}

$c f $.
$( The expression f(A) is a term if A is. $)
tf $a wff f ( A ) $.

$( NF doesn't need a new case because this is a term and $d can handle NF for terms. $)

${
  $( Substitution into f(B). $)
  sbf.1 $e substT B ( x / A ) = C $.
  sbf $a substT f ( B ) ( x / A ) = R ( C ) $.
$}

Mario

[Brian Nguyen]

It seems you are asking several things, let's back up a little.

It might help if you explain a little more what your application is, and why equality is not desirable, since you have to go through some hoops to eliminate it and still have a complete FOL.  In most systems of practical interest, you're going to be adding in equality axioms anyway, so usually there's no reason not to include it from the start.

But aside from that, with or without equality, if you are asking for a system that has primitive notions of free variable and proper substitution exactly as stated in textbooks, it can be done in Metamath with a significantly more complex foundation (discussed in the Google Group thread I'm linking to below) that offers no advantages.  These notions are usually stated informally in English as side conditions in textbooks and accompanied in the text with verbal descriptions of the algorithms to check that a variable is free etc.

Tarski's paper I mentioned, on pp. 63-67, shows how to formalize these informal notions of the traditional system.  Their significant complexity, when formalized, led him to the simplified system that we use.

Keep in mind that both our (Tarski's) and the traditional system are expressed with axiom schemes.  Each scheme represents (can be instantiated with) an infinite number of actual axioms (the object language).  The important thing is that both Tarski's system and the traditional system generate exactly the same set of object language axioms.  This is discussed here, which also shows the traditional schemes and how we can approximate them in in Tarski's system:

http://us.metamath.org/mpeuni/mmset.html#traditional

As for understanding axiom schemes vs. the object language axioms, this might be helpful:

http://us.metamath.org/mpeuni/mmset.html#axiomnote

The 2017 thread starting below is somewhat long, but I think it addresses some of the things you are asking and might be worth reading or at least skimming through in its entirety:

"learning formal logic, feature request"
https://groups.google.com/d/msg/metamath/hOo18rTwUBM/dASE79_qAAAJ

---

As for the language restrictions you mention:

> the typecode of variables are global

This was recently added to the spec at the request of Mario Carneiro I believe, but I can't locate the message right now, perhaps he can refresh my memory.  All of our databases did that anyway so it had no effect on any existing work.

> label tokens may not collide with math symbol tokens

I agree this is somewhat silly, but at least one and perhaps two writers of early verifiers requested this because they used a single name space to make parsing faster or something.  It seems relatively harmless since a violation can be detected and fixed instantly.  If in the future there is a pressing need not to have it, the requirement can always be dropped (at the expense of those verifiers), but once dropped we can never go back without possibly having to fix multiple databases.

> dummy disjoint variable restrictions are required

This has been debated off and on and is discussed here:

http://us.metamath.org/mpeuni/mmset.html#dvnote2

Essentially it simplifies the language slightly and makes it more transparent (no hidden implicit distinct variables).

Norm

As far as I can tell, the Metamath language has been restricted more and more over time: first "mandatory spaces between tokens", then in 2006 (according to the book) "math symbols and statement labels share namespace", and then "variable types are global" (a restriction I've never seen in any other computer language). Even C#, which disallows variable shadowing, doesn't have this. I believe that although the first restriction simplified the language greatly (by not special casing certain characters and tokens), the later restrictions complicate both the machine side (verifier development) and the human side (inputting axioms and theorems) of Metamath.

• Without the namespace restriction I could manage statements and math symbols with two list variables. With the restriction I must either check that the two namespaces do not intersect or use one list for both and annotating whether an identifier refers to a symbol or a proposition. It is supposedly added to make writing certain parsers easier, but in my opinion some other parsers are more complicated.
• The "variable types are global" restriction is outright silly. The purpose of variable scoping is to declare that variables with the same name in different scopes are different variables. This also requires verifiers keep track of local variable scope and global variable types at the same time. Isn't it stupid? This also wreaks havoc with included files, which may declare common variable names with unrelated types, a problem exacerbated by the lack of a real module/namespace system.
• The implicit disjoint variable restriction is even worse. The Metamath program developed by Norman Megill in C clearly has the ability to determine which variables are dummy. Also, "implicit" distinct variables don't even exist because they don't matter to users of the theorem (after all, you can reprove the theorem under a different name without the redundant disjoint restrictions with a short proof referencing the original theorem).

Even if we assume that these restrictions make writing tools simple, the simplest solution is no code, no computer, no automation at all and letting people write and verify proofs in the informal style, which defeats the entire point of Metamath. Also repeatedly making backwards incompatible changes to a program for no good reason and without a conversion/migration tool is poor practice. We will never know how many private databases were, are and will be broken by the introduction of the restrictions.

Anyway, I was trying to axiomatize the not-free predicate as follows: If a variable x does not occur in an expression S then x is not free in S. If S is a quantifier expression (of the form forall x: P, exists x: P, et cetera) then x, being quantified over is not free. If S1, S2 are arbitrary sequences of symbols, neither contains x, S is an expression in which x is not free and the sequence S1 S S2 is an expression then x is not free in S1 S S2.

[Mario Carneiro]

On Mon, Oct 21, 2019 at 12:37 PM Brian Nguyen <musicde...@gmail.com> wrote:

As far as I can tell, the Metamath language has been restricted more and more over time: first "mandatory spaces between tokens", then in 2006 (according to the book) "math symbols and statement labels share namespace", and then "variable types are global" (a restriction I've never seen in any other computer language). Even C#, which disallows variable shadowing, doesn't have this.

This is a rather bizarre comparison. Have you seen the spec of C#? I haven't, but I'm pretty sure it doesn't fit on 2 pages.

 

I believe that although the first restriction simplified the language greatly (by not special casing certain characters and tokens), the later restrictions complicate both the machine side (verifier development) and the human side (inputting axioms and theorems) of Metamath.

• Without the namespace restriction I could manage statements and math symbols with two list variables. With the restriction I must either check that the two namespaces do not intersect or use one list for both and annotating whether an identifier refers to a symbol or a proposition. It is supposedly added to make writing certain parsers easier, but in my opinion some other parsers are more complicated.

Or you store them in separate lists and call it a day. You have the *option* to store them in the same list but you don't have to.

• The "variable types are global" restriction is outright silly. The purpose of variable scoping is to declare that variables with the same name in different scopes are different variables. This also requires verifiers keep track of local variable scope and global variable types at the same time. Isn't it stupid? This also wreaks havoc with included files, which may declare common variable names with unrelated types, a problem exacerbated by the lack of a real module/namespace system.

It makes variable tracking easy: You just ignore scopes entirely, and allow redefinition of variables. Actually, I would prefer that we go all the way and just make variables completely top level and global. There is no loss of expressivity, and local variables in Metamath are clunky at best. (Why do you have to name the variable hypotheses?) I think that to have proper handling of local variables in metamath would require a new language.

The restriction was only added as a way to acknowledge existing practice. set.mm and all the other major mm databases have had almost entirely only global variables for years, with exceptions only for things like introducing a variable before the typecode is properly defined.

• The implicit disjoint variable restriction is even worse. The Metamath program developed by Norman Megill in C clearly has the ability to determine which variables are dummy. Also, "implicit" distinct variables don't even exist because they don't matter to users of the theorem (after all, you can reprove the theorem under a different name without the redundant disjoint restrictions with a short proof referencing the original theorem).

This is a deliberate aesthetic choice on Norm's part. It is being more explicit about what you mean.

 

Even if we assume that these restrictions make writing tools simple, the simplest solution is no code, no computer, no automation at all and letting people write and verify proofs in the informal style, which defeats the entire point of Metamath.

This is a straw man. Metamath is entirely the opposite of this: it is an *extremely explicit* style of writing proofs that is optimized for easy verification.

 

Also repeatedly making backwards incompatible changes to a program for no good reason and without a conversion/migration tool is poor practice. We will never know how many private databases were, are and will be broken by the introduction of the restrictions.

We'll never know (or care) unless they tell us. As far as I can tell this has broken no one's code.

Anyway, I was trying to axiomatize the not-free predicate as follows: If a variable x does not occur in an expression S then x is not free in S. If S is a quantifier expression (of the form forall x: P, exists x: P, et cetera) then x, being quantified over is not free. If S1, S2 are arbitrary sequences of symbols, neither contains x, S is an expression in which x is not free and the sequence S1 S S2 is an expression then x is not free in S1 S S2.

I see. To make this work you would need to define a type of "arbitrary sequences of symbols" and use that type for S1 and S2. I recommend against it, because the syntax ambiguity will bite you later. You can do it using well formed expressions if you have axioms for each syntax constructor; that's what I did in my message.

Mario