Are Metamath and Q0 "roughly equivalent"?

[Cris Perdue]

My comments here are partly stimulated by some recent postings, especially by Ken Kubota. Like Ken, I am a fan of Q0's as a logical foundation. I am also a fan of Metamath in its role as something of a modern Principia Mathematica and as a sort of encyclopedia of mathematical results, with all proofs and definitions completely spelled out and easily accessible on the Web.

While working on a software system, (http://prooftoys.org/)  that happens to be closely based on Q0, and following Metamath a bit, I have had persistent sense that proofs in Metamath feel a lot like proofs in Q0, though their axioms and in general statements in the languages look rather different.

In particular I have lately been asking myself whether perhaps the WFF and class variables in Metamath are equivalent or at least significantly parallel to functions in Q0 from individuals to booleans. I am thinking now that the answer to this question may be that yes, in fact there is a technical equivalence. I will refer to propositions in Andrews, 2002 by their numbers or names there in case anyone wishes to look them up.

I have been struck by the comparison between Metamath's Axiom of Quantifier Introduction 2 (http://us.metamath.org/mpegif/ax-17.html), and a metatheorem of Q0, closely related to Andrews' 2103 and Andrews' 5235, namely:

A => ∀ x. A

(provided that x is not free in A).

It appears to me that being not free in A amounts in the end to the same thing as not appearing at all in phi in Metamath, because there is enough freedom to rename Metamath variables.  (If this or other proposals appear to be incorrect, I will be grateful for responses with corrections.)

All of this is especially interesting in that this Axiom 17 of Metamath is precisely the only one that has a distinct variable condition.

Comparing with Q0, it is a theorem of Q0 that p => ∀ x. p, where x is an individual and p is a boolean variable. We can substitute any boolean term for p here, provided that x is not free in the boolean term, and thus the metatheorem just above. (Or we could indeed substitute any boolean term for p, but then we must rename the quantified x, which is contrary to the intention.)

Metamath of course uses greek letters for wff variables where Andrews uses bolded latin capitals, but here is the start of a parallel.

To get the effect of wff metavariables within quantifiers in Q0, we can use a modification of the approach above. Inventory all of the quantified variables (e.g. x and y) in which the wff appears in Metamath. Then write a Q0 statement such as p(x, y) in place of the Metamath phi or other greek variable, where p (or q, etc.) is a predicate over individuals. This p(x, y) can be made into an arbitrary wff by instantiating p with a lambda term, most conveniently x and y, e.g. λx. λy. <wff>. The lambda binding prevents capturing of the variables in <wff>, and lambda conversion makes the lambdas disappear, leaving just the wff wherever p appeared in the original Q0 statement. (Technically Q0 does not have functions/predicates of more than one variable, but Currying accomplishes the same effect.)

Now this is only useful if the Q0 statement corresponding to the Metamath statement is a theorem of Q0.  I have looked at the list of Metamath predicate calculus axioms, and most of them seem to be simple theorems in Q0.

Axiom 11 (Variable Substitution) deserves a bit closer look than I have given it, but it looks like this one can be proven by Andrews' fundamental (but derived!) rule of inference rule R Prime (R'). By asserting the theorem x = y => x = y, I think we get the prerequisites to apply Rule R' to derive Axiom 11's direct counterpart. For what it's worth, Metamath implicit substitution looks directly related to Q0's rules R and R', with the difference (I believe) that implicit substitution replaces ALL occurrences, not just one or more.

Full set theory in the form of ZFC, or ZF, or even Z, is not part of Q0. So in suggesting an equivalence between the systems I am assuming the addition of axioms for set theory to Q0, specifically a theory in Q0 where the individuals are sets. The idea then is that Metamath class variables translate to variables of type "predicate of sets" in Q0.

Q0, for its part, has higher types and quantifiers over variables of higher types, but from what I read, this does not give it fundamentally greater power than FOL with ZFC.

Am I missing something??  I will be very interested in analysis of how this sort of equivalence between Metamath and Q0 breaks down, if that is the case.

Regards,

Cris

[Cris Perdue]

My previous posting omits discussion of direct substitution versus noncapturing substitution. Sorry for not addressing that before sending it off.  I have not looked carefully at that aspect, but I do recall an old posting by Raph Levien related to distinct variable conditions and translation from Metamath to Ghilbert, which might be relevant. He talks about "fresh" variables, and I need to understand the implications of freshness better.

https://groups.google.com/forum/#!searchin/metamath/distinct$20variable$20conditions/metamath/hJupn_hvqu8/KJg69J8BFAEJ

Does someone have easy examples of Metamath taking advantage of direct substitution to do prove something more easily than a system with noncapturing substitutions?

[Mario Carneiro]

On Mon, Apr 17, 2017 at 7:42 PM, Cris Perdue <cris....@gmail.com> wrote:

My comments here are partly stimulated by some recent postings, especially by Ken Kubota. Like Ken, I am a fan of Q0's as a logical foundation. I am also a fan of Metamath in its role as something of a modern Principia Mathematica and as a sort of encyclopedia of mathematical results, with all proofs and definitions completely spelled out and easily accessible on the Web.

