Some questions

[Lakedaemon]

Hello

I'm not sure that I understand correctly type dependencies list are (what they really mean, how they somewhat do the job of metamath $d directives..., how to use them) Could you please answer some questions / confirm or infirm my understanding ?

A dependencies

1. In axiom ax_clab {x: set} (ph: wff x): $ x ec. {x | ph} <-> ph $;

a. {x: set} + ph wff x means that ph MAY depend on the FREE x setvar (not MUST) b. dependency list only concern setvars that are in the arguments of theorems/axioms/terms/definitions

2. In axiom ax_5 {x: set} (ph: wff): $ ph -> A. x ph $;

a. {x: set} + ph:wff means that ph MUST NOT have a free x inside b. which means that it somehow works like $d x, ph in metamath

3. In term term wal {x: set} (ph: wff x): wff

a. ph: wff x means that ph MAY depend on the FREE x setvar b) the resulting term DOES NOT/MUST NOT depend on x = ALL x are bound in the resulting term

B The Mario deduction technique

In my proof assistant, I will mostly let user write proofs of a new theorem with inference step1 -> step2 -> step3 And then the proof assistant will use previously proven deduction theorem variants of step1, step2, step3 to prove a deduction form and a closed form for this new theorem

Do you see a reason why it wouln't work ? Isn't this what metamathematician actually do ?

C. I'll probably use more nodes that the ones used in mm0 Notably :

• folding/unfolding n-uplets, f(a,b,c,d,e....n)
• to unfold/fold numbers
• to unfold matrices of numbers

Do you see a reason why it would be stupid ?

Best regards, Olivier

[Lakedaemon]

I was completely wrong. So I reread the specs

Then I thought phi x y was an upper bound to the dependencies can have

but that was wrong too

So I reread the specs (I'll manage to make it make sense eventually, by thinking about maths and how I would do it). My latest take :

• in a var A of a def, A:wff x y means that the setvar with name x and y are bound in A
• if that that had setvar z and w, those are free in the resulting term
• This sentence still doesn't make sense to me : v is free in a term foo x1 ... xn unless v is also substituted for bound variable xj and xi depends on xj

because, what is this xi ? why would it depend on xj ? if xi were to be substituted with xj ? But then it would depend if the sype of the resulting term foo w1...xn had a 'xi' part (or not) in the resulting type

Oh Well, I'll ponder further and try to find math examples to understand what you meant

This examples makes more sense to me :

then for the DEF foo a b P, we have FV(foo a b P) = (FV(P) \ {a}) u. {b}, so that if P := (a = b /\ a = c) then FV(P) = {a,b,c} and FV(foo a b P) = {b,c}.

So basically, for EACH regular var, you take all it's free vars BUT you remove those that have been bounded by stuff like wff x y AND you add to the resulting set of free vars the setvar that appear in the def's result

AND doted setvar cannot be a free var in the result (because they are not exposed ...)

Which somewhat explains def weu {x .y: set} (ph: wff x): wff = $ E. y A. x (ph <-> x =s y) $;

y SHOULD be bounded in the result (but there is no y in phi : wff x) because def wex {x: set} (ph: wff x): wff = $ ~(A. x ~ph) $;

Says that x is bounded in the result of a wex

Also Class do not have free setvar, those are only for wff Class are suposed to be used with x ec. A which turns them into a wff

Got to think some more to truely see if this is and it makes sense it or if I am wrong AGAIN

Now, in axiom axiom ax_gen {x: set} (ph: wff x): $ ph $ > $ A. x ph $; x becomes bounded in the result (though it wasn't in the first place)

And in axiom axiom ax_5 {x: set} (ph: wff): $ ph -> A. x ph $; x is not bounded in the result because a substitution can still change the value of any x that would be in the leftmost ph (while they are bounded in the rightmost ph)

The consideration about bounds only matter in definition checking and not for type checking (parsing of defs, axioms, theorems)

AND... I am wrong again because of this part :

def weu {x .y: set} (ph: wff x): wff = $ E. y A. x (ph <-> x =s y) $;

We can calculate the free variables of the expression recursively.

FV(ph) = {x}

Which says that x is a free var in ph (and not that any x in ph will be bounded) by weu...

Got te reread the specs and make sense out of it again...

Looking very hard at

def weu {x .y: set} (ph: wff x): wff = $ E. y A. x (ph <-> x =s y) $;

Theses sentences : the declaration term all {x: set} (ph: wff x): wff means that any occurrences of x in ph are bound by the term if it had type {x: set} (ph: wff): wff then x would not be free in all x ph unless it appears in ph

Imply that x can be free in ph AND DOESN'T need to be declared... hence the choice ph : wff or ph : wff x doesn't depend on the fact that x is free in ph or not

But FV(ph) = {x} then says that phi x brings the information that x is a known free variable in ph

...

Another try

More generally, v is free in a term foo x1 ... xn:

1. If v is substituted for bound variable xi, and foo has return type depending on xi, or
2. If v is free in the substitution for regular variable xi,
3. unless v is also substituted for bound variable xj and xi depends on xj

I might have understood it this time

1 -> the resulting type tells additonnal free variable for the result term( ):wff x y means that x and y are free in term (x, y, A, B, C) 2 -> term(A,B) has free vars of A union those of B 3 -> EXCEPT if like term {x:set} (ph:wff x) y e. A -> ph y -> x

x is bounded in ph but has been replaced by y so y which was free in y e. A has been bounded and doesn't appear in the free variable of the result

So in term (x, y, A, B, C) We get all the free var of A, B, C EXCEPT those that might have been bounded by the wff x y declarations and the substitutions and we add the free variables added by the result...

Let's check if it is correct (so ph:wff x y in the args means that x and y (substituted) are bounded in ph) and def:wff x y means that x and y are free in the result

[Lakedaemon]

They were upper bounds, damn...

The answer was phi : wff x y IS a wff that MAY USE the x and y free setvar and term() : wff x y means this term is a wff that MAY use x and y free setvar

Thanx to axiom 5 and gen & the distinc metamath for the understanding

In term all {x: set} (ph: wff x): wff phi MAY use x but it will be bound by the term because of x is bound {x:set}

in {x: set}: wff x > wff x where x > ph > result ph MAY use a free x that will get bound by the {x:set} BUT the term ensure that the result MAY have a free x (for exemple if there is an addition by x somewhere or a And x <=>.....)

In {x: set} (ph: wff): wff
ph MAY NOT use a free x AND the term ensure that the result won't "free" x

This ensures that the distinct x, ph condition in metamath ax_ Axiom ax-gen can be written in mm0 like axiom ax_gen {x: set} (ph: wff x): $ ph $ > $ A. x ph $;

(ph MAY have a dependency on x)

While metamath theorem Axiom ax-5 needs a distinct group x, ph and can dbe written in mm0 with axiom ax_5 {x: set} (ph: wff): $ ph -> A. x ph $;

Now, it makes sense for me, I'll be able to correctly use this.

Sorry for the rant

[Lakedaemon]

Finally found the answer