Q0 Library in Metamath

[Thierry Arnoux]

Hi Mario, Norm, Cris, all,

Curious about the Q0 language, and about whether Metamath can 'do Q0'
just like it 'does set theory' in set.mm, I've started Q0 library in
Methamath I wanted to share. I see this as a side project and don't plan
to go very far, but wanted to share anyway.

First, where would this go to? I would like to be able to share and
track changes like we do with set.mm in GitHub. Shall I create a
different repository or would this fit into any existing one?
It's very small in size, so I'm attaching it to this mail to share a
first version.

Second, I have a technical question. While I can write all proofs using
the metamath program, MMJ2 refuses to apply ~ mpeq and related theorems
( ~ mpbi , ~ r-f ). Is there anything I'm doing wrong? Or are there
maybe special $j primitives that MMJ2 requires to apply those theorems?
This is quite a handicap because ~ mpeq is probably going to be needed
in nearly every proof. I wanted to ask you before I give up or dig into
MMJ2 to understand $j ' use.

I think I have a good starting point, but I see one caveat : the current
~ xa axiom states that variables can be of any type. I'm afraid this is
maybe too flexible and could lead to contradictions, as one could use it
twice in the same proof to give to one variable ` x ` two different
types. This could actually not be a real issue, but anyway needs more
thought.

BR,
_
Thierry

[Mario Carneiro]

Hi Thierry,

A meta-suggestion: use hol.mm as a starting point. It needed to solve basically the same problems, and the solutions might be helpful to you.

A few suggestions:

* Use a : instead of _ as the typing judgment (this is standard in the type theory literature)

* You are right that xa is going to cause inconsistencies, or more precisely, you can use it to ignore typing constraints and turn this into the untyped lambda calculus. The solution is to annotate the type in the lambda builder. In hol.mm I used the notation "\ x : al . A" for lambda (the slash looks kind of like a lambda, and the brackets are not needed).

* Don't bother with an abbreviation for iff if it is identical to = (which you have already given an abbreviation).

* Your smiley-face implication is bizarre. Why not use "->" or "=>"? (Please don't use the superset symbol, that is archaic notation.)

* I suggest you reuse fop for equality: Use "=" instead of "Q.". (I assure you this will be easier to read, and simpler with fewer notational definitions. You might argue about notational differences from Q0, but it will be hard enough to read as it is and you should do your best to make it as clean as possible otherwise.)

For the second point above, there are two directions to go to type variables, and I have tried both of them:

* In hol.mm, I type variables by having every variable come with an explicit type at every occurrence. This is extremely cumbersome for larger formulas, but is a reasonable approach when you have mechanisms to hide internal data in presentation format. This is the approach OpenTheory had been using, so I borrowed it for HOL.

* In dtt.mm (dependent type theory), unlike HOL, typing judgments were done with a context. (Are there sigma and pi builders in Q0? If so, it is a DTT). In this case, it is possible to remove type annotations from variables, because the typing judgment will carry the type through. For example:

 |- [] , x : al |= x : al

|- [] |= \ x : al . x : al -> al

As to your technical question: what do you mean by "apply" mpeq? If you write

:mpeq |- x _ alpha

does it not produce

50::  |- &C1 _ alpha

51::  |- [ x = &C1 ]

52::mpeq |- x _ alpha

? Or are you hoping that it will be automatically applied in certain conditions? mmj2 does not use most of the $j annotations - they are mostly theoretical at this point, although mm-scala can read them. One thing which mmj2 has hardcoded, which presents difficulty in switching databases, is that the provable assertion is "|-" and the corresponding syntax type is "wff" - so you will have difficulty if you change theses names. But you haven't, so it must be something else. (In hol.mm, I also have the problem that the "&T" default metavariable notation overlaps for "term" and "type", so I have to override one of them in the RunParms.)

Mario

Thierry


--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Ken Kubota]

Dear Thierry,

I am thrilled seeing a Q0 implementation in the Metamath logical framework.
Some people at the HOL mailing list will be interested in this, too, so let me copy to this list.

Unfortunately, I’m busy with my own projects and unable to get into
the details of Metamath currently, which seems very interesting.