While working on a software system, (http://prooftoys.org/)  that happens to be closely based on Q0, and following Metamath a bit, I have had persistent sense that proofs in Metamath feel a lot like proofs in Q0, though their axioms and in general statements in the languages look rather different.

Let me begin with the answer to your general question: Yes, there is an "intended" translation between many terms of Q0 and terms of Metamath, and as long as you stay in this fragment you will get that "persistent sense" of equivalence. Unfortunately, there are various technicalities that make this translation fray at the edges, and it is exactly in the axioms of the respective systems where this equivalence is at its poorest, where each system can make statements that the other cannot interpret.

 

In particular I have lately been asking myself whether perhaps the WFF and class variables in Metamath are equivalent or at least significantly parallel to functions in Q0 from individuals to booleans. I am thinking now that the answer to this question may be that yes, in fact there is a technical equivalence. I will refer to propositions in Andrews, 2002 by their numbers or names there in case anyone wishes to look them up.

This is definitely the intended translation. More specifically, a wff expression is a term of type o, a set variable is a variable of type i, and a class expression is a term of type (oi) (that is, a function from sets to propositions). Wff and class expressions may contain free variables, and these are lambda-abstracted when a binder such as A. x ... or { x | ... } is applied.

 

I have been struck by the comparison between Metamath's Axiom of Quantifier Introduction 2 (http://us.metamath.org/mpegif/ax-17.html), and a metatheorem of Q0, closely related to Andrews' 2103 and Andrews' 5235, namely:

A => ∀ x. A

(provided that x is not free in A).

It appears to me that being not free in A amounts in the end to the same thing as not appearing at all in phi in Metamath, because there is enough freedom to rename Metamath variables.  (If this or other proposals appear to be incorrect, I will be grateful for responses with corrections.)

All of this is especially interesting in that this Axiom 17 of Metamath is precisely the only one that has a distinct variable condition.

This is the part of the translation where Metamath is stronger than Q0 (that is, able to express Q0-inexpressible statements). The distinct variable condition is less interesting than its absence, which may have gone without comment through the first 16 axioms but requires some additional thought. In FOL or lambda calculus based systems, variables are distinct because they are textually different, so bound variable capture is a syntactic constraint that is enforced by alpha conversion during substitution. In Metamath, this is a provable predicate (which is trivially decidable and hence never written out) asserting that two variables have no common substitutions. This whole idea doesn't even make sense in FOL, where variables are variables, but in Metamath variables act like metavariables, so that certain meta constraints are lowered to the object level. (If I understand correctly, this is what Ken means by "eliminating the metalanguage".)

Q0 is much more orthodox in its handling of variable binding, so that so-called "bundled" theorems such as |- E. x x = y (with no disjointness condition on x,y) are not expressible directly in Q0. (There are more complicated expressions involving conjunctions of mirror copies of the theorem, but this translation is not compositional.)

 

Comparing with Q0, it is a theorem of Q0 that p => ∀ x. p, where x is an individual and p is a boolean variable. We can substitute any boolean term for p here, provided that x is not free in the boolean term, and thus the metatheorem just above. (Or we could indeed substitute any boolean term for p, but then we must rename the quantified x, which is contrary to the intention.)

I think you are seeing how the parallel is not perfect here, since there are additional rules for bound variable renaming in lambda calculus systems like Q0.

 

To get the effect of wff metavariables within quantifiers in Q0, we can use a modification of the approach above. Inventory all of the quantified variables (e.g. x and y) in which the wff appears in Metamath. Then write a Q0 statement such as p(x, y) in place of the Metamath phi or other greek variable, where p (or q, etc.) is a predicate over individuals. This p(x, y) can be made into an arbitrary wff by instantiating p with a lambda term, most conveniently x and y, e.g. λx. λy. <wff>. The lambda binding prevents capturing of the variables in <wff>, and lambda conversion makes the lambdas disappear, leaving just the wff wherever p appeared in the original Q0 statement. (Technically Q0 does not have functions/predicates of more than one variable, but Currying accomplishes the same effect.)

I'm not quite clear on the direction of your translation, but I think you have the right idea. Provided that all set variables are distinct, a Metamath theorem has a simple interpretation as an inference rule in FOL, or a term in dependent type theory (or Q0), in which each wff variable is translated into a variable of type ((oi)...i), which is applied to the same variables x,y,... that appear in binders surrounding the variable. (I plan to write a paper about this translation process once I have a working implementation.)
 

Now this is only useful if the Q0 statement corresponding to the Metamath statement is a theorem of Q0.  I have looked at the list of Metamath predicate calculus axioms, and most of them seem to be simple theorems in Q0.

Here is where Ken's approach makes things more complicated. Since he doesn't want any non-logical axioms, this means that he will not be able to assert that the type i of "individuals" has any particular properties, such as being infinite. He prefers to do all such work within a conditional. Although this is possible, and done in set.mm in a few places, notably in the big theorems that use choice (like http://us2.metamath.org:88/mpegif/zorng.html, where A e. dom card means A is well-orderable), in the large scale it is quite impractical. I would not want to have "ZFC ->" prepending every theorem in set.mm. Speaking roughly, I say that an axiom is worth making an axiom and not a conditional if you (a) can't ever prove the statement by other means (for example, A e. dom card is provable in the case where A is a countable set) and (b) you want to reason about the axiom being false (for example if you want to prove an equivalent form of the axiom of choice). Note that it is not sufficient to merely want to consider the possibility of the axiom not holding, because this can be done easily enough by not referencing the axiom (provided that the software tracks axiom usage, as Metamath does).

 

Axiom 11 (Variable Substitution) deserves a bit closer look than I have given it, but it looks like this one can be proven by Andrews' fundamental (but derived!) rule of inference rule R Prime (R'). By asserting the theorem x = y => x = y, I think we get the prerequisites to apply Rule R' to derive Axiom 11's direct counterpart. For what it's worth, Metamath implicit substitution looks directly related to Q0's rules R and R', with the difference (I believe) that implicit substitution replaces ALL occurrences, not just one or more.

Full set theory in the form of ZFC, or ZF, or even Z, is not part of Q0. So in suggesting an equivalence between the systems I am assuming the addition of axioms for set theory to Q0, specifically a theory in Q0 where the individuals are sets. The idea then is that Metamath class variables translate to variables of type "predicate of sets" in Q0.

Q0, for its part, has higher types and quantifiers over variables of higher types, but from what I read, this does not give it fundamentally greater power than FOL with ZFC.

Here is the other side of the failure of translation. Of course, Q0 is a higher order logic, so it can quantify over things that Metamath (meaning set.mm) can't. This means that the intuitive translation from Metamath to Q0 is not surjective, i.e. there are plenty of statements that can't be translated to FOL. Because Q0 is so weak, it is possible to translate all of Q0 to Metamath, but this will require changing the meta positioning of the two systems, by using Metamath as a metalanguage for Q0 instead of the other way around. For this, you could take o as the set {0,1}, i as the set NN, and function types as functions, equality as equality, etc.

 
On Mon, Apr 17, 2017 at 8:39 PM, Cris Perdue <cris....@gmail.com> wrote:

Does someone have easy examples of Metamath taking advantage of direct substitution to do prove something more easily than a system with noncapturing substitutions?

An example of a proof which naturally produces a "bundled" theorem, where the bundling can be taken advantage of in an essential way, is the theorem 19.2 (http://us2.metamath.org:88/mpegif/19.2.html):

|- ( A. x ph -> E. y ph )

with no disjointness conditions on anything. This is proven in two steps:

  |- ( A. x ph -> ph )
  |- ( ph -> E. y ph )
|- ( A. x ph -> E. y ph )

Since the "x" in the first step and the "y" in the second are not related, this is simply the syllogism of two unrelated binders so that we may allow "x" and "y" to be the same variable. However, in FOL the choice of whether or not "x" and "y" are distinct results in completely different theorems, even though the proof is the same. If they are different, the appropriate translation is:

|- (∀x, P(x, y) -> ∃y, P(x, y))

or after bound variable renaming and taking the universal closure:

|- ∀x y, (∀x', P(x', y) -> ∃y', P(x, y'))

