Re: [Metamath] Reorganizing the variable list; model theory

[Mario Carneiro]

On Mon, Jan 18, 2016 at 2:49 PM, Norman Megill <n...@alum.mit.edu> wrote:

(in an earlier post you wrote:)
>In fact, it may be necessary to wait for this before reorganizing, >because unless you have a tool for fixing all the proofs after such a >change I'm not sure how it can be done.

Suppose we want to change the order of hypotheses for theorem xyz.  The way I do it now is to make a copy of it then rename the original and its references to xyzOLD.  The copy becomes the new xyz after getting its proof to work locally (hypotheses can be swapped safely if the proof is saved as /normal).  Then we go into MM-PA for each proof using xyzOLD and do 'minimize_with xyz/allow_growth' to replace each reference to xyzOLD with xyz.

That actually wouldn't work in this case, because a change to $f order causes all theorems to have their hypotheses reordered, and there is no way to specify a different order. For example, if we have

$v x y $.
vx $f set x $.
vy $f set y $.
weq $a wff x = y $.

then weq will have the hypothesis order [vx, vy]. If we try to make a copy of it -

weqOLD $a wff x = y $.

this will also have hypothesis order [vx, vy]. Changing the order of vx and vy will cause both axioms to have their hypothesis list reordered, you can't have both in the same database (except, ironically, if you use local variables). Alternatively, you could use

weqOLD $a wff y = x $.

which would have the desired effect, but such a redefinition requires a lot more "creativity" in selecting variable names that have the desired relative orders, and would not be much better than /explicit.

I suppose it's (far) too late to change this, but I would have preferred that $f hyps come in the order they show up in the expression itself, that is, something like wbr $a wff A R B $. should have its arguments come in the order [cA, cR, cB]. If there are $e hyps then it would be the order that variables show up in text order, i.e. for

eqtrd.1 $e |- ( ph -> A = B ) $.

eqtrd.2 $e |- ( ph -> B = C ) $.

eqtrd $p |- ( ph -> A = C ) $.