However, it might help to have formalizations of the proofs at hand.
For example, Andrews’ theorems 5205, 5210, 5211, and 5212,
which you seem to have proven, are all formalized in the
R0 implementation:
http://doi.org/10.4444/100.10.3


To create an HTML file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.html
To create and automatically open the HTML file (Mac only), enter
make A5211.r0.out.html && open -a Finder $_

To create a PDF file for the proof of Andrews' Theorem 5211 (T & T = T)
implemented in file 'A5211.r0.txt', run
make A5211.r0.out.pdf
To create and automatically open the PDF file (Mac only), enter
make A5211.r0.out.pdf && open -a Finder $_
PDF creation requires installation of LaTeX and pandoc.

More details can be found at
http://www.owlofminerva.net/files/README.txt


Best regards,

Ken Kubota

____________________________________________________


Ken Kubota
http://doi.org/10.4444/100



Link to mail and attachment:
https://groups.google.com/d/msg/metamath/I9obSTiuDl4/t-qoolnHAgAJ

> --
> You received this message because you are subscribed to the Google Groups "Metamath" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

> To post to this group, send email to meta...@googlegroups.com.
> Visit this group at https://groups.google.com/group/metamath.
> For more options, visit https://groups.google.com/d/optout.

> <q0.mm>

[Cris Perdue]

Thierry's effort related to Metamath and Q0 piques my own curiosity a bit also.

It surprises me a bit to think that Metamath might be able to represent Q0's fundamental inference rule R directly, since it applies to an arbitrary subexpression of the target statement. As I recall, in HOL Light there is no such primitive capability, and HOL Light might be easier to implement in Metamath as a consequence. Presumably something like rule R is built in HOL Light as a derived rule of inference. If so, this suggests to me that in Metamath, a counterpart to rule R would need some sort of automation to implement it.

Metamath's implicit substitution looks to me much like Q0's rule R, but I believe it must replace all occurrences rather than just one, which seems more consistent with Metamath's substitution primitive. 

Any thoughts on this?

[Mario Carneiro]

Every formal system I know except Metamath has some primitive rule for proper substitution, HOL included. (In the case of HOL it is the beta rule.) Metamath is quite unique in this respect.

The major observation that makes Metamath capable of simulating all these systems is that all inductive definitions are specifiable by a finite number of axiom (schemes) in Metamath. Here, Thierry is accomplishing the inductive definition of substitution by defining the redex [ [ L^ x A ] B ] by induction on A with ax-4c, ax-4i, ax-4ap, ax-4ab, and ax-4ab2. It is then a metatheorem that every term A can be reduced by these axioms.

I should be careful, though: Metamath *does* have a substitution primitive, namely the substitution of an expression for each term in a theorem, which is Metamath's "one rule". This is, however, a non-capturing substitution, so it can be defined in arbitrary string rewriting systems.

Mario

[Thierry Arnoux]

Thank you Mario and Ken for your detailed answers!

* Concerning the type of variables: thank you very much for pointing me to hol.mm, this is very similar to Q0 and a good source of inspiration - I shall have checked it before. I did not find dtt.mm, though, where can I find it?