This is to be compared against the translation of the same Metamath statement where "x" and "y" are substituted for the same variable z:

|- ( A. z ph -> E. z ph )

which becomes

|- (∀z, P(z) -> ∃z, P(z))

It is not hard to see that neither of these two translated theorems easily follows from the other, and you would have to choose which one to use in each individual case, even though the FOL proofs of these statements are mirror versions of each other.

Mario

[Ken Kubota]

Let me first add a note on references in R0, and then answer below each quoted passage.

Page references in http://www.owlofminerva.net/files/formulae.pdf

usually are given for the 2nd edition of Andrews' textbook (2002),

but if you have to use the 1st edition (1986), the following information

might help.

The encoding of the file names is as follows: Files beginning with

'A' (for "Andrews", e.g., A5224) contain formalized proofs first presented

by Andrews, files beginning with 'K' (for "Kubota", e.g., K8000) my own.

Theorem A5224 corresponds to Theorem 5224 in Andrews' textbook.

In some cases two variants of a proof exist, with (A5224H) and

without (A5224) hypothesis. To preserve the ordering of filenames, the

'X' in the name of Andrews' exercises (e.g., X5308) are moved to

the center (A53X08).

In Andrews' textbook, the first figure denotes the chapter, and the first two

figures denote the paragraph, hence Theorem 5224 is from chapter 5, §52.

Am 18.04.2017 um 02:54 schrieb Mario Carneiro <di....@gmail.com>:

On Mon, Apr 17, 2017 at 7:42 PM, Cris Perdue <cris....@gmail.com> wrote:

My comments here are partly stimulated by some recent postings, especially by Ken Kubota. Like Ken, I am a fan of Q0's as a logical foundation. I am also a fan of Metamath in its role as something of a modern Principia Mathematica and as a sort of encyclopedia of mathematical results, with all proofs and definitions completely spelled out and easily accessible on the Web.