we would have arguments [wph, cA, cB, cC]. There is of course the present advantage that $f hyps can be freely reordered, and a $a or $p will not change its order unless its math string changes. It also means that a grammar parse comes in basically infix notation, meaning that an expression ( 1 * ( 2 ( f ` 3 ) 4 ) ) has leaf nodes in the order [1, *, 2, f, 3, 4], which you would expect, rather than the current non-obvious order [1, 2, 4, 3, f, *]

OK, in order to simplify writing parsers, we can add to the spec that redeclaration of a variable type ($f) must match any previous $f for that variable.  No database violates this now AFAIK, and if does it can be easily fixed.

As for Appendix C, it assumes that the database has been pre-processed into abstract "frames" (p. 164 bottom) where each variable used in the frame is assigned a unique type ($f).  Since each statement's frame is self-contained, I don't think it matters if a variable is assigned a different type in some other frame.  It is possible that I am overlooking something.

This is true. But it leaves a "variable" ($v) in a strange position, since it really isn't meaningful without an $f to go with it. This passes directly to the theoretical framework of Appendix C; I once tried to define the subset of EX_C that represents provable formulas, but I can't without an assignment of all the variables to typecodes, i.e. a frame, which makes it sound like a local property when it's not. Here is an alternative definition of appendix C with a global type function.

> Let CN be a set, the set of constants, and VR be another set disjoint from CN, denoting the variables. Let Type be a function from VR to CN, this maps a variable to its typecode. Then define SM = CN u. VR, EX = U_ n e. om SM^n, EX_C = { e e. EX | |e| > 0 /\ e_0 e. CN }, DV = { x C_ VR | |x| = 2 }, VT = { <Type(v), v> | v e. VR }. The function V(E), where E e. EX, is V(E) = VR i^i ran E, and V(S) for S C_ EX is V(S) = U_ e e. S V(e).

> A substitution is a function σ : EX -> EX such that σ(<c>) = <c> for c e. CN and σ(a concat b) = σ(a) concat σ(b).

> A pre-statement is a tuple <D, H, A> with D C_ DV, H C_ EX_C is finite, and A e. EX_C. The reduct of <D, H, A> is <D_M, H, A> where D_M = { x e. D | x C_ V(H u. {A}) }, and a statement is the reduct of some pre-statement.

> A formal system is a tuple <CN, VR, Type, Γ> where Γ is a set of statements. The closure of a set H C_ EX_C relative to D is the smallest set C such that H u. VT C_ C, and for every <D', H', A'> e. Γ and every substitution σ, if A. h e. (H' u. VT) σ(h) e. C and A. {a,b} e. D' A. c e. V(σ(<a>)) A. d e. V(σ(<b>)) {c,d} e. D, then σ(A') e. C. A pre-statement <D, H, A> is provable if A is in the closure of H relative to D, and a statement is provable if it is the reduct of a provable pre-statement. The universe of a formal system is its set of provable statements.

I reiterated most of the definitions unchanged, so that it is clear what is and is not changed. The difference is Type, which is now a global function on VR, and VT replaces the local variable T in pre-statements. In particular, we can make the following definition:

> The distinct universe of a formal system is the closure of the empty set relative to DV.

This is the set of expressions derivable in a theorem with no hypotheses where all variables are assumed distinct.

I'll show a bit more work I've done on the model theory of metamath, which is now easier to state with a global type function.

> Let TC be the set { A_0 | <D, H, A> is provable }. This is the set of typecodes (in set.mm, this would be {set, class, wff, |-}). Fix a function OV on TC, which represents the universe for each typecode. (In set.mm, OV(class) is roughly the ZFC universe, OV(wff) is {0,1}, OV(|-) is {1}, and OV(set) is {v0, v1, ...}.) Let OM be the set of object morphisms, that is functions τ on VR such that τ(v) e. OV(Type(v)) for all v e. VR. (This can be thought of as a variable assignment, but to objects of the universe, not expressions.)

> A model of a formal system is a tuple <OV, Δ, η> where Δ is a symmetric relation on the disjoint union of OV(c), and η_τ is a OM-indexed family of partial function on EX_C such that for all τ e. OM:
> * for all e e. EX_C, if η_τ(e) is defined then η_τ(e) e. OV(Type(e_0)),
> * η_τ(<Type(v), v>) = τ(v) for v e. VR, and

> * For each <D, H, A> e. Γ, if τ(a) Δ τ(b) for all {a,b} e. D and η_τ(h) is defined for all h e. H, then η_τ(A) is defined.

> Additionally, the η_τ functions are connected by the substitution principle: For any substitution σ, η_τ(σ(e)) = η_σ(τ)(e), where σ(τ) is defined such that σ(τ)(v) = η_τ(σ(<Type(v), v>)).

Just a little teaser, I hope to get a paper out of the above. As an example for prop calc, we have OV = {wff -> {0, 1}, |- -> {1}} (the universe of wffs is two elements), Δ = (/) (doesn't matter, since wff $d's don't occur), and η_τ is the smallest function such that η_τ("wff v") = τ(v) for each wff variable v, and η_τ("wff -. ph") = 1 - η_τ("wff ph") and η_τ("wff ( ph /\ ps )") = η_τ("wff ph") * η_τ("wff ps") for any wff strings ph, ps. Additionally, η_τ("|- v") = 1 if η_τ("wff v") = 1, otherwise it is undefined.

 

As for otherwise allowing local scopes for $v and $f, I assume you find that ok?  Although it isn't needed now, I'm anticipating a hypothetical case with hundreds of dummy variables whose overhead we don't want to affect the remainder of set.mm.

This should be fine, as it doesn't affect the theoretical results above.

Mario

[Norman Megill]

Sorry, I was hasty and was thinking of the swapping of local $e's
affecting one theorem, not $f's that affect many theorems. One way to
do it is as follows.

Suppose we want to move 'vq $f set q' somewhere else. Rename vq, q to
vqOLD, qOLD (throughout set.mm) then insert

$v q $.
vq $f set q $.

where you want the vq to move to.

Suppose abc is the first theorem referencing vqOLD. Make a copy of
theorem abc and rename the original to abcOLD. Save the proof of the
new abc in /normal format then change qOLD to q and vqLD to vq. Then
change all references to abcOLD to abc by using
'minimize.../allow_growth' as I described before.

Repeat this all the way down until no more theorems reference vqOLD.

Of course, this is a too large a task to do by hand, and it would have
to be automated with a somewhat complex script.

Maybe waiting for the /explicit proof format is the practical thing to
do. I'll move it up on my to-do list.

Norm

[Norman Megill]

On 1/19/16 6:32 PM, Norman Megill wrote:
> Maybe waiting for the /explicit proof format is the practical thing to
> do. I'll move it up on my to-do list.
>
> Norm

Version 0.123 of the metamath program adds a new /explicit proof format
that allows hypotheses ($e, $f) in set.mm to be reordered without any
side effects. It is available here:
http://us2.metamath.org:88/index.html#mmprog

Specifically, the following features were added to metamath.exe:

1. The /packed qualifier is now available for 'show [new_]proof' and
'save [new_]proof'. (Originally it was available, but undocumented, for
'save'.)
2. A new /explicit qualifier is available with /normal and /packed
formats in 'show' and 'save' proofs.

The current /normal proof is a list of labels. The /packed format is an
extension to /normal that adds local labels "<nn>:" to subproofs that
can be referenced later in the proof without repeating them. The
/explicit format is an extension to /normal and /packed that puts a
target label "<target>=" in front of the (source) label in each step.
This target label overrides the order in which hypotheses are declared.

The /explicit formats will let you rearrange the ordering of $f and $e
hypotheses in the database without affecting any proofs.

The /packed and /explicit qualifiers aren't documented in the help yet.
The following examples illustrate all current proof formats:

MM> sh p ru/compressed
Proof of "ru":
---------Clip out the proof below this line to put it in the source file:
( vy cv wnel cab cvv wcel wn wceq wex wb wal pm5.19 df-nel
eleq12d notbid
eleq1 id syl5bb mtbir bibi12d a4v mto abeq2 nex isset mpbir )
ACZUHDZAEZF

DUJFGZHUKBCZUJIZBJUMBUMUHULGZUIKZALZUPULULGZUQHZKZUQMUOUSABUHULIZUNUQ ...

MM> sh p ru/normal
Proof of "ru":
---------Clip out the proof below this line to put it in the source file:
vx cv vx cv wnel vx cab cvv wnel vx cv vx cv wnel vx cab cvv wcel
wn vx
cv vx cv wnel vx cab cvv wcel vy cv vx cv vx cv wnel vx cab wceq...

MM> sh p ru/normal/explicit
Proof of "ru":
---------Clip out the proof below this line to put it in the source file:
vx=vx cA=cv vx=vx cB=cv wph=wnel vx=vx cA=cab cB=cvv wph=wnel
vx=vx cA=cv
vx=vx cB=cv wph=wnel vx=vx wcel.cA=cab wcel.cB=cvv wph=wcel
wps=wn vx=vx
cA=cv vx=vx cB=cv wph=wnel vx=vx wcel.cA=cab wcel.cB=cvv wph=wcel
vx=vy
wceq.cA=cv vx=vx cA=cv vx=vx cB=cv wph=wnel vx=vx wceq.cB=cab ...

MM> sh p ru/packed
Proof of "ru":
---------Clip out the proof below this line to put it in the source file:
vx 1:cv 1 2:wnel vx 3:cab cvv wnel 3 cvv 4:wcel wn 4 vy 5:cv 3
6:wceq vy
wex 6 vy 6 1 5 7:wcel 2 8:wb vx 9:wal 9 5 5 10:wcel 10 11:wn
12:wb ...

MM> sh p ru/packed/explicit
Proof of "ru":
---------Clip out the proof below this line to put it in the source file:
vx=vx 1:cA=cv cB=1 2:wph=wnel vx=vx 3:cA=cab cB=cvv wph=wnel
wcel.cA=3
wcel.cB=cvv 4:wph=wcel wps=wn wph=4 vx=vy 5:wceq.cA=cv wceq.cB=3
6:wph=wceq vx=vy wps=wex wph=6 vx=vy wph=6 wcel.cA=1 wcel.cB=5
7:wph=wcel
wps=2 8:wph=wb vx=vx 9:wps=wal wph=9 wcel.cA=5 wcel.cB=5
10:wph=wcel...

Here are the size and proof verification speed impacts of these formats
for set.mm (when all proofs are saved in the format):

/compressed: 'verify proof *' 14s, file size 28MB
/normal: 'verify proof *' 118s, file size 148MB
/normal/explicit: 'verify proof *' 4055s, file size 302MB
/packed: 'verify proof *' 20s, file size 36MB
/packed/explicit: 'verify proof *' 39s, file size 64MB

The 'verify proof *' time for /packed/explicit may vary depending on how
much hypothesis rearranging was done to in the database. The 39s
assumes no hypotheses were rearranged. Ordinarily, after editing the
hypothesis order as desired in the database, we would then 'save proof
*/compressed'.

The long run time for /normal/explicit might be improved somewhat with
more efficient code, but I don't think it will be used much so it
shouldn't matter.

Norm