I believe the best way to solve the issue stem from why I initially introduced this axiom ~ ax . In most proofs, I feel actually OK with adding the type of the variables used as an hypothesis. I only introduced this new axiom when proving ~ wf , which states that F. is of type _o (truth value). The definition of F. , [ F. = [ [ L^ x T. ] = [ L^ x x ] ] ] , uses a variable x. However the variable does not appear in the final theorem, so it shall not be necessary to add an hypothesis about the type of that variable. My solution, to add as an axiom that a variable can be of any type, is probably too simplistic, and I might have to adopt one of the two solutions proposed by Mario. (There are no Sigma and Pi type builders in Q0, it is based on Church's type theory "simple type theory").

* I solved the issue I had with MMJ2. What I did is adding one dot symbol at the end of the formula. I guess that MMJ2 had issues with parsing some formula without it, and the dot makes them unambiguous (I thought they already were). I can now work with MMJ2 (and Eclipse). I also discovered the parameter "LogicStmtType" in MMJ2 so I chose to change my statement type from "wff" to "statement" for the sake of clarity.

I'm moving on and sharing my library on GitHub, under the same license as set.mm (creative commons). I see that Ken has added Prof. Andrews to the mail: if there is any issue with this, please tell me.

Thanks again,

Regards,
_
Thierry

PS. For the notation:

* As for the symbol choice, I will replace " _ " with " : " in type definitions.

* I will also replace the "superset" symbol for implication with " -> ".  I initially chose it as it was the one used in the textbook, and the smiley face was the nearest I could get with ASCII. Actually I was confused by this "superset" notation initially as I did not know it and when taken as a set operation, it's meaning is actually the opposite ( in the sense that A implies B (A ⊃ B) if and only if  { x | A } ⊂ { x | B }... )

* Equivalence ( ≡ which I note " == " in ASCII) is not exactly the same as equality ( = ), as it is only valid for truth values, so their "type domains" are not the same, even though they are identical in the domain of ≡ ...

On 18/05/2017 19:22, Mario Carneiro wrote:

Hi Thierry,

A meta-suggestion: use hol.mm as a starting point. It needed to solve basically the same problems, and the solutions might be helpful to you.

A few suggestions:

* Use a : instead of _ as the typing judgment (this is standard in the type theory literature)

* You are right that xa is going to cause inconsistencies, or more precisely, you can use it to ignore typing constraints and turn this into the untyped lambda calculus. The solution is to annotate the type in the lambda builder. In hol.mm I used the notation "\ x : al . A" for lambda (the slash looks kind of like a lambda, and the brackets are not needed).

* Don't bother with an abbreviation for iff if it is identical to = (which you have already given an abbreviation).

* Your smiley-face implication is bizarre. Why not use "->" or "=>"? (Please don't use the superset symbol, that is archaic notation.)

* I suggest you reuse fop for equality: Use "=" instead of "Q.". (I assure you this will be easier to read, and simpler with fewer notational definitions. You might argue about notational differences from Q0, but it will be hard enough to read as it is and you should do your best to make it as clean as possible otherwise.)

For the second point above, there are two directions to go to type variables, and I have tried both of them:

* In hol.mm, I type variables by having every variable come with an explicit type at every occurrence. This is extremely cumbersome for larger formulas, but is a reasonable approach when you have mechanisms to hide internal data in presentation format. This is the approach OpenTheory had been using, so I borrowed it for HOL.

* In dtt.mm (dependent type theory), unlike HOL, typing judgments were done with a context. (Are there sigma and pi builders in Q0? If so, it is a DTT). In this case, it is possible to remove type annotations from variables, because the typing judgment will carry the type through. For example:

 |- [] , x : al |= x : al

|- [] |= \ x : al . x : al -> al

As to your technical question: what do you mean by "apply" mpeq? If you write

:mpeq |- x _ alpha

does it not produce

50::  |- &C1 _ alpha

51::  |- [ x = &C1 ]

52::mpeq |- x _ alpha

? Or are you hoping that it will be automatically applied in certain conditions? mmj2 does not use most of the $j annotations - they are mostly theoretical at this point, although mm-scala can read them. One thing which mmj2 has hardcoded, which presents difficulty in switching databases, is that the provable assertion is "|-" and the corresponding syntax type is "wff" - so you will have difficulty if you change theses names. But you haven't, so it must be something else. (In hol.mm, I also have the problem that the "&T" default metavariable notation overlaps for "term" and "type", so I have to override one of them in the RunParms.)

Mario

On Wed, May 17, 2017 at 10:41 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Hi Mario, Norm, Cris, all,

Curious about the Q0 language, and about whether Metamath can 'do Q0' just like it 'does set theory' in set.mm, I've started Q0 library in Methamath I wanted to share. I see this as a side project and don't plan to go very far, but wanted to share anyway.

First, where would this go to? I would like to be able to share and track changes like we do with set.mm in GitHub. Shall I create a different repository or would this fit into any existing one?
It's very small in size, so I'm attaching it to this mail to share a first version.

Second, I have a technical question. While I can write all proofs using the metamath program, MMJ2 refuses to apply ~ mpeq and related theorems ( ~ mpbi , ~ r-f ). Is there anything I'm doing wrong? Or are there maybe special $j primitives that MMJ2 requires to apply those theorems? This is quite a handicap because ~ mpeq is probably going to be needed in nearly every proof. I wanted to ask you before I give up or dig into MMJ2 to understand $j ' use.

I think I have a good starting point, but I see one caveat : the current ~ xa axiom states that variables can be of any type. I'm afraid this is maybe too flexible and could lead to contradictions, as one could use it twice in the same proof to give to one variable ` x ` two different types. This could actually not be a real issue, but anyway needs more thought.

BR,
_
Thierry


--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

[Thierry Arnoux]

Hi all,

I've been progressing at my own pace on the Q0 library, and I believe that with your help I solved the second issue with declaring the type of variables.

Since my initial construction showed that types of variables could not be declared in separated hypothesis, I've included them in the statements where they are required. At the same time, I'm dropping them again once a lambda expression is build with the variable used. These variable type declaration are otherwise carried over in proofs. The axioms I've designed to introduce them include distinct variable ($d) statements that ensure they follow the expected rules.

Declarations for the types of compound formulas remain in separated hypothesis. I believe this makes sense because proof statements could otherwise be cluttered with these type declarations, and this would require more manipulation axioms and longer proofs to manipulate.

I believe I found a sound basis and I'll now follow-up by on proving a few more theorems with this system.

You can see the changes I've done in GitHut: https://github.com/tirix/q0.mm

Regards,
_
Thierry

PS. I still don't know where to find ddt.mm, and I would still be curious to read it!

[Mario Carneiro]

On Tue, May 23, 2017 at 9:22 PM, Thierry Arnoux <thierry...@gmx.net> wrote:

Hi all,

I've been progressing at my own pace on the Q0 library, and I believe that with your help I solved the second issue with declaring the type of variables.

Interesting solution. Not what I expected, but I don't see any obvious exploits. Of course it always helps to prove to oneself (or others) a soundness theorem, something like "If |- vardecls | A : alpha, then every variable which appears in A has exactly one variable declaration associated to it". There is an obvious incompleteness issue with ds2/3t/f, since you can't permute any variables deeper in the declaration list, but these axioms are probably optional anyway (it is a conservative extension). In order to fully resolve this (to get all variable declaration permutations), you would need an additional judgement "V/ <=> W/" which states that two variable declaration lists are permutations of each other (which you can generate by reflexivity, transitivity, two-element swap, and appending an element to equivalent lists).

Since my initial construction showed that types of variables could not be declared in separated hypothesis, I've included them in the statements where they are required. At the same time, I'm dropping them again once a lambda expression is build with the variable used. These variable type declaration are otherwise carried over in proofs. The axioms I've designed to introduce them include distinct variable ($d) statements that ensure they follow the expected rules.

Declarations for the types of compound formulas remain in separated hypothesis. I believe this makes sense because proof statements could otherwise be cluttered with these type declarations, and this would require more manipulation axioms and longer proofs to manipulate.

This should be okay. If you read any papers on dependent type theory, you will notice this basic structure in the type judgements.

PS. I still don't know where to find ddt.mm, and I would still be curious to read it!

That's because I never released it. Anyway, you've convinced me that it's worth pursuing, so here it is:

https://github.com/digama0/dtt.mm

I make no guarantees about completeness. IIRC I stopped around the formalization of inductive types, and universes are not very well handled.

 

Mario

[Thierry Arnoux]

Hi all,

I've been progressing at my own pace on the Q0 library, and I believe that with your help I solved the second issue with declaring the type of variables.

Since my initial construction showed that types of variables could not be declared in separated hypothesis, I've included them in the statements where they are required. At the same time, I'm dropping them again once a lambda expression is build with the variable used. These variable type declaration are otherwise carried over in proofs. The axioms I've designed to introduce them include distinct variable ($d) statements that ensure they follow the expected rules.

Declarations for the types of compound formulas remain in separated hypothesis. I believe this makes sense because proof statements could otherwise be cluttered with these type declarations, and this would require more manipulation axioms and longer proofs to manipulate.

I believe I found a sound basis and I'll now follow-up by on proving a few more theorems with this system.

You can see the changes I've done in GitHut: https://github.com/tirix/q0.mm

Regards,
_
Thierry

On 20/05/2017 20:49, Thierry Arnoux wrote:

[Mario Carneiro]

(Thierry's email below has been waylaid by the Google group spam filter, and is apparently an old message - feel free to ignore it.)