While working on a software system, (http://prooftoys.org/)  that happens to be closely based on Q0, and following Metamath a bit, I have had persistent sense that proofs in Metamath feel a lot like proofs in Q0, though their axioms and in general statements in the languages look rather different.

Let me begin with the answer to your general question: Yes, there is an "intended" translation between many terms of Q0 and terms of Metamath, and as long as you stay in this fragment you will get that "persistent sense" of equivalence. Unfortunately, there are various technicalities that make this translation fray at the edges, and it is exactly in the axioms of the respective systems where this equivalence is at its poorest, where each system can make statements that the other cannot interpret.

In logical frameworks like Metamath you distinguish between the

(1) language of the framework and the

(2) language formalized within.

For example, in Isabelle you would have

Isabelle/HOL and

Isabelle/ZF,

and the corresponding Metamath notation would be

Metamath/hol or Metamath/hol.mm

Metamath/set or Metamath/set.mm

Since Q0 is (2) a language to be formalized within, and

the Metamath language (1) the language of the framework,

I see no point in comparing these two directly.

Larry Paulson already pointed out that the language of the

framework (1) can be much weaker:

"Actually, the object version of higher-order logic has to be

much larger than the meta-logic because it is intended for

expressing all kinds of mathematics. The meta-logic only

has to express other formal systems."

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 3)

I try to avoid the terms "meta-logic" and "object logic" here,

as they might lead to confusion when discussing Hilbert-style systems.

Also, Q0 has, like [Church, 1940], no type variables (in the

object language). For a comparison with current logics, one should

use a more recent formulation with type variables, type abstraction,

and dependent types, such as R0.

In particular I have lately been asking myself whether perhaps the WFF and class variables in Metamath are equivalent or at least significantly parallel to functions in Q0 from individuals to booleans. I am thinking now that the answer to this question may be that yes, in fact there is a technical equivalence. I will refer to propositions in Andrews, 2002 by their numbers or names there in case anyone wishes to look them up.

This is definitely the intended translation. More specifically, a wff expression is a term of type o, a set variable is a variable of type i, and a class expression is a term of type (oi) (that is, a function from sets to propositions). Wff and class expressions may contain free variables, and these are lambda-abstracted when a binder such as A. x ... or { x | ... } is applied.

 

I have been struck by the comparison between Metamath's Axiom of Quantifier Introduction 2 (http://us.metamath.org/mpegif/ax-17.html), and a metatheorem of Q0, closely related to Andrews' 2103 and Andrews' 5235, namely:

A => ∀ x. A

(provided that x is not free in A).

It appears to me that being not free in A amounts in the end to the same thing as not appearing at all in phi in Metamath, because there is enough freedom to rename Metamath variables.  (If this or other proposals appear to be incorrect, I will be grateful for responses with corrections.)

All of this is especially interesting in that this Axiom 17 of Metamath is precisely the only one that has a distinct variable condition.

This is the part of the translation where Metamath is stronger than Q0 (that is, able to express Q0-inexpressible statements). The distinct variable condition is less interesting than its absence, which may have gone without comment through the first 16 axioms but requires some additional thought. In FOL or lambda calculus based systems, variables are distinct because they are textually different, so bound variable capture is a syntactic constraint that is enforced by alpha conversion during substitution. In Metamath, this is a provable predicate (which is trivially decidable and hence never written out) asserting that two variables have no common substitutions. This whole idea doesn't even make sense in FOL, where variables are variables, but in Metamath variables act like metavariables, so that certain meta constraints are lowered to the object level. (If I understand correctly, this is what Ken means by "eliminating the metalanguage".)

Q0 is much more orthodox in its handling of variable binding, so that so-called "bundled" theorems such as |- E. x x = y (with no disjointness condition on x,y) are not expressible directly in Q0. (There are more complicated expressions involving conjunctions of mirror copies of the theorem, but this translation is not compositional.)

Do you mean

|- E x . x = y

with any type of x, y, such that it could be expressed with a type variable a or alpha:

|- E x : a   .   x : a  = y : a

?

Why do you think this could not be obtained in Q0?

If the scope of the variable is a problem, my first attempt would be

prepending universal quantifiers, e.g.,

|- A y : a  E x : a   .   x : a  = y : a

and in R0, even over the type variable a of type t (tau, the type of types)

|- A a : t  A y : a  E x : a   .   x : a  = y : a

and later eliminate the universal quantifiers using universal instantiation

(Andrews' theorem 5215 referred to on p. 11 of

http://www.owlofminerva.net/files/formulae.pdf)

Comparing with Q0, it is a theorem of Q0 that p => ∀ x. p, where x is an individual and p is a boolean variable. We can substitute any boolean term for p here, provided that x is not free in the boolean term, and thus the metatheorem just above. (Or we could indeed substitute any boolean term for p, but then we must rename the quantified x, which is contrary to the intention.)

I think you are seeing how the parallel is not perfect here, since there are additional rules for bound variable renaming in lambda calculus systems like Q0.

 

To get the effect of wff metavariables within quantifiers in Q0, we can use a modification of the approach above. Inventory all of the quantified variables (e.g. x and y) in which the wff appears in Metamath. Then write a Q0 statement such as p(x, y) in place of the Metamath phi or other greek variable, where p (or q, etc.) is a predicate over individuals. This p(x, y) can be made into an arbitrary wff by instantiating p with a lambda term, most conveniently x and y, e.g. λx. λy. <wff>. The lambda binding prevents capturing of the variables in <wff>, and lambda conversion makes the lambdas disappear, leaving just the wff wherever p appeared in the original Q0 statement. (Technically Q0 does not have functions/predicates of more than one variable, but Currying accomplishes the same effect.)

I'm not quite clear on the direction of your translation, but I think you have the right idea. Provided that all set variables are distinct, a Metamath theorem has a simple interpretation as an inference rule in FOL, or a term in dependent type theory (or Q0), in which each wff variable is translated into a variable of type ((oi)...i), which is applied to the same variables x,y,... that appear in binders surrounding the variable. (I plan to write a paper about this translation process once I have a working implementation.)
 

Now this is only useful if the Q0 statement corresponding to the Metamath statement is a theorem of Q0.  I have looked at the list of Metamath predicate calculus axioms, and most of them seem to be simple theorems in Q0.

Here is where Ken's approach makes things more complicated. Since he doesn't want any non-logical axioms, this means that he will not be able to assert that the type i of "individuals" has any particular properties, such as being infinite. He prefers to do all such work within a conditional. Although this is possible, and done in set.mm in a few places, notably in the big theorems that use choice (like http://us2.metamath.org:88/mpegif/zorng.html, where A e. dom card means A is well-orderable), in the large scale it is quite impractical. I would not want to have "ZFC ->" prepending every theorem in set.mm. Speaking roughly, I say that an axiom is worth making an axiom and not a conditional if you (a) can't ever prove the statement by other means (for example, A e. dom card is provable in the case where A is a countable set) and (b) you want to reason about the axiom being false (for example if you want to prove an equivalent form of the axiom of choice). Note that it is not sufficient to merely want to consider the possibility of the axiom not holding, because this can be done easily enough by not referencing the axiom (provided that the software tracks axiom usage, as Metamath does).

Your use of the word "impractical" reveals that you use criteria

other than expressiveness for specifying the logic.

Unfortunately, in some fields, expressiveness and practical

considerations (e.g., automation) contradict each other.

If you want to be consequent, you have to decide for either one.

The concept of Metamath as presented on the homepage

("philosophy of simplicity", "minimum possible framework",

"completely transparent with nothing hidden from the user")

is included in or identical with Andrews' notion of expressiveness.

If one consequently follows this path, then the use of conditionals

should be preferred to the use of axioms. This has at least three

major advantages.

First, universality: using conditionals allows for expressing different theories

in the same field of discourse, which otherwise would contradict, as the

axioms of each theory rules out the other. Possible relations between the

two theories can be expressed, and further theorems based on both

theories.

Second, the emptiness of theories with contradicting axioms

can be expressed, as they simply result in the emptiness of the

defined set. Using axioms, the logic is rendered inconsistent

as a whole, without the possibility of explicitly stating the

emptiness of the defined set.

Third, the dependency is made explicit. If "the software tracks

axiom usage, as Metamath does", the task of tracking dependencies

is moved from the logic to the software, which I already, in another

context, criticized at Kunčar/Popescu's approach (which is

nevertheless legitimate as an auxiliary approach).

But if nothing should be "hidden from the user", this means it actually

should be part of the logic. For example, in the email to John Harrison

I forwarded to you, Andrews' exercise X5308 which is stated and 

formalized on pp. 151 ff. of

http://www.owlofminerva.net/files/formulae.pdf

is taken as an example where the dependency of the theorem

is make explicit, assuming the form

AC => theorem

since the (non-logical) Axiom of Choice was

introduced as a conditional, not as an axiom.

In summary, with non-logical axioms the expressiveness

of the logic would be reduced significantly (see the three

examples above), just for gaining some possible practical

advantages, which is, from a logical perspective,

completely irrelevant.

For this reason, I believe that Q0 and R0 are more consequent

in carrying out their underlying design principles than Metamath

with its obviously very similar or even identical concept

(although of course I acknowledge the strong achievements by Metamath).

Please note that the concept of expressiveness shouldn't be reduced

to just simplicity, since with the reduction to a few rules and symbols

the inner dependencies of the logic are revealed.

I wrote on this issue earlier:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-September/msg00014.html

Axiom 11 (Variable Substitution) deserves a bit closer look than I have given it, but it looks like this one can be proven by Andrews' fundamental (but derived!) rule of inference rule R Prime (R'). By asserting the theorem x = y => x = y, I think we get the prerequisites to apply Rule R' to derive Axiom 11's direct counterpart. For what it's worth, Metamath implicit substitution looks directly related to Q0's rules R and R', with the difference (I believe) that implicit substitution replaces ALL occurrences, not just one or more.

This description of Rule R Prime (Rule R') is not completely accurate,

since it is actually not a derived rule of inference.

The introduction of Rule R' [Andrews, 2002, p. 214] just

the page following the page introducing Rule R [Andrews, 2002, p. 213],

occurs in the form of a 'definition': "we shall define this concept […]".

But, strictly speaking, this isn't a regular mathematical definition

(which is nothing more than a shorthand for a longer expression).

In fact, a second rule is introduced.

Logically, one might consider Rule R just as the subcase of Rule R'

with an empty set of hypotheses.

Technically, both rules have to be implemented separately, since

with the set of hypotheses the formula structure is slightly different,

see functions rule_substitution_r() and rule_substitution_r_prime() on pp. 517 f. of

http://www.owlofminerva.net/files/formulae.pdf

I wrote on this issue earlier, see section 4 of

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-August/msg00069.html

Full set theory in the form of ZFC, or ZF, or even Z, is not part of Q0. So in suggesting an equivalence between the systems I am assuming the addition of axioms for set theory to Q0, specifically a theory in Q0 where the individuals are sets. The idea then is that Metamath class variables translate to variables of type "predicate of sets" in Q0.

Q0, for its part, has higher types and quantifiers over variables of higher types, but from what I read, this does not give it fundamentally greater power than FOL with ZFC.

Here is the other side of the failure of translation. Of course, Q0 is a higher order logic, so it can quantify over things that Metamath (meaning set.mm) can't. This means that the intuitive translation from Metamath to Q0 is not surjective, i.e. there are plenty of statements that can't be translated to FOL. Because Q0 is so weak, it is possible to translate all of Q0 to Metamath, but this will require changing the meta positioning of the two systems, by using Metamath as a metalanguage for Q0 instead of the other way around. For this, you could take o as the set {0,1}, i as the set NN, and function types as functions, equality as equality, etc.

 
On Mon, Apr 17, 2017 at 8:39 PM, Cris Perdue <cris....@gmail.com> wrote:

Does someone have easy examples of Metamath taking advantage of direct substitution to do prove something more easily than a system with noncapturing substitutions?

An example of a proof which naturally produces a "bundled" theorem, where the bundling can be taken advantage of in an essential way, is the theorem 19.2 (http://us2.metamath.org:88/mpegif/19.2.html):

|- ( A. x ph -> E. y ph )

with no disjointness conditions on anything. This is proven in two steps:

  |- ( A. x ph -> ph )
  |- ( ph -> E. y ph )
|- ( A. x ph -> E. y ph )

Since the "x" in the first step and the "y" in the second are not related, this is simply the syllogism of two unrelated binders so that we may allow "x" and "y" to be the same variable. However, in FOL the choice of whether or not "x" and "y" are distinct results in completely different theorems, even though the proof is the same. If they are different, the appropriate translation is:

|- (∀x, P(x, y) -> ∃y, P(x, y))

or after bound variable renaming and taking the universal closure:

|- ∀x y, (∀x', P(x', y) -> ∃y', P(x, y'))

This is to be compared against the translation of the same Metamath statement where "x" and "y" are substituted for the same variable z:

|- ( A. z ph -> E. z ph )

which becomes

|- (∀z, P(z) -> ∃z, P(z))

It is not hard to see that neither of these two translated theorems easily follows from the other, and you would have to choose which one to use in each individual case, even though the FOL proofs of these statements are mirror versions of each other.

Mario

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

[Norman Megill]

On Wednesday, April 19, 2017 at 6:13:45 AM UTC-4, Ken Kubota wrote:

>> Am 18.04.2017 um 02:54 schrieb Mario Carneiro:


[...]

 

In logical frameworks like Metamath you distinguish between the

(1) language of the framework and the

(2) language formalized within.

For example, in Isabelle you would have

Isabelle/HOL and

Isabelle/ZF,

and the corresponding Metamath notation would be

Metamath/hol or Metamath/hol.mm

Metamath/set or Metamath/set.mm

Since Q0 is (2) a language to be formalized within, and

the Metamath language (1) the language of the framework,

I see no point in comparing these two directly.

Larry Paulson already pointed out that the language of the

framework (1) can be much weaker:

"Actually, the object version of higher-order logic has to be

much larger than the meta-logic because it is intended for

expressing all kinds of mathematics. The meta-logic only

has to express other formal systems."

http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-175.pdf (p. 3)

I try to avoid the terms "meta-logic" and "object logic" here,

as they might lead to confusion when discussing Hilbert-style systems.

I our terminology, the Metamath language is a framework (or meta-metalanguge).

The file set.mm uses this framework to implement a metalanguage, stating axiom schemes and proving theorem schemes of FOL and set theory.

The intended object language of the set.mm metalanguage is FOL and ZFC proper.  It consists of all instantiations of the schemes in set.mm.  The object language cannot be represented directly in Metamath, although the metalanguage can emulate it if desired (by imposing global distinct variable conditions on all pairs of individual variables).

[...]

Q0 is much more orthodox in its handling of variable binding, so that so-called "bundled" theorems such as |- E. x x = y (with no disjointness condition on x,y) are not expressible directly in Q0. (There are more complicated expressions involving conjunctions of mirror copies of the theorem, but this translation is not compositional.)

Do you mean

|- E x . x = y

with any type of x, y, such that it could be expressed with a type variable a or alpha:

|- E x : a   .   x : a  = y : a

?

The x and y in Mario's example are metavariables ranging over the individual variables v_1, v_2, ... of the intended object language.  Without requiring that x and y represent distinct object language variables, |- E. x x = y represents two kinds of object language instances simultaneously:

(1)  |- E. v_1  v_1 = v_2,  |- E. v_7 v_7 = v_5, etc. (each with two object language variables)
 
(2)  |- E. v_1  v_1 = v_1,  |- E. v_2 v_2 = v_2, etc. (each with one object language variable)

I think most proof languages keep free and bound variables distinct from each other.  Some people think the direct substitution that results in (2) is inelegant because of its disregard of the roles (free or bound) of x and y.  For those people, and for better compatibility with other proof languages, we can require that x and y be distinct variables.  Keep in mind, though, that |- E. x x = y is a scheme, not an object language statement.
 

Why do you think this could not be obtained in Q0?

I would guess it probably can't if it is like most languages that don't allow a direct common substitution for free and bound variables, but this is an unimportant issue to dwell on.  I'm sure Q0 can represent this with two separate theorems |- E. x x = y and |- E. x x = x, so in the end it is the same thing.

The "bundling" of the set.mm FOL axioms in this way is a natural consequence of Tarski's axiom schemes they are founded on, where the concepts "free variable" and "proper substitution" are absent as primitive notions and replaced with the simpler concept of a variable not occurring in a formula.  People who don't want bundling can still specify that x and y be distinct in the statement of |- E. x x = y.

Tarski himself used the bundled |- E.x x = y for some of his axiomatizations and the unbundled version for others, depending on whether |- E. x x = x was needed for logical completeness of the particular axiomatization.
 

[...]

Here is where Ken's approach makes things more complicated. Since he doesn't want any non-logical axioms, this means that he will not be able to assert that the type i of "individuals" has any particular properties, such as being infinite. He prefers to do all such work within a conditional. Although this is possible, and done in set.mm in a few places, notably in the big theorems that use choice (like http://us2.metamath.org:88/mpegif/zorng.html, where A e. dom card means A is well-orderable), in the large scale it is quite impractical. I would not want to have "ZFC ->" prepending every theorem in set.mm. Speaking roughly, I say that an axiom is worth making an axiom and not a conditional if you (a) can't ever prove the statement by other means (for example, A e. dom card is provable in the case where A is a countable set) and (b) you want to reason about the axiom being false (for example if you want to prove an equivalent form of the axiom of choice). Note that it is not sufficient to merely want to consider the possibility of the axiom not holding, because this can be done easily enough by not referencing the axiom (provided that the software tracks axiom usage, as Metamath does).

Your use of the word "impractical" reveals that you use criteria

other than expressiveness for specifying the logic.

Unfortunately, in some fields, expressiveness and practical

considerations (e.g., automation) contradict each other.

If you want to be consequent, you have to decide for either one.

I don't think "impractical" is necessarily the right word.  It is certainly possible to prefix every theorem with "ZFC ->" if we really wanted to, just that is it ugly and redundant: it doesn't tell us very much.  It is made very clear in the set.mm file that the ZFC axioms are assumed; it is not something hidden in the software.  It's just that we state the axioms once and assume them subsequently; it is wasteful to repeat them as a hypothesis or antecedent of every theorem.  What Mario means by "track axiom usage" is that the software can trace back through proofs to see if say the Axiom of Union was actually used somewhere along the line to prove a particular theorem.  If you don't care about that level of detail, you can just assume that ZFC as a whole was used because it is plainly stated as the axioms in the set.mm file.  We do tend to prove as much as possible after each ZFC axiom is introduced, before introducing new ZFC axioms.

Prepending "ZFC ->" to every theorem does not tell you whether a particular axiom in the conjunction defined as "ZFC" is actually needed or not for the rest of the statement.  The Axiom of Union could have been used somewhere 100 theorems ago, but we wouldn't know it.  In fact, it would make our present axiom tracking software useless because it would track back only to the FOL axioms.  Alternately, we could prepend each theorem with the conjunction "EXT /\ UN /\ POW..." for a finer-grained statement, but that is even uglier, and it still doesn't tell us which of those axioms were actually needed somewhere back in the tree of theorems.  We have to trust that the person stating the theorem didn't use EXT /\ UN /\ POW -> x = x as a lemma.

The concept of Metamath as presented on the homepage

("philosophy of simplicity", "minimum possible framework",

"completely transparent with nothing hidden from the user")

is included in or identical with Andrews' notion of expressiveness.

If one consequently follows this path, then the use of conditionals

should be preferred to the use of axioms. This has at least three

major advantages.

First, universality: using conditionals allows for expressing different theories

in the same field of discourse, which otherwise would contradict, as the

axioms of each theory rules out the other. Possible relations between the

two theories can be expressed, and further theorems based on both

theories.

Second, the emptiness of theories with contradicting axioms

can be expressed, as they simply result in the emptiness of the

defined set. Using axioms, the logic is rendered inconsistent

as a whole, without the possibility of explicitly stating the

emptiness of the defined set.

Third, the dependency is made explicit. If "the software tracks

axiom usage, as Metamath does", the task of tracking dependencies

is moved from the logic to the software, which I already, in another

context, criticized at Kunčar/Popescu's approach (which is

nevertheless legitimate as an auxiliary approach).

But if nothing should be "hidden from the user", this means it actually

should be part of the logic.

It _is_ part of the logic.  The axioms are stated in the set.mm file and not hidden from the user in any way.

For example, in the email to John Harrison

I forwarded to you, Andrews' exercise X5308 which is stated and 

formalized on pp. 151 ff. of

http://www.owlofminerva.net/files/formulae.pdf

is taken as an example where the dependency of the theorem

is make explicit, assuming the form

AC => theorem

since the (non-logical) Axiom of Choice was

introduced as a conditional, not as an axiom.

In summary, with non-logical axioms the expressiveness

of the logic would be reduced significantly (see the three

examples above), just for gaining some possible practical

advantages, which is, from a logical perspective,

completely irrelevant.

For this reason, I believe that Q0 and R0 are more consequent

in carrying out their underlying design principles than Metamath

with its obviously very similar or even identical concept

(although of course I acknowledge the strong achievements by Metamath).

We could make ZFC -> part of every theorem and use just the axioms of FOL.  That we don't do this is a ultimately matter of taste of how we have chosen to state our theorems, not a limitation of the Metamath framework or of set.mm.  On every web page generated from set.mm, we list exactly what axioms were actually used by a particular proof, which I think is much more informative than just seeing ZFC -> in front of every theorem.

I should mention that this is the style we use for ZFC itself (although sometimes we use CHOICE <-> ... to show AC equivalents, before we introduce AC as an axiom).  For theories derived under the ZFC axioms, such as group theory, we don't state the group "axioms" as separate axioms.  Instead, we define the class Grp of all group structures, with the "axioms" embedded as a conjunction in the definition, and prepend "G e. Grp ->" (G is a group) in front of theorems about groups.

Norm

[Cris Perdue]

Thanks very much to both Mario and Norman for the thorough and enlightening responses on the parallels and differences between a higher-order logic in the form of Q0, and Metamath with its set theory. I think this will help me a lot in relating to how the systems are different. The example theorems with their proofs are also great from my point of view.

As Mario puts it, "The distinct variable condition is less interesting than its absence", which I have failed to properly appreciate up to now. 

So is theorem bundling (in the absence of distinct variable conditions) the key essential extension of expressive power in Metamath compared with HOL systems such as Q0? If so, it seems a very interesting fact.

From remarks in Raph Levien's old posting, I gather that this bundling is not terribly widespread in Metamath. Given that most of the Metamath axioms are expressed without distinct variable constraints (or can be so expressed in the case of its set theory), it seems surprising to me that the phenomenon does not occur all over the place.

About Ken's use of conditionals such as "ZFC -> <theorem>" --

It seems to me that this approach can be a good idea, or not, depending greatly on the practical context.  For example, in Metamath the theorems are all stated in their full detail to be read by human beings on the Web site if desired, and this is part of Metamath's commitment to transparency. Furthermore, in general it seems to be pretty clear from context whether a theorem is part of set theory or pure logic. Since Metamath shows exactly which axioms are used in the derivation of a theorem, it is also easy to check in case of doubt. So the extra conditional tends to amount to clutter.

On the other hand, in the internals of a theorem prover, including the axioms explicitly in conditionals seems an elegant way to keep track of the theory one is working in. And I don't think it would prevent practical construction of algorithms to determine the exact set of axioms used in (or really "relevant to") the derivation of a theorem. Does this seem fair?

-Cris

[Norman Megill]

On Thursday, April 20, 2017 at 2:45:28 PM UTC-4, Cris wrote:
[...]

About Ken's use of conditionals such as "ZFC -> <theorem>" --

It seems to me that this approach can be a good idea, or not, depending greatly on the practical context.  For example, in Metamath the theorems are all stated in their full detail to be read by human beings on the Web site if desired, and this is part of Metamath's commitment to transparency. Furthermore, in general it seems to be pretty clear from context whether a theorem is part of set theory or pure logic. Since Metamath shows exactly which axioms are used in the derivation of a theorem, it is also easy to check in case of doubt. So the extra conditional tends to amount to clutter.

On the other hand, in the internals of a theorem prover, including the axioms explicitly in conditionals seems an elegant way to keep track of the theory one is working in. And I don't think it would prevent practical construction of algorithms to determine the exact set of axioms used in (or really "relevant to") the derivation of a theorem. Does this seem fair?

 I agree.  It depends on the situation and context.  My earlier comment had to do with Metamath/set.mm where I don't think "ZFC ->" would be appropriate because of the ease of getting the same information either by looking in the file itself (just grep for all previous $a statements) or with software tools (to get fine-grained information about what axioms are actually used).  So it would seem redundant and somewhat wasteful.

There may be different considerations with other situations or systems.  I could see the appeal having all information self-contained in a single statement, with nothing but the logic of the proof system needed for its proof, in principle at least.

Norm