Re: unbundling set.mm

[Mario Carneiro]

Cross-posting to metamath list with permission:

On Mon, Feb 15, 2016 at 12:16 PM, Norman Megill <n...@alum.mit.edu> wrote:

Hi Mario,

I did an experiment that seems applicable to what we discussed last summer, which is to maximally unbundle all set variables for easier automated translation of set.mm to another FOL language.  I think you were experimenting with that in ax-7d through ax-11d.

I made every set variable in set.mm distinct from every other globally, for all axioms and all theorems, and ran 'verify proof *' to see what failed.  I ignored errors caused by $d's on weq, wel, wsb (due to the global scope of my new $d's).  There were 731 error messages in 424 proofs, all of them with "variable ... in common" type failures of course.  There were 77 previously-bundled axioms and theorems whose $d's violations caused these errors.

To fix these, we would provide alternate versions of the 77 violated statements, reproved with bundled variables made the same, such as '-. A. x -. x = x` (call it say ax9-same-xy) to eliminate the ax-9 violations.  Then we would do 'minimize ax9-same-xy/allow' or equivalent to replace ax-9 in proofs where it now causes a failure.  (For this to work always, I would have to add an option to 'minimize' to ignore $d failures when there are multiple previously-bundled statements causing them.)

Some cases, like ax9-same-xy, can be proved as theorems; others might need additional axioms.

So unless I'm overlooking something, it shouldn't be an insurmountable task to obtain universal $d's on set variables.

Here are the 77 bundled statements that cause failures when universal $d's are added, sorted in set.mm order:

ax-8 ax-13 ax-14 ax-12o ax10lem27 ax-9 hbequid ax67 ax467 19.2 ax-9o equtr equequ1 equequ2 elequ1 elequ2 hbae hbae-o hbnae hbnae-o hbnaes dral2 dral2-o drex2 cbv1 drsb1 sbequ12 sbequ5 aev aev-o drsb2 a16gb df-clab hbab eqsb3 hbeq hbel cbvral2v hbeqd hbned hbsbcg sbcabel copab zfrepclf zfpair2 elopab epel dfid3 djudisj xporderlem rdglem1 eqerlem cbvixp pwfilem fin23lem32 suprlub suprleub infmrgelb btwnz isfild metequiv evthicc norm1exi norm1hex elmzpcl ax4567 bnj1156 bnj1309 bnj1307 bnj1326 bnj1329 bnj1418 ax9lem1 cdlemk22 erngdvlem4 erngdvlem4-rN cdlemn2a

I would not want to do this to the standard set.mm but instead to a modified version specifically for a project requiring unbundling.  It might be possible to keep it in sync with 3-way merges.

As for wff and class variables, I don't know too much about what features other proof languages have, but I think some (maybe Isabelle?) can have predicates and terms with fixed arguments, such as phi(x) shown for ax-sep in http://us.metamath.org/mpegif/ax-sep.html .

Feel free to post publicly if you want.

Norm

On Mon, Feb 15, 2016 at 3:16 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 2/15/16 1:53 PM, Mario Carneiro wrote:

Could you make a branch off of develop for this test? That way we can

play around with it and if necessary split it off to its own file later.

It is a rather trivial change, it just adds 3 $d statements:

$d x y z w v u t $. above wal
$d f g x y z w v u t $.  in cbvex4v (for the local f,g)
$d a b c d e f g h i j k l m n o p q r s t u v w x y z $. above df-clab

A final version would omit $d's on wel, weq, wsb, maybe by moving those theorems up.

On Mon, Feb 15, 2016 at 6:33 PM, Norman Megill <n...@alum.mit.edu> wrote:

Question:  Would this actually be used, or is it just hypothetical? In particular, are there other unresolved issues that would prevent the translation(s) you have in mind?  I recall we had talked about ax-gen and others where bundling can occur as a side effect of substitutions.

TBH I haven't thought about this much since our last conversation, but the "Models" paper puts this on much stronger theoretical footing. It would be nice to have a generic "bundling" theorem, which for example takes "-. A. x -. x = x" and "-. A. x -. x = z" with $d x z, and appropriate substitutions showing that the first one is equivalent to "-. A. x -. x = y" under the assumption "A. x x = y" and the second expression is also equivalent to this under the dvelim assumptions(?) for substituting z for y under "-. A. x x = y". I'm not giving an exact statement because I'm not sure what the proper idiom is in this case, perhaps you have a better idea.

I did this experiment because it was quick and easy, just to get an idea of what would be involved, and was pleasantly surprised that it wasn't as bad as I feared.  But it would still take some days of time to do the work, which I wouldn't want to do if it will never be used for anything.  Or perhaps it would make sense to postpone it until we're closer to using it and understand the issues more clearly.

 Postponing is probably the best course of action. IIRC this was discussed in conjunction with a possible export from Metamath to OpenTheory or MMT+LF. I will try to go to CICM 2016 in June with the "Models" paper, and if I see Florian we will have another discussion about this. The exact problem points will be identified once a full translation is attempted. In fact, since the Models paper supports the meta-level directly, it might actually support a direct embedding of Metamath in LF, with $d's and all.

A while ago Florian sent me this mockup Metamath theory file:

https://gl.mathhub.info/MMT/experimental/blob/master/source/logics/metamath.mmt

Note in particular the type of the forall: (set -> wff) -> wff. This makes sense if wffs are explicitly parameterized (the input there is not a wff but a function from set (the model) to wff (the bools)), but in our case they are not, and instead the type of forall for us is (set X. wff) -> wff. Here set is the collection of *set variables* (the v0, v1, ... set), while wff is the collection of functions from variable assignments to bools. (The paper discusses this construction in detail.) So my version of the file (ASCIIfied for your reading pleasure) would look like this:

  // set variables
  set: type
  // well-formed formulas
  wff: type

  // all variables (disjoint union of set and wff)
  var: type
  set-var: set => var
  wff-var: wff => var

  // connectives
  weq: set => set => wff # 1 = 2 prec 10
  wel: set => set => wff # 1 e. 2 prec 10
  wi: wff => wff => wff  # 1 -> 2 prec 5
  wn: wff => wff         # -. 1   prec 5
  wal: wff => set => wff # A. 2 1 prec 5

  // disjoint variable pair productions
  djset: set => var => type # $d 1 2 prec 0

  proof: wff => type     # |- 2 prec 0

  // prop calc
  ax-1: {ph:wff,ps:wff} |- ( ph -> ( ps -> ph ) )
  ax-2: {ph:wff,ps:wff,ch:wff} |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
  ax-3: {ph:wff,ps:wff} |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
  ax-mp: {ph:wff,ps:wff} |- ph => |- ( ph -> ps ) => |- ps

  // Example proof
  a1i: {ph:wff,ps:wff} |- ph => |- ( ps -> ph )
     = [ph][ps][H] ax-mp ph (ps -> ph) H (ax-1 ph ps)

  // pred calc
  ax-5: {ph:wff,ps:wff,x:set} |- ( A. x ( ph -> ps ) -> ( A. x ph -> A. x ps ) )
  ax-6: {ph:wff,x:set} |- ( -. A. x ph -> A. x -. A. x ph )
  ax-7: {ph:wff,x:set,y:set} |- ( A. x A. y ph -> A. y A. x ph )
  ax-gen: {ph:wff,x:set} |- ph => |- A. x ph
  ax-8: {x:set,y:set,z:set} |- ( x = y -> ( x = z -> y = z ) )
  ax-9: {x:set,y:set} |- -. A. x -. x = y
  ax-11: {ph:wff,x:set,y:set} |- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
  ax-12: {x:set,y:set,z:set} |- ( -. x = y -> ( y = z -> A. x y = z ) )
  ax-13: {x:set,y:set,z:set} |- ( x = y -> ( x e. z -> y e. z ) )
  ax-14: {x:set,y:set,z:set} |- ( x = y -> ( z e. x -> z e. y ) )
  ax-17: {ph:wff,x:set} $d x ph => |- ( ph -> A. x ph )

  // Tricky: forget dummy vars. The hypothesis "fresh x s" means that x is not
  // any of the set variables in s.
  
  // Inductive definition for a list of variables
  vars: type
  vars0: vars                 # [] prec 10
  varsp1: var => vars => vars # 1 . 2 prec 10

  // I omit the inductive definitions of these operations on vars, treated as
  // sets of elements
  in: var => vars => type
  subset: vars => vars => type
  union: vars => vars => vars

  varsin: var => vars
  varsin-set: {x:set} varsin x = x . []
  varsin-weq: {x:set,y:set}  varsin (x = y) = (varsin x) union (varsin y)
  varsin-wel: {x:set,y:set}  varsin (x e. y) = (varsin x) union (varsin y)
  varsin-wi: {ph:wff,ps:wff} varsin (ph -> ps) = (varsin ph) union (varsin ps)
  varsin-wn: {ph:wff}        varsin (-. ph) = varsin ph
  varsin-wal: {ph:wff,x:set} varsin (A. x ph) = (varsin x) union (varsin ph)

  // deduce disjointness
  dj: {x:set,ph:var} ({a:var} a in (varsin ph) => $d x a) => $d x ph

  fresh: set => vars => type
  freshdj: {x:set,y:var,s:vars} fresh x s => y in s => $d x y
  
  forget: {ph:wff,x:set,s:vars} not (x in s) =>
    ((varsin ph) subset s) => (fresh x s => |- ph) => |- ph

More generally, this is a basic structure for embedding Metamath in a dependent type theory like LF, Coq or Lean. (It does not work for simple type theories such as OpenTheory or hol.mm, at least not without modification.)

Mario

[fl]

I can't resist. I didn't know Lean. I've come across this site. This person would use set.mm, he would know the conjecture 

he is trying to prove is not a theorem :-)

http://cstheory.stackexchange.com/questions/32357/whats-wrong-with-this-lean-proof

-- 

FL

[fl]

 

I can't resist. I didn't know Lean. I've come across this site. This person would use set.mm, he would know the conjecture 

he is trying to prove is not a theorem :-)

The explanation of the error behind is a bit confused I think. He should explain that A. is a sort of gigantic /\  over the universe.

x = 0 -> A. x = 0 means

x = 0 -> ( 0 = 0 /\ 1 = 0 /\ ... )

                             ^ this wrong

     then  |-----------------------------| all this wrong ( table of truth of /\ )

|-------------------------------------------| all this wrong ( table of truth of -> )

-- 

FL

[Mario Carneiro]

Strictly speaking, this is not necessarily true, and to make this approach make rigorous sense would require infinitary logic. In particular, Lean (usually) uses constructive logic, so a simple truth table may not always be enough to prove a tautology.

Your breakdown assumes that x = 0 -> F. evaluates to F., but if the antecedent is also false it might still be provable. What I think you wanted to write was

0 = 0 -> ( 0 = 0 /\ 1 = 0 /\ ... )

and since the left side is 0 = 0 which is true and the right side includes 1 = 0 which is false, the overall proof is false.

In Lean, they use dependent types for this. The type of the proposed lemma is P. (x:A) (p x -> P. (x':A) p x'), where P. (x:A) B(x) is the dependent type operator, an analogue of ZFC's X_ x e. A B(x), and A -> B is a shorthand for P. (x:A) B, that is, the set of functions from A to B. Thus the lemma is a function which takes three arguments x:A, H:(p x), x':A and produces an element (or proof) of type (p x'). (Strictly speaking there are also two more "hidden" arguments, A:Type and p:A -> Prop, which are treated as constants for the rest.)

Of course, the author is arguing that such a function can't exist, so he uses it to derive a falsehood, which in lean is represented by a member of the empty type.

lemma inconsistent : false :=
  assert h : 0 == 0 → (∀ x, x == 0), from (lma num (λ n, n==0) 0),
  assert e : 1 == 0, begin
    refine (h _ 1), 
    reflexivity
  end,
  show false, by cases e

In the first step, the function lma is applied to A=num (natural numbers), p = (n |-> n = 0), and x = 0. This produces a function from H:(0 = 0) and x':num to the type (x' = 0), that is, a member of the type (0 = 0 -> A. x, x = 0), which they call h.

Applying this to arguments _ and 1 (where the _ is a signal for Lean to go synthesize an element t:(0 = 0), by reflexivity), the resulting value is (h _ 1):(1 = 0). Finally "by cases" is used as a proof search mechanism which can work with sets with decidable equality, such as the naturals, in order to synthesize a member u:(1 =/= 0), which is the same as u:(1 = 0 -> false), and applying u to (h _ 1) gives a member of false.

Behind the scenes, Lean is calculating proof terms for the type inference steps, which are for the most part done in entirely deterministic ways. If you ask it, it will supply the fully expanded term after this "elaboration" step, which is where proof output would come from, if it were to be done. My future work will likely take me in the direction of Lean, because the person who is likely to be my advisor come fall is on the Lean theorem proving group.

[Mario Carneiro]

I tried this proof out in the online Lean interpreter. The "tactic" parts of the proof can be mostly eliminated, to get

lemma inconsistent : false :=
  assert e : 1 = 0, from
    lma num (λ n, n = 0) 0 (eq.refl 0) 1,
  by cases e

where the original begin...end block was being used to synthesize the term (eq.refl 0) : (0 = 0). (This is the equivalent to metamath's "cc0 eqid" proof of "|- 0 = 0".) There still remains the "by cases" tactic, though; eliminating this as well is a bit uglier since it shows more of the underlying recursors for the inductive type "num":

lemma inconsistent : false :=
eq.cases_on (lma num (λ n, n = 0) 0 (eq.refl 0) 1)
  num.no_confusion (eq.refl 0)

The types of the theorems used here are:

eq.cases_on : Π {A : Type} {a : A} {C : A → Type} {a_1 : A}, a = a_1 → C a → C a_1
eq.refl : ∀ {A : Type} (a : A), a = a
num.no_confusion : Π {P : Type} {v1 v2 : num}, v1 = v2 → num.no_confusion_type P v1 v2

The {} arguments are automatically inferred, which means that even the expanded proof term above is hiding some things. Here it is again with all arguments explicit:

lemma inconsistent : false :=
@eq.cases_on num 1 (λ (t : num), 0 = t → false) 0 (lma num (λ (n : num), n = 0) 0 (@eq.refl num 0) 1)
    (@num.no_confusion false 0 1)
    (@eq.refl num 0)

In other words, the argument applies eq.cases_on to the proposition (λ (t : num), 0 = t → false), first plugging in 1 and then 0, using the proof of 0 = 1. In the first case we get 0 = 1 → false, which is provable by num.no_confusion (which is the Lean version of one of the Peano axioms - 0 is not a successor), and in the second case we get 0 = 0 → false, and since (@eq.refl num 0) proves 0 = 0, we show false.

Finally, let me point out that the whole approach is quite unnecessarily overcomplicated, and there is a much simpler direct proof:

lemma inconsistent : false := lma Prop id true trivial false

Here we instantiate the lemma with the type Prop and the identity function, so that (lma Prop id) maps x:Prop, H:x, x':Prop to an element of x'; then we take x=true, H=trivial (the proof of true), and x'=false to get an element of false.

Mario

[fl]

Strictly speaking, this is not necessarily true, and to make this approach make rigorous sense would require infinitary logic.

 

 

In particular, Lean (usually) uses constructive logic, so a simple truth table may not always be enough to prove a tautology.

 

 

In his mind it was a proposition of FOL. But I agree that my explanation has as little rigour as his own.

 

Your breakdown assumes that x = 0 -> F. evaluates to F., but if the antecedent is also false it might still be provable.

 

You are right but if it is a tautology it needs to be true for every valuation then you take 0 = 0 for the antecedent as you say then.

 

--

FL

[fl]

 

 But I agree that my explanation has as little rigour as his own.

 

 

The idea of gigantic /\ peculiarly. 

 

--

FL

[Mario Carneiro]

This is logically related to the "metamath zero" thread (https://groups.google.com/d/msg/metamath/raGj9fO6U2I/dmVwJJcjCQAJ), but I want to re-characterize it in pure metamath terms. A while ago Norm did an experiment on the consequences of unbundling all theorems (in the thread I'm replying to). I have some more data to report on that front, now that I am getting closer to implementing a translation that includes proofs, not just statements. The following is a list of all "shadow copies" of statements that would be required to translate bundled theorems into their unbundled counterparts. For example, equtrr has [[0,1,0],[0,1,1]] written after it, meaning that of its three set variables x,y,z, they can be merged in the pattern x,y,x and x,y,y to obtain a new version of the theorem, which would be a substitution instance in metamath but is a separate theorem in unbundled land. This list includes all transitively collapsed theorems, i.e. applying the same proof for a collapsed theorem will probably involve calling other collapsed theorems, causing those to be generated as well.

Should we do something about these theorems, or leave them as is? Some of them are recognizable as theorems that are really substitution instances in FOL, like ax-7, but whenever binders get involved it's not so easy. This at least justifies the sense that although unbundling causes exponential blowup *in principle*, in practice almost all of the theorems don't do anything special with bundling. This list is longer than the 77 theorems in Norm's list, because I'm working transitively, meaning I see both the first layer DV errors as well as all the errors that happen when you fix those, and so on.

220 bundled theorems, 299 total copies
2exbidv          [[0,0]]
exlimivv         [[0,0]]
weq              [[0,0]]
wsb              [[0,0]]
df-sb            [[0,0]]
sbequ2           [[0,0]]
sb1              [[0,0]]
ax-7             [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
equcomi          [[0,0]]
equcom           [[0,0]]
equcoms          [[0,0]]
equtr            [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
equtrr           [[0,1,0],[0,1,1]]
equequ1          [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
equequ2          [[0,0,0],[0,1,0],[0,1,1]]
equtr2           [[0,0,1]]
ax13b            [[0,0,1],[0,1,0]]
wel              [[0,0]]
ax-8             [[0,1,0],[0,1,1]]
elequ1           [[0,1,0],[0,1,1]]
ax-9             [[0,1,0],[0,1,1]]
elequ2           [[0,1,0],[0,1,1]]
ax13dgen1        [[0,0]]
ax-11            [[0,0]]
hbal             [[0,0]]
hbald            [[0,0]]
ax-12            [[0,0]]
nfal             [[0,0]]
nfald            [[0,0]]
stdpc7           [[0,0]]
sbequ1           [[0,0]]
sbequ12          [[0,0]]
sbequ12r         [[0,0]]
ax-13            [[0,0,1]]
ax13v            [[0,0,1]]
axc9lem1         [[0,0,1]]
axc9lem2         [[0,0,1]]
a6e              [[0,0]]
equs4            [[0,0]]
axc9lem3         [[0,0,1]]
dveeq2           [[0,0,1]]
dveeq1           [[0,0,1]]
nfeqf            [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
axc9             [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
axc9lem3OLD      [[0,0,1]]
axc9lem5OLD      [[0,0,1]]
ax13             [[0,0,1],[0,1,0]]
axc11nlem1       [[0,0,1]]
axc11nlem2       [[0,0,1]]
axc112           [[0,0]]
axc11n           [[0,0]]
axc11nlem5OLD    [[0,1,0,2]]
aecoms           [[0,0]]
naecoms          [[0,0]]
axc11            [[0,0]]
hbae             [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
nfae             [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
hbnae            [[0,1,0],[0,1,1]]
nfnae            [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
aevlem1          [[0,1,0,1],[0,1,0,2],[0,1,2,0]]
axc16g           [[0,1,0],[0,1,1]]
aev              [[0,1,0,0,2],[0,1,1,1,2],[0,1,2,0,2],[0,1,2,2,0],[0,1,2,2,3]]
a16nf            [[0,1,0]]
a16gb            [[0,1,0]]
dral2            [[0,0,1],[0,1,0]]
dral1            [[0,0]]
drex1            [[0,0]]
drex2            [[0,0,0],[0,1,0]]
drnf1            [[0,0]]
drnf2            [[0,1,0]]
nfald2           [[0,0]]
dvelimf          [[0,0,1],[0,1,0]]
dvelimdf         [[0,0,1],[0,1,0]]
ax12v2           [[0,0,1]]
ax12a2           [[0,0,1]]
axc15            [[0,0]]
equs5            [[0,0]]
sb2              [[0,0]]
sb4              [[0,0]]
sbequi           [[0,1,0],[0,1,1]]
sbequ            [[0,1,0],[0,1,1]]
drsb1            [[0,1,0]]
drsb2            [[0,1,0],[0,1,1]]
sbequ5           [[0,1,2,1]]
nfsb4t           [[0,1,0]]
sbcom3           [[0,1,0]]
nfsbd            [[0,1,0]]
ax-c10           [[0,0]]
ax-c11           [[0,0]]
ax-c9            [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
aecom-o          [[0,0]]
aecoms-o         [[0,0]]
hbae-o           [[0,1,0],[0,1,1]]
axc711           [[0,0]]
axc5c711         [[0,0]]
hbnae-o          [[0,1,0],[0,1,1]]
dral2-o          [[0,1,0],[0,1,1]]
aev-o            [[0,1,2,2,0]]
df-clab          [[0,0]]
drnfc1           [[0,0]]
nfabd2           [[0,0]]
nfabd            [[0,0]]
dvelimdc         [[0,0,1]]
dvelimc          [[0,0,1]]
nfcvf            [[0,0]]
nfcvf2           [[0,0]]
cbvral2v         [[0,1,2,0]]
dfsbcq2          [[0,0]]
sbsbc            [[0,0]]
nfsbcd           [[0,0]]
nfcsbd           [[0,0]]
nfcsb            [[0,0]]
copab            [[0,0]]
df-opab          [[0,0,1]]
ax-pr            [[0,0,1,2]]
zfpair2          [[0,0]]
elopab           [[0,0]]
epel             [[0,0]]
dfid3            [[0,0]]
djudisj          [[0,0]]
fmpt2d           [[0,0]]
xporderlem       [[0,1,2,3,2,3]]
rdglem1          [[0,1,2,0,3,4]]
eqerlem          [[0,1,2,2]]
pwfilem          [[0,0,1]]
fin23lem28       [[0,1,2,3,4,5,2,6,7]]
fin23lem29       [[0,1,2,3,4,5,2,6,7]]
fin23lem30       [[0,1,2,3,4,5,2,6,7]]
fin23lem31       [[0,1,2,3,4,5,2,6,7]]
fin23lem32       [[0,1,2,3,4,5,6,2,7,8,9]]
suprlub          [[0,1,1]]
suprleub         [[0,1,0],[0,1,1]]
infmrgelb        [[0,1,0],[0,1,1]]
btwnz            [[0,0]]
isfild           [[0,1,0]]
metequiv         [[0,1,2,2,1]]
evthicc          [[0,1,0,1],[0,1,2,1]]
norm1exi         [[0,0]]
norm1hex         [[0,0]]
fcobijfs         [[0,0,1]]
mzpclval         [[0,1,0,1,1,2]]
elmzpcl          [[0,1,0,1,1]]
axc5c4c711       [[0,0]]
ovmpt3rab1       [[0,1,2,1,3,4]]
elovmpt3rab1     [[0,1,2,1,3,4]]
2wlkeq           [[0,0]]
bnj1307          [[0,1,1,2]]
bnj1326          [[0,1,1,2,3]]
bnj1418          [[0,0]]
bj-hbaeb         [[0,1,1]]
dvelimhwNEW11    [[0,0,1]]
axc9lem2wAUX11   [[0,0,1,2]]
axc9lem4wAUX11   [[0,0,1,2]]
axc9lem6NEW11    [[0,0,1,2],[0,1,0,2]]
axc9lem7NEW11    [[0,0,1,2],[0,1,0,2]]
axc9NEW11        [[0,1,0],[0,1,1]]
dvelimvNEW11     [[0,0,1]]
dveeq2NEW11      [[0,0,1]]
dveeq1NEW11      [[0,0,1]]
ax6NEW11         [[0,0]]
axc10NEW11       [[0,0]]
a6eNEW11         [[0,0]]
axc11nlem4NEW11  [[0,0,1]]
axc11nlem5NEW11  [[0,0,0,1],[0,1,0,1],[0,1,0,2]]
axc11nNEW11      [[0,0]]
aecomNEW11       [[0,0]]
aecomsNEW11      [[0,0]]
axc11NEW11       [[0,0]]
hba1eAUX11       [[0,0]]
hbaewAUX11       [[0,1,1]]
nfaewAUX11       [[0,1,1]]
hbnaewAUX11      [[0,1,1]]
nfnaewAUX11      [[0,1,1]]
nfeqfNEW11       [[0,1,0],[0,1,1]]
dral1NEW11       [[0,0]]
drex1NEW11       [[0,0]]
dral2wAUX11      [[0,1,1]]
drnf2wAUX11      [[0,1,1]]
drsb1NEW11       [[0,0,1],[0,1,0]]
spimtNEW11       [[0,0]]
spimNEW11        [[0,0]]
spimeNEW11       [[0,0]]
spimedNEW11      [[0,0]]
aevwAUX11        [[0,1,2,2,3],[0,1,2,3,2]]
aevNEW11         [[0,1,0,0,2],[0,1,1,1,2],[0,1,2,0,2],[0,1,2,2,0],[0,1,2,2,1],[0,1,2,2,3]]
hbaew3AUX11      [[0,1,0],[0,1,1]]
nfaew3AUX11      [[0,1,0],[0,1,1]]
nfnaew3AUX11     [[0,1,0],[0,1,1]]
equviniNEW11     [[0,1,0],[0,1,1]]
ax12v2NEW11      [[0,0,1]]
ax12a2NEW11      [[0,0,1]]
axc15NEW11       [[0,0]]
equs4NEW11       [[0,0]]
equs5NEW11       [[0,0]]
sb2NEW11         [[0,0]]
a16gNEW11        [[0,1,0]]
a16gbNEW11       [[0,1,0]]
a16nfNEW11       [[0,1,0]]
sb4NEW11         [[0,0]]
hbsb2NEW11       [[0,0]]
sbequ5wAUX11     [[0,1,2,1]]
nfsb2NEW11       [[0,0]]
sbequiNEW11      [[0,1,0],[0,1,1]]
sbequNEW11       [[0,1,0]]
drsb2NEW11       [[0,1,0]]
ax-7OLD11        [[0,0]]
hbaeOLD11        [[0,1,0],[0,1,1]]
nfaeOLD11        [[0,1,0],[0,1,1]]
hbnaeOLD11       [[0,1,0],[0,1,1]]
nfnaeOLD11       [[0,1,0],[0,1,1]]
dral2OLD11       [[0,1,0]]
drnf2OLD11       [[0,1,0]]
cdlemk22         [[0,1,2,3,3,0]]
cdleml6          [[0,1,2,1,3,4]]
cdleml7          [[0,1,2,1,3,4]]
cdleml8          [[0,1,2,1,3,4]]
cdleml9          [[0,1,2,1,3,4]]
erngdvlem4       [[0,1,2,1,3,4,5]]
erngdvlem4-rN    [[0,1,2,1,3,4,5]]
cdlemn2a         [[0,0]]

[Giovanni Mascellani]

Hi,

Il 21/04/19 19:46, Mario Carneiro ha scritto:

> This is logically related to the "metamath zero" thread
> (https://groups.google.com/d/msg/metamath/raGj9fO6U2I/dmVwJJcjCQAJ), but
> I want to re-characterize it in pure metamath terms. A while ago Norm
> did an experiment on the consequences of unbundling all theorems (in the
> thread I'm replying to). I have some more data to report on that front,
> now that I am getting closer to implementing a translation that includes
> proofs, not just statements. The following is a list of all "shadow
> copies" of statements that would be required to translate bundled
> theorems into their unbundled counterparts. For example, equtrr has
> [[0,1,0],[0,1,1]] written after it, meaning that of its three set
> variables x,y,z, they can be merged in the pattern x,y,x and x,y,y to
> obtain a new version of the theorem, which would be a substitution
> instance in metamath but is a separate theorem in unbundled land. This
> list includes all transitively collapsed theorems, i.e. applying the
> same proof for a collapsed theorem will probably involve calling other
> collapsed theorems, causing those to be generated as well.

Please tell me if I am understanding correctly: ideally we would like to
have all theorems "unbundled", i.e. with all set variables required to
be distinct (e.g., in a git $d clause). We would like that because that
would be closer to what a mathematician usually thinks when they look at
a statement (which is taken to be an actual statement, and not a
meta-statement like in Metamath), and also because this is the
assumption usually made by other systems, so it would be a step in the
direction of compatibility. However we cannot just throw in a big $d
statement, because that breaks the proofs that actually substitute the
same variable in two different and originally-non-$d-ed variables.

So, if we want to do the unbundling, we have to first take all the
theorems in which there are variables that are not $d-ed and produce
other N versions of it, in which every couple of variables is either
"concretely" identified or separated by a $d (in the right combinatorial
way), and prove all those new variations (which should actually be easy:
the same proof, changing the variables, should be ok for all of them).
Then we would have to change all the theorems that use the unbundled one
in their proof to select each time the appropriate version.

Is all of this correct? I might be understating something, but it does
not look like a particularly difficult thing to achieve.

Thanks, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Mario Carneiro]

That's exactly right. The whole process can be automated, although it produces some very silly proofs (like the proof of equcomi where the variables are the same - this is just id). Since set.mm is so well optimized, this makes me a bit sad - I would prefer to have an opportunity to manually eliminate that stuff. But with the current setup it's not clear how to work that into the ecosystem. I am working on improving the translation so that fewer theorems are marked as requiring unbundling, but once that's done one way forward is just to remove all or most of these "collapsed" theorem applications in set.mm. They are very rarely necessary or deliberate, and there is only a handful of them in the whole database, so that's a reasonable task. When I talk to mathematicians about metamath (including many of the sorts of people who make claims like "Metamath is not a serious contender for large scale formalization" from the other thread), the strangeness of variables is a chief sticking point. It's hard to get past that for most people. So I think it's worthwhile to try to bring metamath closer to conventional logic, especially if we can do so without having to change the spec at all.

Thanks, Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

--
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.

[Jim Kingdon]

So this just concerns distinct variable constraints (or the lack of them, really) between individual variables, not between individual variables and either formula or class variables?

I guess that's why there are so few. A theorem like equcom is sort of "temporary" in the sense that it doesn't get used as much once we add eqcom (the class equivalent).

Do you have a sense for how much of the bundling just happens "within" first order logic (e.g. statements of axioms, deriving theorems for substitution and all the usual things), and how much affects the usage in the rest of set.mm (ax-ext and beyond)? The consequences of an answer one way or the other especially affect systems with a separation between stating theorems/axioms and proving them, but I guess even in metamath terms alone we can ask whether this affects non-logic sections in a fundamental way or whether bundling outside the logic section would be even easier to avoid than within it.

[Norman Megill]

A fundamental difference between Metamath and other proof languages is that it works exclusively with metavariables ranging over wffs and individual variables, whereas most if not all others work with individual variables.  This is one of the reasons its formal proofs are often much shorter than those of other provers, which usually (perhaps always?) completely lack the ability to show actual textbook formal proofs from axioms, in part perhaps because they would be astronomically long (as an extreme example see http://us.metamath.org/mpeuni/mmset.html#2p2e4length).  Of course Metamath proofs are not formal proofs as defined in textbooks (where proof steps are object-language instantiations of the axiom and inference rule schemes) but can trivially be converted to them for any particular theorem by instantiating the metavariables with object-language instances.

Now I'm not saying that set.mm would become much larger if we unbundle the axioms.  Practically it probably wouldn't, as our experiments have shown.  But doing this seems like we are artificially forcing setvar metavariables to pretend to be object-language variables, which they are not.  It seems to me to violate the "spirit" of what Metamath is all about:  every substitution instance of a scheme is a scheme and never an object language statement.

Consider ax-7, which is an axiom scheme, not an individual axiom.  In Tarski's version, he does not require that the metavariables x,y,z be distinct.  So we are being faithful to Tarski.  Even in most textbook versions of this scheme, I don't think it requires them to be distinct.

Consider ax-gen, which doesn't require that the setvars in any expression substituted for phi be mutually distinct, because there isn't any way to do that in the Metamath language.  I guess we could put in a universal giant $d statement containing all setvars (as I did for my experiment a while back),  but that seems ugly and artificial.

I understand the desire or need to have an unbundled version of set.mm that emulates object-language variables in order to provide a practical interface to other proof languages.  However IMO the proper way to do this would be with an automated tool that transforms the existing set.mm into another .mm file with the required unbundling.  Even if it results in a few "silly" proofs, this shouldn't matter because essentially it would just be an intermediate file in a longer process.

Norm


On Sunday, April 21, 2019 at 3:20:03 PM UTC-4, Mario Carneiro wrote:

[Benoit]

Upon reading Mario's interesting message, I had a reaction very close to Norm's.  I think that the possibility of bundling is a nice feature of metamath.  More precisely, I would say that the main novelty of Megill, A Finitely Axiomatized Formalization of Predicate Calculus with Equality, was to consider schemes as "first-class citizens", whereas before they were only dealt with informally, in the metalogic.  It would be a shame to come back from that state.

If the goal of unbundling is to make metamath closer to other systems, and in order to do so one manages to unbundle metamath schemes automatically, then... problem solved!  No more need to unbundle in order to ease translation: simply include the "unbundling algorithm" within the "translator".

As to the difficulty of understanding bundling, I don't see what's so strange in the fact that two variables may take the same value. It's actually the opposite that would be quite artificial: imagine the sentence "for all real numbers x and y different from each other, one has x + y = y + x"... sounds weird.  Bundling is exactly the same thing one level up.

Of course I know that I'm telling nothing new to most of the readers here... just trying to enunciate things, and be corrected if I have some misconceptions.

Benoît

[David A. Wheeler]

On Sun, 21 Apr 2019 18:33:23 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> ... Of course Metamath

> proofs are not formal proofs as defined in textbooks (where proof steps are

> object-language instantiations of the axiom and inference rule schemes) ...

I disagree.

Metamath proofs absolutely *are* formal proofs using the usual definition.
"A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference."
https://en.wikipedia.org/wiki/Formal_proof and The Cambridge Dictionary of Philosophy, deduction
Metamath proofs completely meet that definition, full stop, no qualifiers.

It's true that most computer systems for formalized math only work at
object-language instantiations. HOWEVER, I think mathematicians don't actually
take that fact all that seriously. For example, let's say someone proved this claim:

∀ x p(x) # CLAIM 1

Imagine someone who said, "Ah, but that's totally different than what I wanted
to prove, because that claim does not prove the following":

∀ y p(y) # CLAIM 2

If you *seriously* believe that your system only works at the object-language instantiation
level, then strictly speaking that is correct. After all, you have to take an extra step to
convert claim 1 into claim 2. But that's absurd. NO ONE would take that seriously.
Once you prove claim 1, no one would bother to try to prove claim 2 unless their tool required it.

I think that while mathematical books & tools often formalize only the object level,
in *practice* mathematicians actually work more at the metamath level.
That is, they presume that you can swap out variables (subject to certain constraints)
and that those expressions in the two claims prove "the same" thing.

> Now I'm not saying that set.mm would become much larger if we unbundle the
> axioms. Practically it probably wouldn't, as our experiments have shown.
> But doing this seems like we are artificially forcing setvar metavariables
> to pretend to be object-language variables, which they are not.

I don't think Mario is claiming that they are the same thing.
Instead, I think what he's arguing for is to intentionally use forms that
are easier to convert to other systems & back, and are easier for other
mathematicians to reason about.

Intentionally limiting the use of some capability,
to gain some other advantage, seems very much worth considering.
I'd like to see it considered further, in particular, I'd like to see an example or two.

> It seems
> to me to violate the "spirit" of what Metamath is all about: every
> substitution instance of a scheme is a scheme and never an object language
> statement.

That wouldn't change, since every instance would still be a scheme.
Rigging things so that the correspondence is clearer is no crime :-).

> I understand the desire or need to have an unbundled version of set.mm that
> emulates object-language variables in order to provide a practical
> interface to other proof languages. However IMO the proper way to do this
> would be with an automated tool that transforms the existing set.mm into
> another .mm file with the required unbundling. Even if it results in a few
> "silly" proofs, this shouldn't matter because essentially it would just be
> an intermediate file in a longer process.

If that's easy, that'd be great.

But if that's not easy, I can see a real advantage to modifying set.mm to make it
easier to import/export proofs with other systems.
One advantage of providing unbundled forms, even if there's an automated process,
is that it'd make the correspondence easier to understand.
Another *potential* advantage would be if it made
the system more acceptable to more mathematicians, by making "most expressions"
more like what they're familiar with.

I think it'd be key to understand what the result would be from Mario's idea.
Axiom ax-7 probably a good case in point. Would the idea be to create multiple
axioms for each unbundled variant? Or create the bundled form, prove
all the unbundled variants, and then mark the bundled version as
"Further usage is discouraged"? What would the impact be?

There are a *lot* of words expended to try to help people understand bundling.
It's powerful, and allows for some simplifications, but it's clearly confusing to many people.
If *not* using that capability results in a system that's easier to use
and import/export, then those are good arguments for reconsideration.

It's true that Metamath variables aren't the object variables. But in *practice*
mathematicians use an object system for "x", and mentally note that that
really applies regardless of what the variable really is... which is closer to what
Metamath does in the first place :-). If by no longer using bundling
the system would be easier to understand, accept, and import/export, then
we should think about doing so. Bundling doesn't seem as powerful in *practice*
as these other potential advantages (though the proof is in the pudding).

--- David A. Wheeler

[Norman Megill]

On Monday, April 22, 2019 at 1:03:43 PM UTC-4, David A. Wheeler wrote:

On Sun, 21 Apr 2019 18:33:23 -0700 (PDT), Norman Megill wrote:
> ... Of course Metamath
> proofs are not formal proofs as defined in textbooks (where proof steps are
> object-language instantiations of the axiom and inference rule schemes) ...

I disagree.

Metamath proofs absolutely *are* formal proofs using the usual definition.
"A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference."
https://en.wikipedia.org/wiki/Formal_proof and The Cambridge Dictionary of Philosophy, deduction
Metamath proofs completely meet that definition, full stop, no qualifiers.

The key phrase is "each of which is an axiom...", not "each of which is an axiom scheme...".  The "axioms" in set.mm correspond to axiom schemes in first-order logic:  http://us.metamath.org/mpeuni/mmset.html#schemes

On the other hand, Metamath can be considered its own formal language, and from that point of view it does display formal proofs in that formal language.  But they aren't, strictly speaking, formal proofs in FOL.

I agree the distinction is somewhat pedantic, but I think it is useful to understand the difference, which I don't see as being hard to understand.
 

It's true that most computer systems for formalized math only work at
object-language instantiations. HOWEVER, I think mathematicians don't actually
take that fact all that seriously. For example, let's say someone proved this claim:

∀ x p(x)    # CLAIM 1

Imagine someone who said, "Ah, but that's totally different than what I wanted
to prove, because that claim does not prove the following":

∀ y p(y)     # CLAIM 2

If you *seriously* believe that your system only works at the object-language instantiation
level, then strictly speaking that is correct.  After all, you have to take an extra step to
convert claim 1 into claim 2.  But that's absurd. NO ONE would take that seriously.
Once you prove claim 1, no one would bother to try to prove claim 2 unless their tool required it.

∀ x p(x) and ∀ y p(y) are logically equivalent but are different wffs.  Because they can be proved to be equivalent, they can be treated the same informally.  But I don't think a mathematician would claim they are identical (which would be silly because one has x and the other has y), only that they are logically equivalent and thus interchangeable.
 

The algorithm to do that should be straightforward, if somewhat tedious to write if we want to discard unbundled instances that aren't used, preserve the niceties of set.mm formatting, and so on.  But once written it should run very fast.

Going back from unbundled to bundled, though, is nontrivial, and all the work doing that would be lost if we adopted the longer unbundled version.

The only reason I can see to unbundle is to emulate object-language variables for easier export of set.mm proofs.  Actually, I would think that translating theorems/proofs that have wff variables would be more problematic than the (somewhat straightforward) issue of unbundling, because no other language AFAIK has the general-purpose wff variables that set.mm does.  Mario has probably thought about that and may wish to comment.

For importing proofs, unbundled theorems would in principle automatically work and can be just added to set.mm.  A more serious problem with importing proofs is that AFAIK no other prover can output formal proofs, and an automated conversion of steps in their internal algorithms to formal proofs may lead to astronomically long proofs.  I don't know what the solution to that is.  At this point, proofs in other languages can only be used as hints to create a Metamath version manually.

 

One advantage of providing unbundled forms, even if there's an automated process,
is that it'd make the correspondence easier to understand.
Another *potential* advantage would be if it made
the system more acceptable to more mathematicians, by making "most expressions"
more like what they're familiar with.

I think it'd be key to understand what the result would be from Mario's idea.
Axiom ax-7 probably a good case in point. Would the idea be to create multiple
axioms for each unbundled variant?  Or create the bundled form, prove
all the unbundled variants, and then mark the bundled version as
"Further usage is discouraged"?  What would the impact be?

There are a *lot* of words expended to try to help people understand bundling.
It's powerful, and allows for some simplifications, but it's clearly confusing to many people.

I don't see how it is confusing provided you spend 5 minutes reading my link above.  Certainly that is a far less onerous prerequisite than for almost every other proof language.

[David A. Wheeler]

> On Monday, April 22, 2019 at 1:03:43 PM UTC-4, David A. Wheeler wrote:
> > Metamath proofs absolutely *are* formal proofs using the usual definition.
> > "A formal proof or derivation is a finite sequence of sentences (called
> > well-formed formulas in the case of a formal language), each of which is an
> > axiom, an assumption, or follows from the preceding sentences in the
> > sequence by a rule of inference."

On Tue, 23 Apr 2019 12:14:39 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> The key phrase is "each of which is an axiom...", not "each of which is an
> axiom scheme...". The "axioms" in set.mm correspond to axiom schemes in
> first-order logic: http://us.metamath.org/mpeuni/mmset.html#schemes
>
> On the other hand, Metamath can be considered its own formal language, and
> from that point of view it does display formal proofs in that formal
> language. But they aren't, strictly speaking, formal proofs in FOL.

Nothing in the definition of "formal proof"
requires that the formal language be FOL.
You can go with that latter interpretation if you'd like :-).

You still have finite sequences of sentences, axioms, assumptions, and rules of inference.
Therefore, Metamath proofs are formal proofs.

--- David A. Wheeler

[Mario Carneiro]

On Mon, Apr 22, 2019 at 1:03 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Sun, 21 Apr 2019 18:33:23 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> ... Of course Metamath
> proofs are not formal proofs as defined in textbooks (where proof steps are
> object-language instantiations of the axiom and inference rule schemes) ...

I disagree.

Metamath proofs absolutely *are* formal proofs using the usual definition.
"A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference."
https://en.wikipedia.org/wiki/Formal_proof and The Cambridge Dictionary of Philosophy, deduction
Metamath proofs completely meet that definition, full stop, no qualifiers.

I agree with David here, and I think this an important point. Metamath is built on an intuition that it is formalizing metavariable mathematics, and it has theorems that are schemes over some unstated "object language". But it is important to realize that this is only an intutition, and Metamath is *not* actually doing this, in the same way that Peano Arithmetic is not the same as the theory of the natural numbers and ZFC is not the same as the theory of the true platonic sets. Metamath is a formal system, and it has rules for when certain theorems (not theorem schemes, theorems according to Metamath spec) are derived from other theorems and axioms. The variables are just variables, and there is simply a rule that you can substitute an expression for a variable when you apply a theorem. This situation has a *model* in which the theorems are theorem schemes over a countable set of variables and disjointness means the variables are unequal, but there are other, more unusual models, and simply as a result of Metamath being a formal proof system it cannot completely characterize this underlying model and exclude the weird models.

This manifests itself in Metamath as certain true-but-unprovable statements like ax-5 (previously ax-17), which follow from the other axioms in every "object language instance" and so are true in the model of metamath as the object language of ZFC, but must be stated as an axiom in metamath to be proven.

 

It's true that most computer systems for formalized math only work at
object-language instantiations. HOWEVER, I think mathematicians don't actually
take that fact all that seriously. For example, let's say someone proved this claim:

∀ x p(x)    # CLAIM 1

Imagine someone who said, "Ah, but that's totally different than what I wanted
to prove, because that claim does not prove the following":

∀ y p(y)     # CLAIM 2

If you *seriously* believe that your system only works at the object-language instantiation
level, then strictly speaking that is correct.  After all, you have to take an extra step to
convert claim 1 into claim 2.  But that's absurd. NO ONE would take that seriously.
Once you prove claim 1, no one would bother to try to prove claim 2 unless their tool required it.

I think that while mathematical books & tools often formalize only the object level,
in *practice* mathematicians actually work more at the metamath level.
That is, they presume that you can swap out variables (subject to certain constraints)
and that those expressions in the two claims prove "the same" thing.

Actually, there are logics that allow those two claims to actually be the same theorem. If you use de Bruijn variables, then both statements are rendered as ∀, p(#0), so no renaming is necessary because there are no variable names. But this is probably beside the point.

 

> Now I'm not saying that set.mm would become much larger if we unbundle the
> axioms.  Practically it probably wouldn't, as our experiments have shown. 
> But doing this seems like we are artificially forcing setvar metavariables
> to pretend to be object-language variables, which they are not.

I don't think Mario is claiming that they are the same thing.
Instead, I think what he's arguing for is to intentionally use forms that
are easier to convert to other systems & back, and are easier for other
mathematicians to reason about.

Intentionally limiting the use of some capability,
to gain some other advantage, seems very much worth considering.
I'd like to see it considered further, in particular, I'd like to see an example or two.

That's right. Metamath will still be Metamath, I'm not proposing to change that. But if a feature can be modeled but is expensive to model, then perhaps it is worthwhile to try to avoid it unless the usage is worth the expense. Currently we don't consider these uses expensive, so they get used freely and accidentally. Part of my thesis is that these uses are mostly inessential, and as I see it there is much to be gained by avoiding their casual use.

 

> I understand the desire or need to have an unbundled version of set.mm that
> emulates object-language variables in order to provide a practical
> interface to other proof languages.  However IMO the proper way to do this
> would be with an automated tool that transforms the existing set.mm into
> another .mm file with the required unbundling.  Even if it results in a few
> "silly" proofs, this shouldn't matter because essentially it would just be
> an intermediate file in a longer process.

If that's easy, that'd be great.

But if that's not easy, I can see a real advantage to modifying set.mm to make it
easier to import/export proofs with other systems.

One advantage of providing unbundled forms, even if there's an automated process,
is that it'd make the correspondence easier to understand.
Another *potential* advantage would be if it made
the system more acceptable to more mathematicians, by making "most expressions"
more like what they're familiar with.

There is a real impedance mismatch here with logicians, as I've tried to stress. A logician knows how variables work - you don't need to tell them. What's more, you show them a system where 99% of the time variables are acting just like the variables they know. And then in 1% of cases variables do this weird collapsing bound variable capture thing and they are running for the door. My goal with the metamath zero variable rules are to capture the things about metamath variables that make substitution dead simple, while eliminating the weird variable capture thing that scares all the serious mathematicians away.

 

I think it'd be key to understand what the result would be from Mario's idea.
Axiom ax-7 probably a good case in point. Would the idea be to create multiple
axioms for each unbundled variant?  Or create the bundled form, prove
all the unbundled variants, and then mark the bundled version as
"Further usage is discouraged"?  What would the impact be?

I believe that in the case of ax-7 there is a better solution. In first order logic, ax-7 doesn't need to be a scheme in order for it to mean what we want. You are allowed to substitute variables for other variables in FOL - this doesn't require any fancy non-disjointness assumptions. In MM0, unlike MM, there are two kinds of variables for each sort. One kind can participate in binding occurrences (like in a forall) and the other kind can be substituted for expressions. In MM these two notions are conflated, so we have "setvar" which is of the first kind, and "class" and "wff" which are of the second kind, and this makes it impossible to indicate (without adding a new sort) that in a particular context you are allowing expressions. Instead, this is kind-of-approximated through the lack of disjoint variable conditions, but this information is very hard to interpret losslessly.

Imagine we had a set.mm sort for things that are manifestly sets (i.e. elements of V). This would have to be different from "setvar" because you can't use expressions for variables in binders. Then ax-7 could be stated using this sort instead of "setvar" - we don't care about binding anything so we are permitted to substitute expressions in this axiom. That's what MM0 is doing, and it accords well with standard FOL, where there are variables and terms and they live in the same sort (you can put either a variable or a term into a function) but only variables can appear as the bound variable of a forall.

 

There are a *lot* of words expended to try to help people understand bundling.
It's powerful, and allows for some simplifications, but it's clearly confusing to many people.

If *not* using that capability results in a system that's easier to use
and import/export, then those are good arguments for reconsideration.

It's true that Metamath variables aren't the object variables.  But in *practice*
mathematicians use an object system for "x", and mentally note that that
really applies regardless of what the variable really is... which is closer to what
Metamath does in the first place :-).  If by no longer using bundling
the system would be easier to understand, accept, and import/export, then
we should think about doing so.  Bundling doesn't seem as powerful in *practice*
as these other potential advantages (though the proof is in the pudding).

I want to make a short parallel here with non-grammatical databases. Metamath is sometimes too general for its own good, in the sense that it is so general that no one knows how to interpret the statements that are being proven anymore. More syntactic generality is not necessarily a good thing, because that means more and stranger models for the theory. Having a system which is working at the base level on strings makes people question their most basic assumptions about what formulas are, and this is unsettling. In "Models for Metamath" I define the concept of a "grammatical database" in order to exclude some not well behaved models. More well behaved models means things act more like you expect them to, and so you can bring your intuitions to bear without fear that nothing is what it appears to be. For a system that is supposed to be providing confidence that certain theorems (of mathematics in the abstract, not formal theorems of metamath) are true, this is a serious concern. That is, I should be able to prove in a metatheory that the proof that there are infinitely many primes in metamath plus the assumption that ZFC (the FOL theory) is consistent together imply that there are actually infinitely many primes. If I can't do this, then what is the point of formalization in the first place?

On Tue, Apr 23, 2019 at 3:14 PM Norman Megill <n...@alum.mit.edu> wrote:

On Monday, April 22, 2019 at 1:03:43 PM UTC-4, David A. Wheeler wrote:

On Sun, 21 Apr 2019 18:33:23 -0700 (PDT), Norman Megill wrote:
> ... Of course Metamath
> proofs are not formal proofs as defined in textbooks (where proof steps are
> object-language instantiations of the axiom and inference rule schemes) ...

I disagree.

Metamath proofs absolutely *are* formal proofs using the usual definition.
"A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference."
https://en.wikipedia.org/wiki/Formal_proof and The Cambridge Dictionary of Philosophy, deduction
Metamath proofs completely meet that definition, full stop, no qualifiers.

The key phrase is "each of which is an axiom...", not "each of which is an axiom scheme...".  The "axioms" in set.mm correspond to axiom schemes in first-order logic:  http://us.metamath.org/mpeuni/mmset.html#schemes

On the other hand, Metamath can be considered its own formal language, and from that point of view it does display formal proofs in that formal language.  But they aren't, strictly speaking, formal proofs in FOL.

I agree the distinction is somewhat pedantic, but I think it is useful to understand the difference, which I don't see as being hard to understand.

I've already said this above, but axioms in Metamath are *not* axiom schemes, they *model* axiom schemes. The actual object language that metamath is supposed to be a metatheory of is nowhere defined and is indeterminate in several ways. Even if you gave a definition of this object language, you wouldn't be able to enforce that metamath models that and only that.

You are right that metamath is a formal language in its own right, and that language is definitely not FOL, even if you add in the FOL-emulating axioms from set.mm. It is *almost* FOL, enough to tempt a full translation to FOL, with some caveats about bundling that propmted this thread.

 

If that's easy, that'd be great.

But if that's not easy, I can see a real advantage to modifying set.mm to make it
easier to import/export proofs with other systems.

The algorithm to do that should be straightforward, if somewhat tedious to write if we want to discard unbundled instances that aren't used, preserve the niceties of set.mm formatting, and so on.  But once written it should run very fast.

I'm generating unbundled instances on the fly, rather than generating all of them and throwing away the unnecessary ones. There are exponentially many unbundled instances in the extreme case, so this is a lot faster. Preserving formatting has not been on the radar but can be done in principle.

 

Going back from unbundled to bundled, though, is nontrivial, and all the work doing that would be lost if we adopted the longer unbundled version.

Actually it's not really, depending on the proof. Recall that $d's are not strictly necessary on theorems; they can be derived from the proof. So you can just put $d's on the axioms according to some annotation and then just forward propagate them through the proofs. At least, this will be able to capture all "harmless" instances of bundling, where, for example, you have two independent scopes that never interact in the proof so it doesn't matter if they are the same or not. If a theorem has to be rewritten to be unbundled, and now makes essential use of the DV condition, then perhaps it won't be dropped so easily. There are a few theorems where bundling is real work (requires some extra case analysis), and those probably won't be recovered. You can still go the other way with appropriate annotation; for example you could mark a theorem as being a bundling of several parallel FOL proofs, and the translator is responsible for applying the bundling (meta)theorem to construct a bundled theorem in metamath.

 

The only reason I can see to unbundle is to emulate object-language variables for easier export of set.mm proofs.  Actually, I would think that translating theorems/proofs that have wff variables would be more problematic than the (somewhat straightforward) issue of unbundling, because no other language AFAIK has the general-purpose wff variables that set.mm does.  Mario has probably thought about that and may wish to comment.

Wff variables are not a problem for HOL. In higher order logic we have variables of many types: wff variables, variables over the domain of discourse (let's say "set"), variables from set -> wff and wff -> wff and (set -> wff) -> wff; this is strictly more powerful than FOL / metamath because of the ability to perform higher order quantification (i.e. classes of classes of classes...). Handling open terms is not a major issue either. The metamath axiom of generalization, |- ph => |- A. x ph, has no $d conditions on it, and you think "oh no, ph can potentially depend on anything! How can I represent it as ph(x,y,z,...)?" But that's not how HOL binding works. Any proof is allowed to depend on a context of available variables, not among those declared, as long as they are scoped appropriately. So just because ph is declared as ph(x) doesn't mean it can't have y in it, if y is never mentioned in the theorem at all. Yes, I know this is a bit unusual for someone who thinks in terms of $d's, but this is standard practice in logic, especially from a type theory perspective. So you would declare that theorem as "! ph : set -> wff, ((! x : set, |- ph(x)) => |- A. x ph(x))", where ! x is meta-quantification. This means that in the proof of |- ph(x) you are permitted to refer to x and ph, and when you apply the theorem you substitute for ph. Just like in metamath, substitution of expressions for variables is done by the verifier itself.

For importing proofs, unbundled theorems would in principle automatically work and can be just added to set.mm.  A more serious problem with importing proofs is that AFAIK no other prover can output formal proofs, and an automated conversion of steps in their internal algorithms to formal proofs may lead to astronomically long proofs.  I don't know what the solution to that is.  At this point, proofs in other languages can only be used as hints to create a Metamath version manually.

It's definitely not true that no other prover can output formal proofs. Every proof system I know has *some* method for exporting proof objects, but metamath is almost unique in its dedication to making this process simple and easy. I think that's one of it's greatest strengths when talking to other people about it - even if you don't care about metamath you can write a small program to get access to the proof and transfer it to your system of choice. Most other systems require you to install some monolith and use obscure commands that no one has maintained in the past ten years, and the author is long gone, and you don't know this other system and have no interest in really learning it either and why can't it be simpler? I've been through this with almost every formal theorem prover out there and metamath is definitely the best in that regard.

But I have to caveat this statement, because while metamath makes it easy to get at the proofs the logic is a barrier. Metamath proofs are difficult to interpret into any other system, and it is difficult to say in any formally precise sense what they actually mean (which is basically the same thing). It's all well and good to say "just follow these rules and even you can verify all of set.mm" but unless you know what those rules are implementing it's hard to say what the import of a proven theorem is. I don't want to translate things into FOL or HOL just because I like them as formal systems; it's because I want to define (and practically exercise) the relation between set.mm and *actual* ZFC, in any metalogic capable of stating both of these things.

There are a *lot* of words expended to try to help people understand bundling.
It's powerful, and allows for some simplifications, but it's clearly confusing to many people.

I don't see how it is confusing provided you spend 5 minutes reading my link above.  Certainly that is a far less onerous prerequisite than for almost every other proof language.

Perhaps if you are starting from scratch. But logic has developed a certain way for a reason, and "I am doing things different than literally everyone else" isn't a positive.

I think there is some great utility in treating variables the way metamath does, and direct substitution is an important factor in the blazing fast speed of metamath verification, but it's not good for the intuition. We need a good story for how we can go from a system that is fast to a verify to a logic that is well understood and studied. Saying "Tarski did it" doesn't seem to cut it for most people.

Mario

[David A. Wheeler]

On Tue, 23 Apr 2019 18:12:48 -0400, Mario Carneiro <di....@gmail.com> wrote:
> That's right. Metamath will still be Metamath, I'm not proposing to change
> that. But if a feature can be modeled but is expensive to model, then
> perhaps it is worthwhile to try to avoid it unless the usage is worth the
> expense. Currently we don't consider these uses expensive, so they get used
> freely and accidentally. Part of my thesis is that these uses are mostly
> inessential, and as I see it there is much to be gained by avoiding their
> casual use.

...

> There is a real impedance mismatch here with logicians, as I've tried to
> stress. A logician knows how variables work - you don't need to tell them.
> What's more, you show them a system where 99% of the time variables are
> acting just like the variables they know. And then in 1% of cases variables
> do this weird collapsing bound variable capture thing and they are running
> for the door. My goal with the metamath zero variable rules are to capture
> the things about metamath variables that make substitution dead simple,
> while eliminating the weird variable capture thing that scares all the
> serious mathematicians away.

Ok. It sounds like your primary concern is the impedence mismatch with logicians.
Trying to address that concern seems worthwhile, but the devil is in the details...
the modified version will have to earn its keep :-).

> I believe that in the case of ax-7 there is a better solution. In first
> order logic, ax-7 doesn't need to be a scheme in order for it to mean what
> we want. You are allowed to substitute variables for other variables in FOL
> - this doesn't require any fancy non-disjointness assumptions. In MM0,
> unlike MM, there are two kinds of variables for each sort. One kind can
> participate in binding occurrences (like in a forall) and the other kind
> can be substituted for expressions. In MM these two notions are conflated,
> so we have "setvar" which is of the first kind, and "class" and "wff" which
> are of the second kind, and this makes it impossible to indicate (without
> adding a new sort) that in a particular context you are allowing
> expressions. Instead, this is kind-of-approximated through the lack of
> disjoint variable conditions, but this information is very hard to
> interpret losslessly.
>
> Imagine we had a set.mm sort for things that are manifestly sets (i.e.
> elements of V). This would have to be different from "setvar" because you
> can't use expressions for variables in binders. Then ax-7 could be stated
> using this sort instead of "setvar" - we don't care about binding anything
> so we are permitted to substitute expressions in this axiom. That's what
> MM0 is doing, and it accords well with standard FOL, where there are
> variables and terms and they live in the same sort (you can put either a
> variable or a term into a function) but only variables can appear as the
> bound variable of a forall.

Can you show more specifically how to do this in Metamath (not MM0)
though some changes to set.mm?
Here's what I *think* you mean, but I may be completely misunderstanding.

Creating a new sort is easy enough:

$c set $.
$( $j syntax 'set'; $)


We need an axiom that lets us assert that some expression is a set
if it's a member of _V
(I would call this a "type conversion" based on programming language notions).
If I understand you correctly, that could be encoded in something like this:

${
$( Is something a member of the class of sets? $)
vset.1 $e |- A e. _V $. ($ Should something else be used here? $)
$( If it is, it's a set. $)
vset $a set A $.
$}

I'm not sure what you'd suggest ax-7 or ax-gen turn into, though, and I
may be misunderstanding you anyway.

Can you give specifics?
It seems like there's be a number of theorems that would have to be adjusted...
what would be the nature of those adjustments?

--- David A. Wheeler

[Benoit]

David: to answer your question (although it's a digression from this thread) have a look at

https://groups.google.com/forum/#!msg/metamath/8l2u5NzuSS8/B5pMbXV8BgAJ

and

https://groups.google.com/d/msg/metamath/nD8QGB7h5mA/5LinGUoWBAAJ

(and the rest of that thread).

Benoît

[Mario Carneiro]

Maybe a better example is doing peano arithmetic in metamath, because there it really is a first order theory with terms, rather than a theory with only a binary relation. But I'll play this one forward.

The vset axiom wouldn't work (according to the definition, it would make the database non-grammatical), because vset is a non context-free syntax axiom (a term former that depends on a proof). The axiom goes the other way around. Since we have a new sort, we need variables for that sort; let's say they are called sx, sy, sz, ...

vsx $f set sx $.

vsy $f set sy $.

...

Now we have an axiom that says that a set is an element of _V, just like vex:

vset $a sx e. _V $.

For this to typecheck we need a coercion from set to class:

cvs $a class sx $.

and we want set variables to be coercible to set expressions:

sv $a set x $.

We don't have to do anything with making set expressions work with e. and = because they already work on classes. Since forall still only accepts a set variable, these set expressions are not admissible to bind values, as they should be. That is, "A. sx ph" doesn't typecheck. To make the theory nontrivial, we add an (axiomatic) term former for making a set from a class:

stoset $a set toSet A $.

ax-toset $a |- toSet A = ( _I ` A ) $. 

Despite appearances that's not a definition of toSet A; it's actually saying that cvs (toSet A) = ( _I ` A ), although because metamath conflates all the = on different sorts it is basically a definition modulo ax-ext. If we admit this definition principle we can start to write other terms of sort "set":

s0 $a set s(/) $.

ax-s0 $a |- s(/) = (/) $.

sfv $a set ( F s` A ) $.

ax-sfv $a |- ( F s` A ) = ( F ` A ) $.

sun $a set ( sx su. sy ) $.

ax-sun $a |- ( sx su. sy ) = ( sx u. sy ) $.

and so on. Because of the coercions these definitions look more trivial than they are; the important thing is that they are all *syntactically* sets. So for instance ( sx su. sy ) e. _V is an application of vset, while ( sx u. sy ) e. _V would require a multi step proof using unex and vset.

Now ax-7 can be stated like so:

ax-7 $a |- ( sx = sy -> ( sx = sz -> sy = sz ) ) $.

There is no question about disjoint variable conditions now, because it's not even possible to state a disjoint variable condition between sx and sy, since neither one is a binding variable. (Well, this is a gentleman's agreement in set.mm, but you get the idea.) It's almost as if we wrote

ax-7 $a |- ( A = B -> ( A = C -> B = C ) ) $.

where again, it's silly to even consider DV conditions in this axiom, except the stated version still only applies to sets - it doesn't have to posit this higher order sort of predicates over the universe (a.k.a classes).

As I mentioned above, an even better example is if you wanted to do peano arithmetic in MM. (You can use https://github.com/digama0/mm0/blob/master/examples/peano.mm0 for reference, although it's in MM0 not MM notation. It would be nice to have an MM database of peano arithmetic, but I'm finding myself having to develop one from scratch because peano.mm is something more specialized, and written in an impractical notation.)

Not counting wffs, we have two sorts, which I will call "nat" (for expressions) and "var" (for variables ranging over natural numbers). I will use variables "x,y,z" for vars and "a,b,c" for nats. The FOL part is just like set.mm predicate calculus, except that "setvar" is renamed to "var". Equality is a relation between two nats, and "cv" is a map from var to nat. So you get (this is a sampling of axioms):

vx $f set x $.

na $f nat a $.

cv $a nat x $.

weq $a wff a = b $.

ax-7 $a |- ( a = b -> ( a = c -> b = c ) ) $.

${ $d x a $. ax-6 $a |- E. x x = a $. $}

n0 $a nat 0 $.

ns $a nat suc a $.

nadd $a nat ( a + b ) $.

nmul $a nat ( a * b ) $.

ax-peano1 $a |- 0 =/= suc a $.

ax-peano2 $a |- ( suc a = suc b -> a = b ) $.

ax-peano5 $a |- ( ( [ 0 / x ] ph /\ A. y ( [ y / x ] ph -> [ suc y / x ] ph ) ) -> A. x ph ) $.

ax-add0 $a |- ( a + 0 ) = a $.

ax-adds $a |- ( a + suc b ) = suc ( a + b ) $.

ax-mul0 $a |- ( a * 0 ) = 0 $.

ax-muls $a |- ( a * suc b ) = ( ( a * b ) + a ) $.

Notice that in ax-6 we can use a nat term rather than a variable. We lose the opportunity to bundle, though, because we can't allow E. x x = ( x + 1 ) to be derivable. In particular, unlike isset, ax-6 has no precondition saying "a is a nat" analogous to "A e. _V" - everything which is constructible is *syntactically* a nat and so is valid to put into a quantifier (from ax-6 we can derive things like ( A. x ph -> [ a / x ] ph ), again with no precondition).

With two separate sorts, one for variables and one for terms, it is really easy to see when disjoint variable conditions are relevant (like in a theorem like 2mo where you need disjointness to perform substitution commutation and so on) and when they are not, especially in cases where they are never even quantified like ax-peano2 here. In set.mm we have a preference for using classes when a variable is never quantified, because it has the added generality of admitting direct substitution rather than using vtocl and friends, and this has the side effect of avoiding unnecessary DV conditions on a variable that isn't being used like a real "variable", something that participates in binding, but is only used as a constant input value in the theorem.

Coming back to what I want in set.mm: The database already has some fairly rigid conventions that help to avoid the worst of the weirdness, and more and more of them are receiving tool support so that we can actively enforce them. Grammar checking and definition checking come to mind here. This bundling business is I think another place where we should find a happy medium in which we enforce some kind of convention which makes translation easier while also preserving the elegance of existing proofs and staying true to the spirit of metamath as a language that exploits advantages of being a metalanguage over an object language.

For many theorems in the predicate calculus section like exrot4 we have no DV conditions because they simply didn't come up in the course of the proof. I think this is great, it's packing some 30 or so FOL-distinct theorems into one and it shows off the power of not caring about disjointness. That said, if we actually think about what those collapsed theorems say, they are manipulating funny double bound formulas that I would certainly declare as suspicious and unnecessarily confusing if they came up in an actual proof. So I would say that "naturally non-disjoint" theorems are fine, they can be translated to distinctified theorems in FOL and then back to a non-disjoint theorem by disjointness inference. But actually *using* those collapsed theorems should be avoided unless the use is deliberate. I won't give a precise recommendation on what annotations to use until the translator gets to the point where it is clear what it can use, but I think we should have explicit opt-in bundling. This makes it easy to translate a theorem since we don't have to forward scan the whole rest of the database to find out what bundles are used, and it also documents when a bundling is deliberate.

On Tue, Apr 23, 2019 at 7:16 PM j4n bur53 <burs...@gmail.com> wrote:

I think, and believe this is the correct understanding of Norman Megill, that
when he writes "object language", he doesn't mean models and interpretations.
But effectively another formal language, which houses the "real" proofs.

I am aware of this. The thing about metamath, what makes it a little funny from a logic point of view, is that it is a formal system whose intended model *is* another formal system, where the model of *that* is some ZFC model thing. It's a two-level model: metamath over an object language over a universe of sets. What I am cautioning against is the belief that metamath perfectly reflects the object language semantics, so that you only have to worry about modeling aspects well known to set theorists about how an object language can model a universe of sets. Instead, because metamath is aimed at this "models of formal systems" level, the object language *itself* is indeterminate, and that universe of sets model below it might not even exist. The "object language" might already be quite weird and not like a formal system - it might have infinite derivation trees, or uncountably many variables, or disjointness might be a topological notion with some continuous smear of variableness. It gets weird, and no one has tried to study it as far as I know.

 

That this understanding of Norman Megill makes a dent, can be easily seen,
by variables of type wff. Some theorem proves **cannot** produce a
theorem of the form:

       ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
       http://us.metamath.org/mpeuni/pm2.27.html

For example a resolution theorem prover, where literals must have
a predicate name and aritry included, cannot produce such a result
strictly speaking.

A resolution theorem prover can prove a theorem like that - the wff variables are treated as propositional variables. Every resolution theorem prover or SAT solver I know has some means of representing atomic variables, and that's exactly what you are looking at there. That they act like "schema variables" in metamath is a consequence of its theorem application rule, which permits simultaneous substitution of the variables in a theorem at the point of application. I think this is what you are talking about with the "lifting lemma" - it is built into the foundations of metamath that this happens on every theorem application. But regardless of whether you think of it as making a scheme more specific, what actually happens in every verifier is a simultaneous substitution of expressions for variables. It's just happening at a different time than something like HOL which might do such substitution only when you apply the beta rule and otherwise only performs a fixed finite set of schematic inference rules built into the verifier.

 

[Jens-Wolfhard Schicke-Uffmann]

Also one should keep in mind that the set of people interested in formal
mathematics on the level of computer verified proofs tend to have a high
tolerance for spending some time on pedantries.

I think throwing away the more powerful and harder proofs just to remove
a automated translation layer is a bad idea.


Regards,
Drahflow

[Mario Carneiro]

On Wed, Apr 24, 2019 at 2:26 AM Jens-Wolfhard Schicke-Uffmann <drah...@gmx.de> wrote:

On Tue, Apr 23, 2019 at 12:14:39PM -0700, Norman Megill wrote:
> On Monday, April 22, 2019 at 1:03:43 PM UTC-4, David A. Wheeler wrote:
>     There are a *lot* of words expended to try to help people understand
>     bundling.
>     It's powerful, and allows for some simplifications, but it's clearly
>     confusing to many people.
> I don't see how it is confusing provided you spend 5 minutes reading my link
> above.  Certainly that is a far less onerous prerequisite than for almost every
> other proof language.
Also one should keep in mind that the set of people interested in formal
mathematics on the level of computer verified proofs tend to have a high
tolerance for spending some time on pedantries.

I disagree. I work with many mathematicians (real mathematicians, not computer science converts like me) that work with formal proofs to some extent in their work. While they recognize the value in pedantry, and want the computer to catch their mistakes and so on, they *do not* want to deal with issues that are only there because the system made these things problems. They want to deal with *math* pedantry (like "oops I forgot this assumption so now my proof won't go through"), not *system* pedantry (like "why isn't it finding this lemma? It's obviously fine, but it's failing to infer this and that... you're a proof assistant, why aren't you assisting me?") Any complications should be caused by them or by their explicit choices, there shouldn't be arbitrary hoops just for the sake of it.

I think throwing away the more powerful and harder proofs just to remove
a automated translation layer is a bad idea.

The proofs that I am talking about are those that haven't significantly benefited from this "bundling power". The experiments already show that it's a rarely used feature, and I'll do another experiment once I can identify and eliminate ax-7 style bundling misdiagnoses and I expect that the number of uses will drop quite a bit more. At that point we can look at the real culprits, and I strongly suspect they are all silly examples for which you can prove all the same results (not necessarily the bundled theorem itself but the theorem's uses) with almost no expansion in proof length. Certainly there have not yet been any example of "more powerful and harder proofs" among the list of bundled theorems, not counting theorems which are specifically exploring bundling as a concept.

Mario

[David A. Wheeler]

On Wed, 24 Apr 2019 03:13:58 -0400, Mario Carneiro <di....@gmail.com> wrote:
> The proofs that I am talking about are those that haven't significantly
> benefited from this "bundling power". The experiments already show that
> it's a rarely used feature, and I'll do another experiment once I can
> identify and eliminate ax-7 style bundling misdiagnoses and I expect that
> the number of uses will drop quite a bit more. At that point we can look at
> the real culprits, and I strongly suspect they are all silly examples for
> which you can prove all the same results (not necessarily the bundled
> theorem itself but the theorem's uses) with almost no expansion in proof
> length. Certainly there have not yet been any example of "more powerful and
> harder proofs" among the list of bundled theorems, not counting theorems
> which are specifically exploring bundling as a concept.

I look forward to those results.

If bundling doesn't provide serious benefits in set.mm, and its use can lead to
rejection of Metamath or difficulty in exchanging data with other systems,
then getting rid of bundling in set.mm sounds like a very good idea.

I appreciate that it's possible to write code to automatically do the mapping
between bundled & unbundled versions.
But often the most efficient code is the code you don't have to write at all :-).
If we switched to unbundled versions that would make the mapping a non-event.

Of course, maybe the "culprits" are not so easy to get rid of after all.
I look forward to seeing the list of "real culprits".... and more importantly,
what could be done instead.

--- David A. Wheeler

[David A. Wheeler]

On Tue, 23 Apr 2019 21:20:08 -0400, Mario Carneiro <di....@gmail.com> wrote:
> ... But I'll play this one forward.

>
> The vset axiom wouldn't work (according to the definition, it would make
> the database non-grammatical), because vset is a non context-free syntax
> axiom (a term former that depends on a proof). The axiom goes the other way
> around. Since we have a new sort, we need variables for that sort; let's
> say they are called sx, sy, sz, ...
>
> vsx $f set sx $.
> vsy $f set sy $.
> ...
>
> Now we have an axiom that says that a set is an element of _V, just like
> vex:
>
> vset $a sx e. _V $.
>
> For this to typecheck we need a coercion from set to class:
>
> cvs $a class sx $.
>
> and we want set variables to be coercible to set expressions:
>
> sv $a set x $.
>
> We don't have to do anything with making set expressions work with e. and =
> because they already work on classes. Since forall still only accepts a set
> variable, these set expressions are not admissible to bind values, as they
> should be. That is, "A. sx ph" doesn't typecheck.

Great! This is very clear, and I can see possible advantages.
That's much better than the approach I posted.

> To make the theory
> nontrivial, we add an (axiomatic) term former for making a set from a class:
>
> stoset $a set toSet A $.
> ax-toset $a |- toSet A = ( _I ` A ) $.
>
> Despite appearances that's not a definition of toSet A; it's actually
> saying that cvs (toSet A) = ( _I ` A ), although because metamath conflates
> all the = on different sorts it is basically a definition modulo ax-ext.

I'm not sure I'm fully grokking this, but for the sake of argument let's keep going.

> If we admit this definition principle we can start to write other terms of
> sort "set":
>
> s0 $a set s(/) $.
> ax-s0 $a |- s(/) = (/) $.
> sfv $a set ( F s` A ) $.
> ax-sfv $a |- ( F s` A ) = ( F ` A ) $.
> sun $a set ( sx su. sy ) $.
> ax-sun $a |- ( sx su. sy ) = ( sx u. sy ) $.
>
> and so on. Because of the coercions these definitions look more trivial
> than they are; the important thing is that they are all *syntactically*
> sets. So for instance ( sx su. sy ) e. _V is an application of vset, while
> ( sx u. sy ) e. _V would require a multi step proof using unex and vset.

I understand some of the advantages of *syntactically* knowing something is a set.

However, this example is starting to get ugly - it looks like there's going to be a huge
number of equivalent "operations" and constants that get defined twice
(once with typeset class, once with typeset set).
I see s(/) , su. , s` , and I expect there'd be a lot more.

If you have to define everything twice, that's probably
twice as much as should be done :-). Especially if there seems to be an unbounded
collection of things that get duplicated.

I presume you're doing things this way so that Metamath's mechanisms
syntax matching can automatically do a lot of work.
If that's the goal, I understand it. However, having to define and
keep track of twice as many symbols doesn't seem like a win.

It seems to me we do something similar without doubling the symbols in use.
We already have to prove that expressions are sets in many contexts,
so that wouldn't really represent much of a change.

Isn't there a way to cleanly do this WITHOUT defining
s(/) , su. , s` , and so on?

> Now ax-7 can be stated like so:
>
> ax-7 $a |- ( sx = sy -> ( sx = sz -> sy = sz ) ) $.
>
> There is no question about disjoint variable conditions now, because it's
> not even possible to state a disjoint variable condition between sx and sy,
> since neither one is a binding variable. (Well, this is a gentleman's
> agreement in set.mm, but you get the idea.)

Metamath obviously *could* state a disjoint variable condition for this case.
I presume what you mean is that in systems OTHER than Metamath,
because there are no binding variables, users would be unsurprised if
sx and sy could refer to the same variable.

If that's what you mean, I see the advantage here.

> It's almost as if we wrote
>
> ax-7 $a |- ( A = B -> ( A = C -> B = C ) ) $.
>
> where again, it's silly to even consider DV conditions in this axiom,
> except the stated version still only applies to sets - it doesn't have to
> posit this higher order sort of predicates over the universe (a.k.a
> classes).
>
> As I mentioned above, an even better example is if you wanted to do peano
> arithmetic in MM.

...

> With two separate sorts, one for variables and one for terms, it is really
> easy to see when disjoint variable conditions are relevant (like in a
> theorem like 2mo where you need disjointness to perform substitution
> commutation and so on) and when they are not, especially in cases where
> they are never even quantified like ax-peano2 here. In set.mm we have a
> preference for using classes when a variable is never quantified, because
> it has the added generality of admitting direct substitution rather than
> using vtocl and friends, and this has the side effect of avoiding
> unnecessary DV conditions on a variable that isn't being used like a real
> "variable", something that participates in binding, but is only used as a
> constant input value in the theorem.
>
> Coming back to what I want in set.mm: The database already has some fairly
> rigid conventions that help to avoid the worst of the weirdness, and more
> and more of them are receiving tool support so that we can actively enforce
> them. Grammar checking and definition checking come to mind here. This
> bundling business is I think another place where we should find a happy
> medium in which we enforce some kind of convention which makes translation
> easier while also preserving the elegance of existing proofs and staying
> true to the spirit of metamath as a language that exploits advantages of
> being a metalanguage over an object language.

I like happy mediums :-). I suspect you're right.
I look forward to your further thoughts & the results of your
unbundling experiments.

--- David A. Wheeler

[Norman Megill]

On Tuesday, April 23, 2019 at 6:13:07 PM UTC-4, Mario Carneiro wrote:

On Mon, Apr 22, 2019 at 1:03 PM David A. Wheeler wrote:

On Sun, 21 Apr 2019 18:33:23 -0700 (PDT), Norman Megill wrote:
> ... Of course Metamath
> proofs are not formal proofs as defined in textbooks (where proof steps are
> object-language instantiations of the axiom and inference rule schemes) ...

I disagree.

Metamath proofs absolutely *are* formal proofs using the usual definition.
"A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference."
https://en.wikipedia.org/wiki/Formal_proof and The Cambridge Dictionary of Philosophy, deduction
Metamath proofs completely meet that definition, full stop, no qualifiers.

I agree with David here, and I think this an important point. Metamath is built on an intuition that it is formalizing metavariable mathematics, and it has theorems that are schemes over some unstated "object language".

Maybe I'm misunderstanding, but the intended object language isn't unstated; it is described in English in mmset.html.  We define object-language wffs as expressions built from variables v1,v2,... and connectives ->, -., A., =, e. .  The setvar and wff (meta)variables in set.mm range over these variables and formulas.  It is no different from a logic textbook that says, "Let phi and psi be wffs.  The axioms are all formulas of the following forms:  (phi -> (psi -> phi)) [etc.]".

If what you mean is that the object language is not a formal part of the set.mm language, that is true, but there is no need because the object language is never used there.

I suppose we could extend the Metamath language with a mechanism to instantiate its schemes and proof steps into object-language formulas, but that seems unnecessarily pedantic since it is obvious to anyone who has read the English-language description and looked at its examples.  It would just be needless complexity that probably no one would ever use.

...

There is a real impedance mismatch here with logicians, as I've tried to stress. A logician knows how variables work - you don't need to tell them. What's more, you show them a system where 99% of the time variables are acting just like the variables they know. And then in 1% of cases variables do this weird collapsing bound variable capture thing and they are running for the door. My goal with the metamath zero variable rules are to capture the things about metamath variables that make substitution dead simple, while eliminating the weird variable capture thing that scares all the serious mathematicians away.

A logician should know the difference between metavariables and variables, and if not they'll have to spend 5 minutes reading the mmset.html link I provided.  What is so difficult about that?

It is hard to believe that bundling "scares all the serious mathematicians away."  Are they also scared away from the papers of Tarski and colleagues that use bundling freely?  Bundling is a trivial concept and the whole issue seems to be making a mountain out of a molehill.  The advanced theorems in set.mm that they would be interested in are unlikely to have bundling anyway, so if they are scared away it probably isn't because of that.

...
 

I think there is some great utility in treating variables the way metamath does, and direct substitution is an important factor in the blazing fast speed of metamath verification, but it's not good for the intuition. We need a good story for how we can go from a system that is fast to a verify to a logic that is well understood and studied. Saying "Tarski did it" doesn't seem to cut it for most people.

 

Tarski was a well-known leader in the field who people take seriously.

But independently of that, I chose his system because I found it very compelling due to the extreme simplicity of its primitive notions.  A reviewer of Tarksi's 1965 paper (Shepherdson, JSL, 1974) said "the author's observations provide the most elegant and most simply describable axiom systems for predicate logic with identity".

The proposal to revamp set.mm to prohibit bundling, add a new variable sort for sets with additional axioms, and add a new collection of variable names them, would change it from a simple and pure metalanguage to a kind of hybrid of metalanguage and quasi-object language that is more complex. To me that is not as elegant and is even somewhat pointless.

The purpose of FOL= in set.mm is to formalize Tarski's system.  He and his colleagues had no issues with bundling and used it often in their papers.  We don't have to use bundling, but it comes for free with the metalogic, and I find it interesting and useful to exploit it to obtain the most general (meta)theorems possible for use (mostly) within FOL=.

Anyone who dislikes bundling is free not to use it.  It is usually easy to avoid or ignore in set theory and beyond anyway, and it hardly has any impact on anyone not working on the FOL= part of set.mm.

I understand the need for unbundling for interfacing to other proof languages.  But since an automated tool could do that for the existing set.mm, I don't see that as a sufficient reason to change set.mm.

If people want to create a set2.mm with the changes you propose, that's fine of course.  But the current FOL= axiomatization in set.mm is stable and essentially finished, it has served well for many years, and I don't see it ever being changed.  I think it is a beautiful thing even if some others may not agree.  It would be a shame to discard it and the significant amount of work that went into it.

Norm

[David A. Wheeler]

On Fri, 26 Apr 2019 05:14:05 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> It is hard to believe that bundling "scares all the serious mathematicians
> away." Are they also scared away from the papers of Tarski and colleagues
> that use bundling freely? Bundling is a trivial concept and the whole
> issue seems to be making a mountain out of a molehill. The advanced
> theorems in set.mm that they would be interested in are unlikely to have
> bundling anyway, so if they are scared away it probably isn't because of that.

I expect that "all" is somewhat hyperbolic, but I believe Mario's report of
his own experiences, so I believe it's true in at least *some* situations.

> The proposal to revamp set.mm to prohibit bundling, add a new variable sort
> for sets with additional axioms, and add a new collection of variable names
> them, would change it from a simple and pure metalanguage to a kind of
> hybrid of metalanguage and quasi-object language that is more complex.

In practice I think those are many separate proposals.
Unbundling, in particular, can be done regardless of whether or not new
typecodes are used.

The result might be much more complex... and it might not be.
Let's discuss ways it *could* be done, and then see what shakes out.
I advocate that we continue to discussion to see what can be done,
preferably incrementally and without massive amounts of new complexity.

Mario's early experiments suggest that bundling, while theoretically
powerful, isn't all that important in *practice*. That's not the same
as a useful final proposal, but it suggests that the investigations are promising.

The "new variable sort" is a very recent proposal. I have serious concerns
about the first cut proposal (in particular all those "duplicate" symbols), so I'm
certainly not sold on that. On the other hand, it's
*already* the case that set variables, sets, and classes (which can be
proper classes) are handled differently in set.mm, so having a new typecode
for sets (different from setvar and class) is not insane on its face.

Let's not cut off discussion too soon.
A more elegant version of at least some of these ideas might result,
or some halfway point might be found.

> To me that is not as elegant and is even somewhat pointless.

Trying to remove stumbling blocks for a number of people and use cases
seems full of point to me :-).


> It would be a shame to discard (set.mm) and the

> significant amount of work that went into it.

I certainly don't advocate for that. Indeed, I plan to continue to
work on set.mm (and iset.mm sometimes).

But there have been a number of
refinements to the set.mm axioms and theorems over the years.
I envision the possibility of a new refinements, including
updating of existing materials so they are *not* discarded.

Let's give their exploration a chance.

--- David A. Wheeler

[Benoit]

On Friday, April 26, 2019 at 5:18:15 PM UTC+2, David A. Wheeler wrote:

The "new variable sort" is a very recent proposal.

No: actually, it's not a proposal at all.  It's only a pedagogical illustration.  The links I gave earlier in this thread contain other interesting information.  As I had proposed in one of those linked threads, maybe "it is worth developing a micro-explorer along these lines, just to show how it would go, for pedagogical purposes".

As for the rest of the thread, I find the experiments by Mario interesting and I look forward to his updates, but I'm with Norm on keeping bundled theorems in set.mm.  Actually, I stand by my first post in this thread and what I called the novelty in Norm's paper "A Finitely Axiomatized..." which is to treat schemes as first-class citizens, hence not shying away from what was later called "bundling".

Benoit

[Mario Carneiro]

On Fri, Apr 26, 2019 at 8:14 AM Norman Megill <n...@alum.mit.edu> wrote:

On Tuesday, April 23, 2019 at 6:13:07 PM UTC-4, Mario Carneiro wrote:

On Mon, Apr 22, 2019 at 1:03 PM David A. Wheeler wrote:

On Sun, 21 Apr 2019 18:33:23 -0700 (PDT), Norman Megill wrote:
> ... Of course Metamath
> proofs are not formal proofs as defined in textbooks (where proof steps are
> object-language instantiations of the axiom and inference rule schemes) ...

I disagree.

Metamath proofs absolutely *are* formal proofs using the usual definition.
"A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the sequence by a rule of inference."
https://en.wikipedia.org/wiki/Formal_proof and The Cambridge Dictionary of Philosophy, deduction
Metamath proofs completely meet that definition, full stop, no qualifiers.

I agree with David here, and I think this an important point. Metamath is built on an intuition that it is formalizing metavariable mathematics, and it has theorems that are schemes over some unstated "object language".

Maybe I'm misunderstanding, but the intended object language isn't unstated; it is described in English in mmset.html.  We define object-language wffs as expressions built from variables v1,v2,... and connectives ->, -., A., =, e. .  The setvar and wff (meta)variables in set.mm range over these variables and formulas.  It is no different from a logic textbook that says, "Let phi and psi be wffs.  The axioms are all formulas of the following forms:  (phi -> (psi -> phi)) [etc.]".

If what you mean is that the object language is not a formal part of the set.mm language, that is true, but there is no need because the object language is never used there.

I suppose we could extend the Metamath language with a mechanism to instantiate its schemes and proof steps into object-language formulas, but that seems unnecessarily pedantic since it is obvious to anyone who has read the English-language description and looked at its examples.  It would just be needless complexity that probably no one would ever use.

My apologies, that came off stronger than intended. Of course this "object language" layer is described in some detail in the documentation. My point is that this is not the only model of metamath theorems, because a first order language (and metamath at the top level is a limited form of first order reasoning) can't completely pin down its models. I hesitate to claim that this implies some incompleteness; in fact I believe that "metalogical completeness" is exactly what I would call "completeness" of this metamath / object language interface. I think the reason is because metamath doesn't have the language to talk about enough of the object language in the first place, i.e. there is no way to refer to v0. For the variables, you end up with the first order language of the "not equal" relation on an infinite set (the variables). This is not finitely axiomatizable but is complete.

 

There is a real impedance mismatch here with logicians, as I've tried to stress. A logician knows how variables work - you don't need to tell them. What's more, you show them a system where 99% of the time variables are acting just like the variables they know. And then in 1% of cases variables do this weird collapsing bound variable capture thing and they are running for the door. My goal with the metamath zero variable rules are to capture the things about metamath variables that make substitution dead simple, while eliminating the weird variable capture thing that scares all the serious mathematicians away.

A logician should know the difference between metavariables and variables, and if not they'll have to spend 5 minutes reading the mmset.html link I provided.  What is so difficult about that?

It is hard to believe that bundling "scares all the serious mathematicians away."  Are they also scared away from the papers of Tarski and colleagues that use bundling freely?  Bundling is a trivial concept and the whole issue seems to be making a mountain out of a molehill.  The advanced theorems in set.mm that they would be interested in are unlikely to have bundling anyway, so if they are scared away it probably isn't because of that.

I think there is some great utility in treating variables the way metamath does, and direct substitution is an important factor in the blazing fast speed of metamath verification, but it's not good for the intuition. We need a good story for how we can go from a system that is fast to a verify to a logic that is well understood and studied. Saying "Tarski did it" doesn't seem to cut it for most people.

 

Tarski was a well-known leader in the field who people take seriously.

There is such a thing as "mainstream logic", and while I wasn't around when Tarski and contemporaries were developing these metavariable systems, I can say with some confidence that this is not mainstream logic anymore, if it ever was. People expect to see FOL, its subsystems, and extensions. There is nothing a priori wrong with investigating other things; indeed that's usually where all the interesting research directions are, but if you are trying to cater to the mainstream then this is a downside.

 

But independently of that, I chose his system because I found it very compelling due to the extreme simplicity of its primitive notions.  A reviewer of Tarksi's 1965 paper (Shepherdson, JSL, 1974) said "the author's observations provide the most elegant and most simply describable axiom systems for predicate logic with identity".

The proposal to revamp set.mm to prohibit bundling, add a new variable sort for sets with additional axioms, and add a new collection of variable names them, would change it from a simple and pure metalanguage to a kind of hybrid of metalanguage and quasi-object language that is more complex. To me that is not as elegant and is even somewhat pointless.

None of those are actual current proposals. I haven't given a concrete proposal yet, besides suggesting that bundling should be avoided (not prohibited). (Actually I'm not even against highly bundled theorems like exrot4, I'm suggesting to limit use of degenerate instances of bundled theorems, i.e. actually taking advantage of bundling.) The actual proposal will probably take the form of some new $j statements that I will have to litter about, plus possibly alternate proofs of degenerate instances to prevent too much recursive degeneration.

As Benoit says, the example with the set term sort is not a proposal, it is an example, in response to a question about what it would look like to have such a thing in metamath. I'm pointing out that there are two different axes here for properties of a sort - the underlying set of things in the domain of discourse (i.e. {T,F} for wffs, V for set, and P(V) for class), and the "variableness" of the sort (i.e. set is a variable sort, wff and class are term sorts). This is a distinction that is made explicit in MM0 and so it helps to have this language for the purpose of discussion.

On Fri, Apr 26, 2019 at 11:18 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Fri, 26 Apr 2019 05:14:05 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> It is hard to believe that bundling "scares all the serious mathematicians
> away."  Are they also scared away from the papers of Tarski and colleagues
> that use bundling freely?  Bundling is a trivial concept and the whole
> issue seems to be making a mountain out of a molehill.  The advanced
> theorems in set.mm that they would be interested in are unlikely to have
> bundling anyway, so if they are scared away it probably isn't because of that.

I expect that "all" is somewhat hyperbolic, but I believe Mario's report of
his own experiences, so I believe it's true in at least *some* situations.

Indeed it's self-refuting: to the extent that I can consider myself a logician, obviously I am not scared away by bundling. But communication with the "outside world" matters a lot to me, because I think metamath does a lot of things right but many people don't invest the time to see the good, and so I'm playing the role of ambassador here to all those logicians who can't be bothered with funny logics.

 

The "new variable sort" is a very recent proposal.  I have serious concerns

about the first cut proposal (in particular all those "duplicate" symbols), so I'm
certainly not sold on that.  On the other hand, it's
*already* the case that set variables, sets, and classes (which can be
proper classes) are handled differently in set.mm, so having a new typecode
for sets (different from setvar and class) is not insane on its face.

I didn't make this clear enough, I think, so let me position that example in the space of ideas. It is *possible* to define a ZFC like metamath database in which there is a sort of set terms, distinct from set variables, and many set theory databases in other languages take this approach. In this formulation you get axioms like pairing expressed as term formers, and unbounded comprehensions don't exist as a term. Probably you wouldn't even have the 'class' sort in such a system.

If you have also a sort of classes, then there is plainly an issue of duplication. The empty set would not be duplicated because there is no need to have a class (/) when "set (/)" is stronger, but things like class union might possibly require two versions - the union of classes is a class, but if both happen to be sets then the union is also a set. "toSet" can be used to eliminate some of that duplication, i.e. you express the set union of two sets as "toSet ( sx u. sy )" using the class union and then coercing back down to a set. This is less nice to work with, though.

A more industrial strength example is https://github.com/digama0/mm0/blob/master/examples/peano.mm0 , which is developing PA in the same way that ZFC is built up in set.mm. Starting from basic arithmetic, you can build up a pairing function (i.e. df-op), and you can use the ackermann bijection to do finite set theory inside nat. This gives you the ability to talk about finite sets, i.e. "nat" is acting as the sort of set terms. But on top of this, I found, just as in set.mm, that it is really convenient to have a sort for arbitrary subsets of nat. Just like in set.mm, this doesn't increase the proof theoretic strength, because you can't quantify over these "proper classes". I define intersection and union of classes, and then the function "lower" is used to turn a class back into a finite set when the class is in fact finite.

While it is possible to define an extension of set.mm with set terms, I have no intention of actually proposing such a thing. I think classes are great, and they are used pervasively in set.mm to great effect. Class functions are very useful, and with only a sort of set terms you can't express this, at least not without having many binding operations. With classes you can have a finite set of "basic binders" and write everything else in terms of that; with only "setvar" and "wff" you need to introduce binders for every new definition that would otherwise be a class.

 

>  It would be a shame to discard (set.mm) and the
> significant amount of work that went into it.

I certainly don't advocate for that.  Indeed, I plan to continue to
work on set.mm (and iset.mm sometimes).

No one is advocating for this. I am actually wondering if I should develop peano.mm0 as a MM database instead, and translate it to MM0. This would require enough annotations in the MM file to ensure that the translation isn't significantly worse than if it were written directly, which is a pretty high bar. Right now I'm having to work from scratch because there is no MM database that implements PA (peano.mm is an experiment, not a practical solution).

Mario

[Norman Megill]

On Friday, April 26, 2019 at 5:40:48 PM UTC-4, Mario Carneiro wrote:

...
 

There is such a thing as "mainstream logic", and while I wasn't around when Tarski and contemporaries were developing these metavariable systems, I can say with some confidence that this is not mainstream logic anymore, if it ever was. People expect to see FOL, its subsystems, and extensions. There is nothing a priori wrong with investigating other things; indeed that's usually where all the interesting research directions are, but if you are trying to cater to the mainstream then this is a downside.

What is "mainstream logic"?

Every mathematical logic book I'm familiar with (that describes a Hilbert-style system for classical FOL=) has exactly the same "object language" as Tarski's system.

The only difference is in the axiom schemes that generate the object language.  Most books start with axiom schemes involving "not free in" and "free for", whereas Tarski's have the simpler notion of "not occurring in".  Tarski derives the former schemes as metatheorems, so his system isn't really different, it just starts with a different but equivalent set of axiom schemes.  All theorems and metatheorems of both systems are the same.

And I'm struggling to find a book that requires x and y (as metavariables) to be distinct in their metatheorems for our ax-7 and ax-11 (quantifier commutation), so it seems they are allowing bundling at least in some cases.

 Norm

[Mario Carneiro]

On Fri, Apr 26, 2019 at 8:01 PM j4n bur53 <burs...@gmail.com> wrote:

I dont think bound variables are easily meta variables, that can
be freely renamed. Renaming has to obey also some rules.
Renaming is alfa conversion, which similarly like beta conversion,

is based on substitution. And subsequently needs to be capture
avoiding. Here is an example of a theorem that gets wrong,
when a wrong alfa conversion is done:

I think this is a decent example of the kind of confusion that can result from misunderstanding how metamath variables work by using intuitions from FOL. In this case, the metamath theorem would have a disjoint variable condition between x and y, that would prevent substitution of the same variable for both. So that FOL theorem is still expressible in metamath but it has a proviso that is not present or at least not explicit in the FOL version, that those variables can be "alpha renamed" but they can't be renamed to the same thing, which avoids the problem.

In metamath, substitution is always direct, and capture avoiding is done by disallowing any substitutions that would potentially be problematic wrt bound variable capture.

Norm: I want to point out that Jan is using natural deduction in his example. When I was taught logic at CMU, they used natural deduction. My proof theory course used natural deduction for first order logic (along with many variations, like one-sided vs two sided calculi). My modal logic course used a HIlbert calculus without explicit commitment to axioms ("all classical tautologies" was one of the schemata); we only briefly touched on first order logic. My model theory class, in a different department, used FOL (the proof theory wasn't important so it was not introduced). And of course the type theorists all use natural deduction and the simply typed lambda calculus to draw the Curry Howard correspondence. My higher order typed compilation course used a variety of type systems but variables are treated using de Bruijn indices and/or explicit substitution calculi. At least where I live, this is what "mainstream" looks like. Explicit variables are in the minority, Hilbert logics are in the minority, and metavariable logics are nonexistent except when I talk to people about metamath.

Mario

[Mario Carneiro]

On Fri, Apr 26, 2019 at 8:26 PM j4n bur53 <burs...@gmail.com> wrote:

Well I should write the proof more precisely:

               ---------------- (Reflexivity of =)
             |- f(v0) = f(v0)
             ---------------------------- (Exists Intro)
             |- exists v1 f(v0) = v1
             -------------------------------------- (Forall Intro)

             |- forall v0 exists v1 f(v0) = v1

I do not exclude the possibility, if meta variables are used
in the above proof in place of v0 and v1, or any other proof

with the same outcome, that a side condition x <> y might
result. Is this demonstrable in meta math?

This theorem is easily provable in metamath. Since f(v0) is a term, and set.mm's FOL= fragment doesn't have any terms, we need the extension to classes. Then we can write ( F ` x ) in place of f(v0). So the proof looks like this:

$d x y $. $d y F $.

1::fvex |- ( F ` x ) e. _V

2:1:isseti |- E. y y = ( F ` x )

3:2:ax-gen |- A. x E. y y = ( F ` x )

Because isseti has a DV condition between its two variables, disjointness of y and ( F ` x ) requires that y be disjoint from F and from x. So you can't substitute x and y for the same variable and thus prove |- A. x E. x x = ( F ` x ) using this theorem.

 

--
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.

[Mario Carneiro]

Metamath (or at least set.mm) doesn't have propositional quantifiers. There are theorem schema over propositional variables, but those can only ever act like universal quantifiers.

On Fri, Apr 26, 2019 at 8:42 PM j4n bur53 <burs...@gmail.com> wrote:

Ok, a different proof. And some curriosity. Reminds me
of Chapter 14: Propositional Quantifiers, Dov M.

Gabbay his exists p (p <-> A). How do you introduce
exists quantifier otherwise in metamath?

Am Samstag, 27. April 2019 02:33:23 UTC+2 schrieb Mario Carneiro:

This theorem is easily provable in metamath. Since f(v0) is a term, and set.mm's FOL= fragment doesn't have any terms, we need the extension to classes. Then we can write ( F ` x ) in place of f(v0). So the proof looks like this:

$d x y $. $d y F $.

1::fvex |- ( F ` x ) e. _V

2:1:isseti |- E. y y = ( F ` x )

3:2:ax-gen |- A. x E. y y = ( F ` x )

Because isseti has a DV condition between its two variables, disjointness of y and ( F ` x ) requires that y be disjoint from F and from x. So you can't substitute x and y for the same variable and thus prove |- A. x E. x x = ( F ` x ) using this theorem.

 

Am Samstag, 27. April 2019 02:19:28 UTC+2 schrieb Mario Carneiro:

On Fri, Apr 26, 2019 at 8:01 PM j4n bur53 <burs...@gmail.com> wrote:

I dont think bound variables are easily meta variables, that can
be freely renamed. Renaming has to obey also some rules.
Renaming is alfa conversion, which similarly like beta conversion,

is based on substitution. And subsequently needs to be capture
avoiding. Here is an example of a theorem that gets wrong,
when a wrong alfa conversion is done:

I think this is a decent example of the kind of confusion that can result from misunderstanding how metamath variables work by using intuitions from FOL. In this case, the metamath theorem would have a disjoint variable condition between x and y, that would prevent substitution of the same variable for both. So that FOL theorem is still expressible in metamath but it has a proviso that is not present or at least not explicit in the FOL version, that those variables can be "alpha renamed" but they can't be renamed to the same thing, which avoids the problem.

In metamath, substitution is always direct, and capture avoiding is done by disallowing any substitutions that would potentially be problematic wrt bound variable capture.

Norm: I want to point out that Jan is using natural deduction in his example. When I was taught logic at CMU, they used natural deduction. My proof theory course used natural deduction for first order logic (along with many variations, like one-sided vs two sided calculi). My modal logic course used a HIlbert calculus without explicit commitment to axioms ("all classical tautologies" was one of the schemata); we only briefly touched on first order logic. My model theory class, in a different department, used FOL (the proof theory wasn't important so it was not introduced). And of course the type theorists all use natural deduction and the simply typed lambda calculus to draw the Curry Howard correspondence. My higher order typed compilation course used a variety of type systems but variables are treated using de Bruijn indices and/or explicit substitution calculi. At least where I live, this is what "mainstream" looks like. Explicit variables are in the minority, Hilbert logics are in the minority, and metavariable logics are nonexistent except when I talk to people about metamath.

Mario

--
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 meta...@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.

[Mario Carneiro]

I think this paper deserves a second mention. It is a proof of the soundness of a very metamath-like FOL= axiomatization. They compare it to metamath by saying that they have eliminated substitution entirely, rather than just limiting it to direct substitution.

C1 |- (p→q)→(q→r)→(p→r)
C2 |- (¬p→p)→p
C3 |- p→¬p→q
C4 |- (∀x.p→q)→(∀x.p)→(∀x.q)
C51 |- p→(∀x.p), x does not occur in p
C52 |- ¬(∀x.p)→(∀x.¬(∀x.p))
C53 |- (∀x.∀y.p)→(∀y.∀x.p)
C6 |- ¬(∀x.¬x=y)
C7 |- x=y→x=z→y=z
C8 |- x=y→p→(∀x.x=y→p), x =/= y
MP If |- (p→q) and |- p then |- q
Gen If |- p then |- ∀x.p

Someone familiar with metamath will then say, what about those variables p, q in the axioms? Don't they have to be substituted? The implementation gets around this by having all of these be axiom schemata, i.e. there is a C1 axiom for each choice of wff p,q,r, and a version of C51 for any variable x and wff p not containing x.

This is not really a practical system to work in, because you can't prove theorem schemata without a metalogic (like Isabelle) to be able to quantify over variables and prove schema from schema. Metamath supports the application of schemata directly, and so can dispense with the logical foundation at the expense of needing simple substitution (which was there in the metalogic before).

So I think the import of this paper is to lend additional credence to FOL= axiomatizations along metamath lines. In fact those axioms look cribbed straight from set.mm itself, although the first three axioms are a bit different. Does anyone else write C8 like that?

On Fri, Apr 26, 2019 at 8:15 PM j4n bur53 <burs...@gmail.com> wrote:

BTW: Meta math has a notable mention in this paper:

Substitutionless First-Order Logic: A Formal Soundness Proof

Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull and Jørgen Villadsen

DTU Compute, AlgoLoG, Technical University of Denmark, 2800 Kongens Lyngby, Denmark

https://files.sketis.net/Isabelle_Workshop_2018/Isabelle_2018_paper_3.pdf

Am Samstag, 27. April 2019 02:01:54 UTC+2 schrieb j4n bur53:

I dont think bound variables are easily meta variables, that can
be freely renamed. Renaming has to obey also some rules.
Renaming is alfa conversion, which similarly like beta conversion,

is based on substitution. And subsequently needs to be capture
avoiding. Here is an example of a theorem that gets wrong,
when a wrong alfa conversion is done:

FOL Theorem, provable in FOL:

       forall x exists y f(x) = y

Here is a proof, in natural deduction:

             ---------------- (Reflexivity of =)
             |- f(x) = f(x)
             ------------------------ (Exists Intro)
             |- exists y f(x) = y
             --------------------------------- (Forall Intro)
             |- forall x exists y f(x) = y

And here what happens if I blindly rename x to y:

            |- forall y exists y f(y) = y
 
Which is not anymore a theorem of FOL.

--

[Mario Carneiro]

Ah, you are right, the C1-8 axioms are directly from Monk (1965). The three versions of C5 are needed because Monk's version is

C51 |- p→(∀x.p), x e/ FV(p)

and they are trying to avoid the FV predicate. I'm not sure if the idea to combine the rules for negation and forall into one rule is original with metamath or is in one of these older logics. Norm will probably know.

On Fri, Apr 26, 2019 at 9:25 PM j4n bur53 <burs...@gmail.com> wrote:

Maybe its a quick rip-off, to get quickly a foot into the door.
Since I couldn't find something longer than the abstract,
and since I dont understand their GitHub, I stopped

looking at it. Inside their abstract they refer to (Monk, 1965)
as an early inspiration. Maybe one would need to start a
study there...?
 

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@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.

[Norman Megill]

On Friday, April 26, 2019 at 8:19:28 PM UTC-4, Mario Carneiro wrote:
...

Norm: I want to point out that Jan is using natural deduction in his example. When I was taught logic at CMU, they used natural deduction. My proof theory course used natural deduction for first order logic (along with many variations, like one-sided vs two sided calculi). My modal logic course used a HIlbert calculus without explicit commitment to axioms ("all classical tautologies" was one of the schemata); we only briefly touched on first order logic. My model theory class, in a different department, used FOL (the proof theory wasn't important so it was not introduced). And of course the type theorists all use natural deduction and the simply typed lambda calculus to draw the Curry Howard correspondence. My higher order typed compilation course used a variety of type systems but variables are treated using de Bruijn indices and/or explicit substitution calculi. At least where I live, this is what "mainstream" looks like. Explicit variables are in the minority, Hilbert logics are in the minority, and metavariable logics are nonexistent except when I talk to people about metamath.

 

I agree that Metamath might be the only "metavariable logic" system.

In other systems, people (or at least textbooks) also use theorem schemes, at least informally.  These schemes are typically backed by informal proofs that reference earlier such schemes.  Metamath simply formalizes the derivation of theorem schemes from earlier theorem schemes.

If people don't grasp that, it can be confusing.  Maybe we have to communicate that better.

Norm

[Norman Megill]

On Friday, April 26, 2019 at 9:34:10 PM UTC-4, Mario Carneiro wrote:

Ah, you are right, the C1-8 axioms are directly from Monk (1965). The three versions of C5 are needed because Monk's version is

C51 |- p→(∀x.p), x e/ FV(p)

and they are trying to avoid the FV predicate. I'm not sure if the idea to combine the rules for negation and forall into one rule is original with metamath or is in one of these older logics. Norm will probably know.

It is original in Monk's paper.  C5 is split into axioms C5-1,2,3 on p. 113.

Most of the set.mm axioms are from Tarski's and Monk's systems as acknowledged in their comments.  Historically, set.mm started with the now-obsolete axioms in my 1995 paper (see the "[Megill]" column in the table at http://us.metamath.org/mpeuni/mmset.html#oldaxioms)  and over time I was able to replace them with axioms as close to Tarski's and Monk's as possible.  Neither Tarski's system nor Monk's system is a "metavariable logic" in the Metamath sense, so I didn't know a priori whether they would be sufficient to replace most of the original set.mm axioms.  Generally I've called them "Tarksi's axioms" because Monk's lack direct substitution (ax-8,9), and our/Monk's ax-10 to ax-13 are metatheorems in Tarski's system.

C1,2,3 are a classical prop calc formalization of Lukasiewicz, theorems luk-1,2,3 in set.mm.  Tarski and Monk chose that system because it has the fewest total symbols or something like that.  I chose ax-1,2,3 (also due to Lukasiewicz) because it was more popular in the literature and I was used to it.

Norm

[Norman Megill]

Mario used the term "metavariable logic" so I repeated it.  I understood what he meant:  it derives theorem schemes (metatheorems) directly from earlier theorem or axiom schemes, and each "theorem" represents a scheme, and each proof step represents a scheme.  I'm not sure whether there is a universally agreed-upon definition of "logic"; perhaps only the intended object language could be considered a logic, in which case I don't know what to call Metamath.  Maybe "metavariable system" is better.

Wiktionary defines a logic as "A formal or informal language together with a deductive system or a model-theoretic semantics."

For a formal specification see Mario's "Models for Metamath".
http://arxiv.org/abs/1601.07699
http://us.metamath.org/ocat/model/model.pptx.pdf (slides)

For a less formal specification (that defines what a verifier must do) see pp. 110-113 of the Metamath book.
http://us.metamath.org/downloads/metamath.pdf

Norm


On Saturday, April 27, 2019 at 10:30:44 AM UTC-4, j4n bur53 wrote:

Now these claims deeply confuse me.

Well metamath is a metavariable system, but not a metavariable logic.
Since the metavariable logic itself is not formalized, its only used.
I guess what happens with variable disjunction conditions etc.. is

what the verifier does with a text based on the many keywords
$c, $v, etc... So would need to look at the verifier. Also test cases
are not really a formal specification. A formal specification

would be some axioms and definitions of the metavariable logic
in some logic, so as to make it a logic. Basically all what would
need to be formalized is the verifyer itself to get to a

metavariable logic, maybe the Haskel implementation of the verifier
can be used to produce a metavariable logic:

HmmImpl.hs:

        {-
           In the following definition we compute the DVRSet on top of the stack as
           follows:

            (1) First we collect all DVRs of the hypotheses that are popped off the
            stack.

            (2) We add the DVRs of the assertion that we are processing, after
            applying the substitution to it.

            (3) We select only those DVRs that occur in the new expression on top
            of the stack.

    :-}

Maybe there are shortcuts, or it can be done indirectly. And
maybe ultimately the metamath metavariable logic could be
done directly inside metamath. Kind of reflecting metamath

metavariable logic, in metamath itself. Such things have already
a long tradition. Like 10 years ago HOAS was en vogue, dunno
what the latest trend is. Ultimately a metavariable logic would

maybe reify the DVRs somehow. Not sure. I know about another
 metavariable logic based on deBruijn indexes, there is a paper
by Huet, with what he calls "The Prism Theorem" in it. Just

doing a fresh googling I find this quite interesting paper, which
I did not yet see, which shows various takes on metavariable
logics, a paper which might be more accessible than Huets:

Proof Pearl: De Bruijn Terms Really Do Work
Michael Norrish and Ren´e Vestergaard
https://www.researchgate.net/publication/221302248_Proof_Pearl_De_Bruijn_Terms_Really_Do_Work

Does have metamath such a matevariable logic specification,
where the verifyer itself is axiomatized?

[Mario Carneiro]

Good news: The MM -> MM0 translation works! It produces unbundled copies of MM theorems and runs them successfully through the MM0 verifier. (So mm0-hs finally counts as another MM verifier, if in a very roundabout way.) Moreover, I implemented the preprocessing step I described in the original post to reduce the number of superfluous unbundlings. The algorithm is as follows:

* If a term constructor has only bound (setvar) arguments, then they can't bind anything because there aren't any regular variables, so free all of them. The canonical example of this is cv: setvar -> class. This is not a binder even though it uses a set variable - this is the way that free set variables appear in class terms. If weq was a primitive term constructor instead of an abbreviation, it would also be eligible by this rule.

* If a theorem or axiom uses no term constructor or theorem in the statement or proof that requires that its argument be bound, then free this variable in the theorem. This is how the set variables in ax-7 are freed.

Here is the new, reduced list of bundled theorems:

105 bundled theorems, 130 total copies
2exbidv          [[0,0]]
exlimivv         [[0,0]]
df-sb            [[0,0]]
sbequ2           [[0,0]]
sb1              [[0,0]]
ax-11            [[0,0]]
hbal             [[0,0]]
hbald            [[0,0]]
ax-12            [[0,0]]
nfal             [[0,0]]
nfald            [[0,0]]
sbequ1           [[0,0]]
sbequ12          [[0,0]]
sbequ12r         [[0,0]]
axc11nlem1       [[0,0]]
axc11nlem2       [[0,0]]
axc112           [[0,0]]
axc11n           [[0,0]]
aecoms           [[0,0]]
naecoms          [[0,0]]
axc11            [[0,0]]
hbae             [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
nfae             [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
hbnae            [[0,1,0],[0,1,1]]
nfnae            [[0,0,0],[0,0,1],[0,1,0],[0,1,1]]
aevlem1          [[0,1,0]]
axc16g           [[0,0]]
aev              [[0,0,1],[0,1,0],[0,1,1]]
a16nf            [[0,0]]
a16gb            [[0,0]]
dral2            [[0,0,1],[0,1,0]]
dral1            [[0,0]]
drex1            [[0,0]]
drex2            [[0,0,0],[0,1,0]]
drnf1            [[0,0]]
drnf2            [[0,1,0]]
nfald2           [[0,0]]
dvelimf          [[0,0,1],[0,1,0]]
dvelimdf         [[0,0,1],[0,1,0]]
sb2              [[0,0]]
sb4              [[0,0]]
sbequi           [[0,1,0],[0,1,1]]
sbequ            [[0,1,0],[0,1,1]]
drsb1            [[0,1,0]]
drsb2            [[0,1,0],[0,1,1]]
sbequ5           [[0,1,2,1]]
nfsb4t           [[0,1,0]]
sbcom3           [[0,1,0]]
nfsbd            [[0,1,0]]
ax-c11           [[0,0]]
aecom-o          [[0,0]]
aecoms-o         [[0,0]]
hbae-o           [[0,1,0],[0,1,1]]
axc711           [[0,0]]
axc5c711         [[0,0]]
hbnae-o          [[0,1,0],[0,1,1]]
dral2-o          [[0,1,0],[0,1,1]]
aev-o            [[0,1,2,0]]
df-clab          [[0,0]]
drnfc1           [[0,0]]
nfabd2           [[0,0]]
nfabd            [[0,0]]
dvelimdc         [[0,0,1]]
dvelimc          [[0,0,1]]
nfcvf            [[0,0]]
nfcvf2           [[0,0]]
cbvral2v         [[0,1,2,0]]
dfsbcq2          [[0,0]]
sbsbc            [[0,0]]
nfsbcd           [[0,0]]
nfcsbd           [[0,0]]
nfcsb            [[0,0]]
df-opab          [[0,0,1]]
elopab           [[0,0]]
dfid3            [[0,0]]
djudisj          [[0,0]]
fmpt2d           [[0,0]]
xporderlem       [[0,1,2,3,2,3]]
rdglem1          [[0,1,2,0,3,4]]
eqerlem          [[0,1,2,2]]
fin23lem28       [[0,1,2,3,4,2,5,6]]
fin23lem29       [[0,1,2,3,4,2,5,6]]
fin23lem30       [[0,1,2,3,4,2,5,6]]
fin23lem31       [[0,1,2,3,4,5,2,6,7]]
fin23lem32       [[0,1,2,3,4,5,6,2,7,8,9]]
suprlub          [[0,1,1]]
suprleub         [[0,1,0],[0,1,1]]
infmrgelb        [[0,1,0],[0,1,1]]
btwnz            [[0,0]]
isfild           [[0,1,0]]
metequiv         [[0,1,2,2,1]]
evthicc          [[0,1,0,1],[0,1,2,1]]
norm1exi         [[0,0]]
norm1hex         [[0,0]]
fcobijfs         [[0,0,1]]
mzpclval         [[0,1,0,1,1,2]]
elmzpcl          [[0,1,0,1,1]]
axc5c4c711       [[0,0]]
ovmpt3rab1       [[0,1,2,1,3,4]]
elovmpt3rab1     [[0,1,2,1,3,4]]
2wlkeq           [[0,0]]
bnj1307          [[0,1,1,2]]
bj-hbaeb         [[0,1,1]]
cdlemk22         [[0,1,2,3,3,0]]
cdlemn2a         [[0,0]]

The axioms on this list are ax-11, ax-12 and ax-c11, which all involve two quantifiers on x and y, so it's not a surprise that they are marked as needing unbundling.

The ones that are directly referenced in unbundled theorems have to be there; there isn't much we can do about that without rewriting the proofs. But there is a lot of transitive degeneration going on here. Let's say that the degeneration level of a degenerated theorem is n+1 if every reference to the theorem is from level n degenerated theorems. So a level 0 theorem is not degenerated, a level 1 theorem is a degenerate instance directly referenced by a nondegenerate theorem, a level 2 theorem is only referenced by level 1 theorems, and so on. What if we say that only level 1 degenerated theorems are permitted? If we restrict our attention only to level 1 theorems that make one or more reference to a level 2 theorem, we get the following list of violations:

theorem aev[0,1,0] references aevlem1[0,1,0]
theorem axc16g[0,0] references aevlem1[0,1,0]
theorem axc5c4c711[0,0] references ax-11[0,0]
theorem axc5c711[0,0] references ax-11[0,0]
theorem axc711[0,0] references ax-11[0,0]
theorem bj-hbaeb[0,1,1] references hbae[0,1,1]
theorem dfid3[0,0] references df-opab[0,0,1], drex1[0,0], drex2[0,0,0], nfcvf2[0,0], nfnae[0,0,0]
theorem drsb1[0,1,0] references df-sb[0,0]
theorem drsb2[0,1,0] references sbequ[0,1,0]
theorem elmzpcl[0,1,0,1,1] references mzpclval[0,1,0,1,1,2]
theorem elopab[0,0] references 2exbidv[0,0], df-opab[0,0,1], exlimivv[0,0]
theorem elovmpt3rab1[0,1,2,1,3,4] references ovmpt3rab1[0,1,2,1,3,4]
theorem fin23lem32[0,1,2,3,4,5,6,2,7,8,9] references fin23lem28[0,1,2,3,4,2,5,6], fin23lem31[0,1,2,3,4,5,2,6,7]
theorem hbae[0,1,0] references ax-11[0,0], axc112[0,0]
theorem hbae-o[0,1,0] references aecoms-o[0,0], ax-11[0,0], ax-c11[0,0]
theorem hbae-o[0,1,1] references aecoms-o[0,0], ax-c11[0,0]
theorem hbnae[0,1,1] references hbae[0,1,1]
theorem nfae[0,1,1] references hbae[0,1,1]
theorem sbcom3[0,1,0] references drsb2[0,1,1], sbequ[0,1,1]
theorem sbequ12[0,0] references sbequ1[0,0], sbequ2[0,0]

19 bundled theorems, 20 total copies
sbequ12          [[0,0]]
hbae             [[0,1,0]]
nfae             [[0,1,1]]
hbnae            [[0,1,1]]
axc16g           [[0,0]]
aev              [[0,1,0]]
drsb1            [[0,1,0]]
drsb2            [[0,1,0]]
sbcom3           [[0,1,0]]
hbae-o           [[0,1,0],[0,1,1]]
axc711           [[0,0]]
axc5c711         [[0,0]]
elopab           [[0,0]]
dfid3            [[0,0]]
fin23lem32       [[0,1,2,3,4,5,6,2,7,8,9]]
elmzpcl          [[0,1,0,1,1]]
axc5c4c711       [[0,0]]
elovmpt3rab1     [[0,1,2,1,3,4]]
bj-hbaeb         [[0,1,1]]

Now we are really down to just a handful. I would propose to provide alternate proofs for these degenerated instances so that there isn't so much of a cascade of degeneration. In almost all cases a degenerated instance is a trivial consequence of a different theorem.

On Tue, Apr 30, 2019 at 3:38 AM j4n bur53 <burs...@gmail.com> wrote:

But it could also be the case that metamath is somehow resilient,
since the other example, Mario Carneiro used x e V, in the

forall x exists y (f(x)=y) versus exists y(f(y)=y) example.
So if conditions such as x e V are stll hanging around,

Then this rule does not apply:

           (3) We select only those DVRs that occur in the new expression on top
            of the stack.

But I might also misinterpret (3). I interpret it as a kind
of garbage collection(*) of DVRs?

(*) Which makes it an interesting problem also for
system implementors, not only logicians.

Am Dienstag, 30. April 2019 09:31:50 UTC+2 schrieb j4n bur53:

Comming from constraint solving, this step here in the verifier:

          (3) We select only those DVRs that occur in the new expression on top
            of the stack.

Could be problematic. I know some examples from SMT where this
dropping constraints gives wrong answers, false positives. Unfortunately
this would need me some time, to dig them out.

But I guess I have found an example outside SMT, and inside metamath,
which could show some pathological behaviour:

   |- ALL(x):ALL(z):[{x}=z <=> ALL(u):[u ε z <=> x=u]]
    --------------------------------------------------- (ALL Elim)

    |- ALL(z):[{x}=z <=> ALL(u):[u ε z <=> x=u]]
    -------------------------------------------- (ALL Elim)  ---------- (Refl)
    |- {x}={x} <=> ALL(u):[u ε {x} <=> x=u]]                 |- {x}={x}
    ------------------------------------------------------------------- (MP)
              |- ALL(u):[u ε {x} <=> x=u]]
              ----------------------------- (ALL Elim)
                   |- y ε {x} <=> x=y

The second natural deduction (ALL Elim) , where I use the
substitution z-->{x}, would provoke a caputure avoiding variable
constraint u not in x.

But since u does not appear in the result y ε {x} <=> x=y,
the constraint would be dropped. But what if in some further
course u would be nevertheless used again?

So a verified verifier could be useful. The verification of the
verifier itself could fail, because of such problematic cases.

--

[Giovanni Mascellani]

Hi Mario,

Il 03/05/19 10:06, Mario Carneiro ha scritto:

> Good news: The MM -> MM0 translation works! It produces unbundled copies
> of MM theorems and runs them successfully through the MM0 verifier. (So
> mm0-hs finally counts as another MM verifier, if in a very roundabout
> way.)

That's very nice news! :-)

I tried and I managed to so the translation and verification too with
your Haskell program.

Since I believe that your MM0 specification might now be considered
nearly frozen (what is your opinion on this?), I brushed off my project
of writing an independent verifier in G. In preparation for that I began
writing a Python implementation, to understand the specification and to
use it as a model for the G implementation. I'm working on a clone of
your repository which is here:

https://github.com/giomasce/mm0/blob/master/mm0-py/parser.py

A question: in the specs it is said that dummy variables are always
bound. Does this mean that it is illegal to declare a dummy variable
with round brackets, or that if a dummy variables it is declared in
round brackets it is automatically considered as declared in braces? If
so, is there a difference between a dummy variable in round brackets or
in braces (i.e., "(.x : set)" vs "{.x : set}")? For example, in
examples/set.mm0 definition wtru has "(.p: wff)". Now, if p must be
considered bound, then it violates the requirement that a bound variable
cannot have a strict sort; if p must be considered unbound, then it
violates the requirement that a dummy variable must be bound. What am I
missing?

Regarding the G compiler from asmc, I wrote a simple emulator for a
subspec of 32 bit x86 machine code that is enough to execute the asmc OS
together with its G compiler and the code produced by the G compiler,
therefore ideally the MM0 verifier implementation in G once it will
exist. The emulator is about 1000 lines of rather clean and readable
C++, so it is helpful to pinpoint exactly what asmc assumes from its
platform. Therefore if we want prove correctness for asmc, G and the G
MM0 checker we know what we must assume as the execution environment,
and it is reasonable (for how the x86 can be reasonable).

On the other hand the emulator is pretty slow, and it is not able to
execute general x86 code. It is optimized for code cleanness and for not
supporting anything more than what G compiled programs need.

The code is here:

https://gitlab.com/giomasce/simplevm

Good to see that plans are going forward, and thank you!

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Mario Carneiro]

On Fri, May 3, 2019 at 5:19 AM Giovanni Mascellani <g.masc...@gmail.com> wrote:

Hi Mario,

Il 03/05/19 10:06, Mario Carneiro ha scritto:
> Good news: The MM -> MM0 translation works! It produces unbundled copies
> of MM theorems and runs them successfully through the MM0 verifier. (So
> mm0-hs finally counts as another MM verifier, if in a very roundabout
> way.)

That's very nice news! :-)

I tried and I managed to so the translation and verification too with
your Haskell program.

Since I believe that your MM0 specification might now be considered
nearly frozen (what is your opinion on this?),

There is only one remaining spec change that I am considering, which is to split "delimiter" into two. That is, currently looks like

delimiter $ ( ) / $;

and would instead look like

delimiter $ ( / $ $ ) / $;

A left delimiter (delimiters in the first group) is one which splits the string after the token, and a right delimiter splits before the token. (Currently every delimiter is both a left and right delimiter.) This allows us to have $($ as left delimiter and $)$ as right delimiter, while still allowing $f($ to be a token, which is very useful for composite notations or decorated brackets.

I'm also thinking of making it part of the spec that delimiters are always one character - the implementation already does this and specifying how multi-character delimiters overlap is cumbersome.

I brushed off my project
of writing an independent verifier in G. In preparation for that I began
writing a Python implementation, to understand the specification and to
use it as a model for the G implementation. I'm working on a clone of
your repository which is here:

  https://github.com/giomasce/mm0/blob/master/mm0-py/parser.py

Great! The more languages the better.

 

A question: in the specs it is said that dummy variables are always
bound. Does this mean that it is illegal to declare a dummy variable
with round brackets, or that if a dummy variables it is declared in
round brackets it is automatically considered as declared in braces? If
so, is there a difference between a dummy variable in round brackets or
in braces (i.e., "(.x : set)" vs "{.x : set}")? For example, in
examples/set.mm0 definition wtru has "(.p: wff)". Now, if p must be
considered bound, then it violates the requirement that a bound variable
cannot have a strict sort; if p must be considered unbound, then it
violates the requirement that a dummy variable must be bound. What am I
missing?

Dummy variables are always considered bound, regardless of the kind of brackets used. Both bracket kinds are legal but it makes no difference.

 

Regarding the G compiler from asmc, I wrote a simple emulator for a
subspec of 32 bit x86 machine code that is enough to execute the asmc OS
together with its G compiler and the code produced by the G compiler,
therefore ideally the MM0 verifier implementation in G once it will
exist. The emulator is about 1000 lines of rather clean and readable
C++, so it is helpful to pinpoint exactly what asmc assumes from its
platform. Therefore if we want prove correctness for asmc, G and the G
MM0 checker we know what we must assume as the execution environment,
and it is reasonable (for how the x86 can be reasonable).

For the x86 side, I've been looking into importing a formal specification from other projects, to encourage cross compatibility and reliability (these other specs tend to already be somewhat torture tested). Notable mentions include the K framework, which is publishing "the most complete formal x86 specification" at PLDI 2019 (paper: http://fsl.cs.illinois.edu/FSL/papers/2019/dasgupta-park-kasampalis-adve-rosu-2019-pldi/dasgupta-park-kasampalis-adve-rosu-2019-pldi-public.pdf , github: https://github.com/sdasgup3/binary-decompilation/tree/pldi19_AE_ConcreteExec/x86-semantics ), and the Sail language, which is designed for specifying ISAs and has a surprisingly short specification of x86, or at least the useful fragment of it (homepage: https://www.cl.cam.ac.uk/~pes20/sail/ , github: https://github.com/rems-project/sail/blob/master/x86/x64.sail ).

I'm not sure there is going to be a high level language at all, though. The goal is to show that some bit of assembly code performs some high level function, but that only requires a concrete syntax at the lowest level (i.e. sequences of machine code bytes), and the rest is theorems and abstractions on top of that. Since I'm not writing a compiler per se, there is no input language, only an input abstract specification. However, since it's not practical to write theorems about every opcode by hand, obviously there will be some theorems for putting stuff together into logical units and manipulating them, and the "input language" will thus end up being whatever tactic language or proof script is used to generate the proof itself. This can be at a G like level, but there is no parsimony constraint on a tactic language since it's only a macro language to build the final proof.

I'm still in the planning stages of this aspect of the proof, but I think there will at least be the following layers of abstraction in the proof:

* Assembly: e.g. prove that 03 3B adds the memory at EBX to EDI. (Whether there will be an explicit assembly AST, i.e. ADD edi, [ebx] is still up for debate.)

* Merge short runs of straight-line assembly into actions on the state of the machine, e.g. running (sequence of bytes) starting from EAX = x and EBX = y results in EAX = (x + y)^2, with EBX and R11 being clobbered (set to an unspecified value)

* Analysis of control flow. The easy theorems will presume that the program is generated from loop and conditional type constructs, and labels are invented nondeterministically (i.e. the assembler knows the future and always puts the right values in the jump slots). This part is usually not automatic in verified programming languages, so some source text will be spent here on giving loop invariants and so on.

* Call graph analysis. I don't think there will be a global stack unless it becomes necessary; it's simpler and faster to just use actual stacks with custom memory management. More important is the hygienic use of global private state, which alleviates the need for any memory allocation after the start of the program.

I'm quite excited about the potential performance gains to be had at the end of the process. Stefan O'Rear wrote the blazingly fast smm verifier for metamath, that can verify set.mm in about a second, but I think that putting together all the advancements in low level control of the code, and design of the (as yet undisclosed) binary mm0 proof format, I think this will be the fastest verifier for any proof language. And it will need to be, because these CS style proofs are much larger than most metamath verifiers are used to dealing with.

Mario

[Giovanni Mascellani]

Hi,

Il 03/05/19 12:14, Mario Carneiro ha scritto:

> Dummy variables are always considered bound, regardless of the kind of
> brackets used. Both bracket kinds are legal but it makes no difference.

But then, why is it this line in examples/set.mm0 valid?

def wtru (.p: wff): wff = $ p <-> p $;

Dummy variables are always bound, but bound variables cannot have strict
type, and wff is strict.

The set.mm0 converted from set.mm does not have the equivalent
definition, because it inherits the definition-by-axiom construction
from set.mm.

Thanks, Giovanni.

[Benoit]

Mario, I might be missing something, but I don't understand the conjunction of your two claims:

"The MM -> MM0 translation works! It produces unbundled copies of MM theorems"

"I would propose to provide alternate proofs for these degenerated instances"

Doesn't your algorithm do precisely this? (or does it only prove the "principal instance" of the bundled theorems, and not the degenerate ones?) If your algorithm provides the needed translation, the good news would be that set.mm does not need to be altered, it seems to me?

Benoît

[Mario Carneiro]

On Fri, May 3, 2019 at 8:13 AM Giovanni Mascellani <g.masc...@gmail.com> wrote:

Hi,

Il 03/05/19 12:14, Mario Carneiro ha scritto:
> Dummy variables are always considered bound, regardless of the kind of
> brackets used. Both bracket kinds are legal but it makes no difference.

But then, why is it this line in examples/set.mm0 valid?

  def wtru (.p: wff): wff = $ p <-> p $;

Dummy variables are always bound, but bound variables cannot have strict
type, and wff is strict.

Hm, I think you've found a bug, but I'm not sure whether it lies in the spec, the verifier, or in my understanding. The spec only says that a variable of strict type cannot appear as a dependency in another variable, so by a strict reading it should be allowed. The verifier checks wellformedness separately for bound variables and dummy variables, and the strict check only appears on bound variables, hence why it passes. They both have the same effect on the context though, so that seems suspicious at best. Even the formal specification mm0.mm0 is okay with this, because in the definition of DefOk, the context is checked for well formedness before appending dummies but not after, so the context actually might be invalid when the expression is checked. That's certainly an error, which would come up once I start using this to prove things. Still it's pretty amazing that three different bugs all line up like that.

This is actually related to a problem I've just encountered in my translation to HOL, which has started going in a weird direction because of exactly this issue. The mapping from MM0 to HOL was designed to be relatively straightforward, but one place where things are weird are definitions like this one: A sort which is not "free" permits the dropping of dependencies in the return type of the def, which supports definitions like wtru there. In metamath we justify this after the fact with a justification theorem, but MM0 doesn't have that luxury. To really drive the point home, this is also a valid MM0 definition right now:

  def foo (.p: wff): wff = $ p $;

This is really bizarre. The HOL translation doesn't know what to make of this, and MM would be inconsistent if it allowed the axiom |- foo <-> p, so how can this possibly be okay? The interpretation of this definition is that there exists a choice of p from the underlying sort "wff" such that the equation foo <-> p holds. We can encode this in HOL via a higher order quantification like so:

forget_foo : (!p (|- foo == p => |- ph)) => |- ph

where the !p is meta-forall quantification and |- foo == p is the convertibility judgment (used for unfolding definitions). Without the continuation passing style, it's also equivalent to an existential quantification like so:

some_foo : ?p |- foo == p

This somewhat goes against the claim that MM only has universal quantifications over its metavariables. It also plays havoc with translation to dependent type theories, where we would like to interpret the == as definitional equality, because you can't assume a definitional equality as a hypothesis. And finally it complicates the proof theory since you have to be able to discharge hypotheses like |- foo == p here, and not use them out of scope.

Given all these considerations, I think the most reasonable course of action is to just drop this whole corner of the language. It is slightly necessary for metamath definitions which is why I added it in the first place, but there are only a handful of occurrences of the technique - wtru is the primary (only?) example, and it's not worth inheriting metamath weirdness for the sake of one example. Most logicians will tell you that T. is not a definition, it is a primitive term constructor (or equivalently F. is primitive), and there is an easy argument that given only implication and negation there is no way to show that there are any ground wffs at all, so being able to produce one seems suspicious.

So what is the consequence for the language? Let's drop the "free" sort modifier, and make it be always true. That is, definitions can't just drop variables like this. That means that wtru is no longer a valid definition. The MM -> MM0 translation is not affected because I haven't implemented definitions yet, but the fallback was always just to leave it as an axiom. (Getting all the things marked as "definitions" in MM to actually be definitions is a really really hard problem, requiring lots of heuristics and decision procedures, plus many $j annotations to do the proofs.) Dummy variables are treated as bound variables, so they cannot have strict type. I'll remove that example from set.mm0.

Mario

[Giovanni Mascellani]

Hi Mario,

Il 05/05/19 11:17, Mario Carneiro ha scritto:

> Given all these considerations, I think the most reasonable course of
> action is to just drop this whole corner of the language. It is slightly
> necessary for metamath definitions which is why I added it in the first
> place, but there are only a handful of occurrences of the technique -
> wtru is the primary (only?) example, and it's not worth inheriting
> metamath weirdness for the sake of one example. Most logicians will tell
> you that T. is not a definition, it is a primitive term constructor (or
> equivalently F. is primitive), and there is an easy argument that given
> only implication and negation there is no way to show that there are any
> ground wffs at all, so being able to produce one seems suspicious.

That's unfortunate (and I am curious about this easy argument that you
mention: do you have a reference for it, or can you repeat it on the
mailing list?), but it's true that dummy variables are probably mostly
used for set variables.

> So what is the consequence for the language? Let's drop the "free" sort
> modifier, and make it be always true. That is, definitions can't just
> drop variables like this. That means that wtru is no longer a valid
> definition. The MM -> MM0 translation is not affected because I haven't
> implemented definitions yet, but the fallback was always just to leave
> it as an axiom. (Getting all the things marked as "definitions" in MM to
> actually be definitions is a really really hard problem, requiring lots
> of heuristics and decision procedures, plus many $j annotations to do
> the proofs.) Dummy variables are treated as bound variables, so they
> cannot have strict type. I'll remove that example from set.mm0.

I see that in the specs you opted for a lighter version of this change,
retaining the "strict" specifier[1] and mandating that a dummy cannot be
strict (instead of dropping "strict" and dummies altogether). Is this
definitive?

[1]
https://github.com/digama0/mm0/commit/33684468bfe20541896fd4ab314659f0fa09f6c7

[Mario Carneiro]

On Mon, May 6, 2019 at 4:56 AM Giovanni Mascellani <g.masc...@gmail.com> wrote:

Hi Mario,

Il 05/05/19 11:17, Mario Carneiro ha scritto:
> Given all these considerations, I think the most reasonable course of
> action is to just drop this whole corner of the language. It is slightly
> necessary for metamath definitions which is why I added it in the first
> place, but there are only a handful of occurrences of the technique -
> wtru is the primary (only?) example, and it's not worth inheriting
> metamath weirdness for the sake of one example. Most logicians will tell
> you that T. is not a definition, it is a primitive term constructor (or
> equivalently F. is primitive), and there is an easy argument that given
> only implication and negation there is no way to show that there are any
> ground wffs at all, so being able to produce one seems suspicious.

That's unfortunate (and I am curious about this easy argument that you
mention: do you have a reference for it, or can you repeat it on the
mailing list?), but it's true that dummy variables are probably mostly
used for set variables.

The argument is simple: If a set A has a unary operation A -> A and a binary operation A -> A -> A, then it doesn't follow that A is nonempty, because the empty set satisfies these conditions. In other words, if I define the set of wffs like so:

    The collection of wffs is minimal such that:

    * If ph is a wff then -. ph is a wff

    * If ph and ps are wffs then ( ph /\ ps ) is a wff

then it follows that the collection of all wffs is empty, i.e. there are no wffs at all, because the empty set satisfies the conditions and is obviously the smallest such set. One might argue that I am missing a clause for propositional variables, but this is the crux of the matter: The claim still holds regarding *ground* wffs, i.e. wffs with no variables. The wff "T." is a ground wff, yet we have no tools from which to build a ground wff like this, so this is a proper extension of the language - it's not a "definition" at all.

Norm's decision to call df-tru a definition does not originate with him, of course - there are logicians who make such a definition. The usual way this is done is that we have a set of wffs, with a countable set of propositional variables, and we define T. to be either (1) p0 <-> p0, or (2) p <-> p for an arbitrary propositional variable p, and then show that the result doesn't depend on the choice.

Approach (2) is misleading, because it suggests that we can define a term by showing it is invariant under provable equivalence. But we have a syntactic class here, we aren't talking about quotients by provable propositions yet. We just want to set up a language of wffs, in which things like ( p /\ p ) and p are distinct because they are textually different. With this fine-grained notion of equality, it's clear that option (2) doesn't work at all - p0 <-> p0 and p1 <-> p1 are different strings of symbols - which one is T. supposed to abbreviate?

Option (1) works, but it relies on the ability to make explicit reference to p0, which is exactly what we can't do in MM or MM0, where everything is a scheme and parametricity over alpha equivalence is forced - nothing is allowed to break the symmetry of variable names.

Metamath's approach is most similar to option (2). Invariance is proven in trujust, but metamath doesn't provide a way to use this fact, so we then just introduce df-tru as an axiom, from which trujust can be proven.

 

> So what is the consequence for the language? Let's drop the "free" sort
> modifier, and make it be always true. That is, definitions can't just
> drop variables like this. That means that wtru is no longer a valid
> definition. The MM -> MM0 translation is not affected because I haven't
> implemented definitions yet, but the fallback was always just to leave
> it as an axiom. (Getting all the things marked as "definitions" in MM to
> actually be definitions is a really really hard problem, requiring lots
> of heuristics and decision procedures, plus many $j annotations to do
> the proofs.) Dummy variables are treated as bound variables, so they
> cannot have strict type. I'll remove that example from set.mm0.

I see that in the specs you opted for a lighter version of this change,
retaining the "strict" specifier[1] and mandating that a dummy cannot be
strict (instead of dropping "strict" and dummies altogether). Is this
definitive?

I haven't implemented this change yet, as I was busy with the HOL translation. That commit fixes the bug regarding the dummy strict check, but it doesn't address any changes to the sort modifiers. The HOL translation will fail if it is run on a definition that has "dropped dependencies" caused by the non-free modifier. For example, the following definition is valid using a subset of the set.mm0 header:

strict provable sort wff;
pure sort set;
term weq (a b: set): wff; infixl weq: $=s$ prec 50;

def foo {.x .y: set}: wff = $ x =s y $;

Here "foo" is a wff with no arguments with indeterminate truth value. This is the sort of definition I want to exclude.

To be clear, MM0 is not inconsistent even with this definitional principle, because it enforces alpha renaming when unfolding the definition. But as I mentioned in the previous message, modeling this in HOL is a pain and it's really non-intuitive, which is exactly what I want to avoid in MM0. From an implementation standpoint, any simplification of the language is a win, and I'm pretty sure this is a far less onerous restriction than unbundling.

Speaking of the HOL translation, there is a MM0 -> HOL translation now! I still need to work out the bugs but the bulk work is done. This translates statements and proofs in MM0 into statements and proofs in a custom-built subset of HOL. The language is more complicated than strictly necessary because it's tailored for MM0 proof strength, but it's easy to embed the HOL subset into actual HOL. The idea is to use this HOL subset as the backend for translators to different targets like Twelf, HOL light, Isabelle, OpenTheory, Coq, and Lean. OpenTheory is probably the easiest initial target, because of its very simple machine-readable format. I'm glad that this work is finally starting to come to fruition; it is dear to my heart since it is the converse to my very first paper ( https://arxiv.org/abs/1412.8091 ). I've worked on HOL translation before for the MMT project, but that was restricted to statements only. This is a reimplementation and completion of that project, and I think we will finally be able to actually practically export set.mm into all the provers once this is done.

Here's what the output of the HOL translation on set.mm0 looks like right now (with made-up syntax):

term wi: wff -> wff -> wff

term wn: wff -> wff

axiom ax_1: !(ph: wff) (ps: wff). |- wi ph (wi ps ph)

axiom ax_2: !(ph: wff) (ps: wff) (ch: wff). |- wi (wi ph (wi ps ch)) (wi (wi ph ps) (wi ph ch))

axiom ax_3: !(ph: wff) (ps: wff). |- wi (wi (wn ph) (wn ps)) (wi ps ph)

axiom ax_mp: !(ph: wff) (ps: wff). |- ph => |- wi ph ps => |- ps

theorem a1i (v0: wff) (v1: wff) (v2: |- v0): |- wi v1 v0 :=
  ax_mp v0 (wi v1 v0) v2 (ax_1 v0 v1)

theorem a2i (v0: wff) (v1: wff) (v2: wff) (v3: |- wi v0 (wi v1 v2)): |- wi (wi v0 v1) (wi v0 v2) :=
  ax_mp (wi v0 (wi v1 v2)) (wi (wi v0 v1) (wi v0 v2)) v3 (ax_2 v0 v1 v2)

...

theorem simplim (v0: wff) (v1: wff): |- wi (wn (wi v0 v1)) v0 :=
  con1i v0 (wi v0 v1) (pm2_21 v0 v1)

def wb (v0: wff) (v1: wff) := wn (wi (wi v0 v1) (wn (wi v1 v0)))

theorem bi1 (v0: wff) (v1: wff) (v2: |- v0): |- wi (wb v0 v1) (wi v0 v1) :=
  mp -(ap wi (delta wb v0 v1) rfl) simplim (wi v0 v1) (wn (wi v1 v0))

I should really finish the proof of set.mm0, so that it's not an incomplete example. In the last example, "mp", "-", "ap", "rfl" and "delta" are names for conversion rules, i.e.

mp : |- p = q => |- p => |- q, and

delta wb : !v0 v1. |- (wb v0 v1) = (wn (wi (wi v0 v1) (wn (wi v1 v0)))

Here are some examples of statements using variables, where it gets interesting. Here is the input file, containing the FOL axioms of set.mm and the proof mpg (which, by the way, you can generate automatically using the command:

  stack exec -- mm0-hs from-mm ../../mm/set2.mm -f ax-5,ax-6,ax-7,ax-8,ax-9,ax-10,ax-11,ax-gen,mpg -o out.mm0 out.mmu

out.mm0:

delimiter $ ( ) $;

provable sort wff;

term wn (ph: wff): wff;

term wi (ph ps: wff): wff;

axiom ax_mp (ph ps: wff):
  $ ph $ >
  $ wi ph ps $ >
  $ ps $;

pure sort setvar;

term wal {x: setvar} (ph: wff x): wff;

axiom ax_gen {x: setvar} (ph: wff x):
  $ ph $ >
  $ wal x ph $;

theorem mpg {x: setvar} (ph ps: wff x):
  $ wi (wal x ph) ps $ >
  $ ph $ >
  $ ps $;

axiom ax_5 {x: setvar} (ph: wff):
  $ wi ph (wal x ph) $;

sort class;

term cv (x: setvar): class;

term wceq (A B: class): wff;

axiom ax_6 {x: setvar} (y: setvar x):
  $ wn (wal x (wn (wceq (cv x) (cv y)))) $;

axiom ax_7 (x y z: setvar):
  $ wi (wceq (cv x) (cv y)) (wi (wceq (cv x) (cv z)) (wceq (cv y) (cv z))) $;

term wcel (A1 B1: class): wff;

axiom ax_8 (x y z: setvar):
  $ wi (wceq (cv x) (cv y)) (wi (wcel (cv x) (cv z)) (wcel (cv y) (cv z))) $;

axiom ax_9 (x y z: setvar):
  $ wi (wceq (cv x) (cv y)) (wi (wcel (cv z) (cv x)) (wcel (cv z) (cv y))) $;

axiom ax_10 {x: setvar} (ph: wff x):
  $ wi (wn (wal x ph)) (wal x (wn (wal x ph))) $;

axiom ax_11 {x y: setvar} (ph: wff x y):
  $ wi (wal x (wal y ph)) (wal y (wal x ph)) $;

axiom ax_11_b {x: setvar} (ph: wff x):
  $ wi (wal x (wal x ph)) (wal x (wal x ph)) $;

and the result is:

sort wff

term wn: wff -> wff

term wi: wff -> wff -> wff

axiom ax_mp: !(ph: wff) (ps: wff). |- ph => |- wi ph ps => |- ps

sort setvar

term wal: (setvar -> wff) -> wff

axiom ax_gen: !(ph: setvar -> wff). (!(x: setvar). |- ph x) => |- wal (\(x: setvar). ph x)

theorem mpg (v1: setvar -> wff) (v2: setvar -> wff) (v3: !(v0: setvar). |- wi (wal (\(v0: setvar). v1 v0)) (v2 v0)) (v4: !(v0: setvar). |- v1 v0) (v0: setvar): |- v2 v0 :=
ax_mp (wal (\(v0: setvar). v1 v0)) (v2 v0) (ax_gen (\(v0: setvar). v1 v0) (\(v0: setvar). v4 v0)) (v3 v0)

axiom ax_5: !(ph: wff). |- wi ph (wal (\(x: setvar). ph))

sort class

term cv: setvar -> class

term wceq: class -> class -> wff

axiom ax_6: !(y: setvar -> setvar). |- wn (wal (\(x: setvar). wn (wceq (cv x) (cv (y x)))))

axiom ax_7: !(x: setvar) (y: setvar) (z: setvar). |- wi (wceq (cv x) (cv y)) (wi (wceq (cv x) (cv z)) (wceq (cv y)(cv z)))

term wcel: class -> class -> wff

axiom ax_8: !(x: setvar) (y: setvar) (z: setvar). |- wi (wceq (cv x) (cv y)) (wi (wcel (cv x) (cv z)) (wcel (cv y)(cv z)))

axiom ax_9: !(x: setvar) (y: setvar) (z: setvar). |- wi (wceq (cv x) (cv y)) (wi (wcel (cv z) (cv x)) (wcel (cv z)(cv y)))

axiom ax_10: !(ph: setvar -> wff). |- wi (wn (wal (\(x: setvar). ph x))) (wal (\(x: setvar). wn (wal (\(x: setvar). ph x))))

axiom ax_11: !(ph: setvar -> setvar -> wff). !(y: setvar). |- wi (wal (\(x: setvar). wal (\(x: setvar). ph x y))) (wal (\(x: setvar). wal (\(x: setvar). ph x y)))

axiom ax_11_b: !(ph: setvar -> wff). |- wi (wal (\(x: setvar). wal (\(x: setvar). ph x))) (wal (\(x: setvar). wal (\(x: setvar). ph x)))

The backslash is a lambda abstraction. Notice how variables are abstracted in the arguments of theorems like ax_gen. Sorry about the variable names; currently the proof format replaces everything with numbers so the string names have to be reconstructed on output. While I think using numbers is good for speed, the string names should probably be tucked away somewhere so that the user can still read the resulting theorem.

Mario

[Mario Carneiro]

On Mon, May 6, 2019 at 4:56 AM Giovanni Mascellani <g.masc...@gmail.com> wrote:

I see that in the specs you opted for a lighter version of this change,
retaining the "strict" specifier[1] and mandating that a dummy cannot be
strict (instead of dropping "strict" and dummies altogether). Is this
definitive?

 

Oops, I should read what you say more carefully. Dummies aren't being removed from the language. What is being removed is the exception for non-free sorts, i.e, in the spec:

    We require for a definition, that every free variable in the definiens with a  `free` sort is among the declared dependencies of the definition (i.e. the return type is `wff x` if `x` is free in the definiens and the sort of `x` is declared as `free`).

The words "with a free sort" would be removed, so the dependency check is always required. An example of a valid definition using dummy variables is df-eu:

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

The spec basically mandates a proper not-free check on the definition value to make sure that y is bound in a quantifier for the definition to be acceptable. This was already the case if you mark the sort as free, but now it will always be the case.

Mario

[Norman Megill]

On Monday, May 6, 2019 at 7:41:29 AM UTC-4, Mario Carneiro wrote:
...

Norm's decision to call df-tru a definition does not originate with him, of course - there are logicians who make such a definition. The usual way this is done is that we have a set of wffs, with a countable set of propositional variables, and we define T. to be either (1) p0 <-> p0, or (2) p <-> p for an arbitrary propositional variable p, and then show that the result doesn't depend on the choice.

df-tru was added quite late in the set.mm development, by Anthony Hart in 2010.  Initially I didn't plan to move it out of his mathbox, but FL started to use it in theorems that were moved to the main set.mm, so I moved up df-tru (with mixed feelings) in 2011 to accommodate that.  Since then, a number of "truth table" type tutorial theorems and descriptions have been added for T. and F., many by DAW, but few of these are used for later practical work.

Early on there were objections to df-tru because it has a "free" wff variable on one side that isn't on the other.  Andrew Salmon felt that A. x x = x would be a better definition, but that would have required that df-tru be moved to the predicate calculus section.

I have no fundamental objection to defining T. as A. x x = x and moving it to pred calc.  It shouldn't be too hard because df-tru isn't heavily used in prop calc, where there are 30 proofs referencing ~ wtru, all but one about properties of T.  So moving them to pred calc wouldn't be a big deal.  There are another 361 uses of wtru beyond prop calc, and from a quick check it seems they are mainly used to convert deductions into inferences.  There are 115 proofs referencing wfal, mostly in studies of prop calc axiomatizations along with some theorems about F. itself.  Tthere are 39 theorems that contain T. or F. or both, all in prop calc and none after prop calc (excluding mathboxes).

One of my initial objections to df-tru was that I felt it to be unnecessary for ordinary math.  It is rare to see T. in ordinary math outside of the beginnings of logic to demonstrate truth tables.  Even there I think it is typically used as a semantic constant to model propositional logic more than as a defined constant in the language itself.  (I may be wrong on that.)

The constant F. is used as a primitive in some propositional calculus axiomatizations, and for classical logic at least,  I think -. phi is typically defined as (phi -> F.) early on and the F. abandoned for practical development.

Norm

[Norman Megill]

On Monday, May 6, 2019 at 3:00:21 PM UTC-4, Norman Megill wrote:

The constant F. is used as a primitive in some propositional calculus axiomatizations, and for classical logic at least,  I think -. phi is typically defined as (phi -> F.) early on and the F. abandoned for practical development.

That might not be completely correct.  I think F. might be common in formal proofs by resolution which show that negating an assumption leads to F., thus proving the assumption.

Norm

[Benoit]

Digression regarding "T.":

I think Mario described the situation clearly.  This is one of the reasons why I had proposed last year (attachment to https://groups.google.com/d/msg/metamath/mYchAks747s/TDntf_0CAAAJ) to introduce T. via the axiom

  ax-tru $a |- T. $.

I think that defining T. to be some wff which we know is true (like ( ph -> ph ) or ( ph -> ( ps -> ph ) ) or A. x x = x) and then prove from that definition " |- T. " is simply going the other way around: simply postulate it.

(Granted, that's not very important, but I think it is conceptually cleaner.)

Benoît

[David A. Wheeler]

On Mon, 6 May 2019 12:00:21 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> Early on there were objections to df-tru because it has a "free" wff
> variable on one side that isn't on the other. Andrew Salmon felt that A. x
> x = x would be a better definition, but that would have required that
> df-tru be moved to the predicate calculus section.
>
> I have no fundamental objection to defining T. as A. x x = x and moving it

> to pred calc. ...

That's rather unfortunate, because T. and F. really belong
in the propositional calculus section, not in the later predicate calculation section.
Is there no alternative for keeping T. and F. within propositional calculus?

Perhaps an alternative is to simply state it axiomatically, something like this:
df-tru $a |- T. $.

I imagine there are ramifications to this that I haven't considered. Thoughts?
Can those ramifications be addressed?

--- David A. Wheeler

[Norman Megill]

On Monday, May 6, 2019 at 3:22:42 PM UTC-4, David A. Wheeler wrote:

On Mon, 6 May 2019 12:00:21 -0700 (PDT), Norman Megill wrote:
> Early on there were objections to df-tru because it has a "free" wff
> variable on one side that isn't on the other.  Andrew Salmon felt that A. x
> x = x would be a better definition, but that would have required that
> df-tru be moved to the predicate calculus section.
>
> I have no fundamental objection to defining T. as A. x x = x and moving it
> to pred calc.  ...

That's rather unfortunate, because T. and F. really belong
in the propositional calculus section, not in the later predicate calculation section.
Is there no alternative for keeping T. and F. within propositional calculus?

Perhaps an alternative is to simply state it axiomatically, something like this:
  df-tru $a |- T. $.

This doesn't qualify as a definition but would be an axiom.  The problem with adding it as an axiom is that it implies that ax-1,2,3 is not a complete axiomatization for prop calc because it can't prove this df-tru.  Or that df-tru is an extralogical notion beyond the reach of prop calc.

Another possibility is T. <-> A. x ( x = x <-> x = x ).  Then we would only need ax-gen to prove trutru (the only theorem we need from any df-tru).  Since ax-gen is the very first axiom in pred calc, this df-tru can be added as the very first section in pred calc, immediately after prop calc.  Even though we are using pred calc (very mildly), we aren't introducing any new axioms.

Norm
 

[Norman Megill]

Or even better?   T <-> ( A. x x = x <-> A. x x = x )
This way we need only introduce the syntax for A. and = , and we don't need any pred calc axioms to prove trutru.

In a sense this isn't even outside of prop calc, since the intended object language expressions the wff variables range over already involve v0 v1... and -> -. A. = e. only (no wff variables), even in prop calc.

Norm

[David A. Wheeler]

On Mon, 6 May 2019 13:59:29 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> Or even better? T <-> ( A. x x = x <-> A. x x = x )
> This way we need only introduce the syntax for A. and = , and we don't need
> any pred calc axioms to prove trutru.
>
> In a sense this isn't even outside of prop calc, since the intended object
> language expressions the wff variables range over already involve v0 v1...
> and -> -. A. = e. only (no wff variables), even in prop calc.

That's an interesting alternative.

There are negatives to it. That means we'll have to introduce the
syntax for A. , =, setvar, and x into the prop calc section
(before they are *really* needed). That's really unfortunate. Also, this:
|- T.
is clearly simpler than:
|- T. <-> ( A. x x = x <-> A. x x = x )

I'm fine with claiming that this is a "definition" of true:
|- T.
even though it doesn't fit our current definition of a definition.
You can change the definition of "definition" to make an exception for this case,
and it's harder for something to be simpler than ` |- T. ` .

That said, using A. is clearly a viable alternative.

--- David A. Wheeler

[Benoit]

  |- T. <-> ( A. x x = x <-> A. x x = x )

I think this should really be avoided. The current definition is better.  Apparently, my message from earlier didn't get through, so I copy it here, hoping this message does:

------------------------

------------------------

Benoit

[Mario Carneiro]

On Mon, May 6, 2019 at 3:38 PM Norman Megill <n...@alum.mit.edu> wrote:

On Monday, May 6, 2019 at 3:22:42 PM UTC-4, David A. Wheeler wrote:

On Mon, 6 May 2019 12:00:21 -0700 (PDT), Norman Megill wrote:
> Early on there were objections to df-tru because it has a "free" wff
> variable on one side that isn't on the other.  Andrew Salmon felt that A. x
> x = x would be a better definition, but that would have required that
> df-tru be moved to the predicate calculus section.
>
> I have no fundamental objection to defining T. as A. x x = x and moving it
> to pred calc.  ...

That's rather unfortunate, because T. and F. really belong
in the propositional calculus section, not in the later predicate calculation section.
Is there no alternative for keeping T. and F. within propositional calculus?

Perhaps an alternative is to simply state it axiomatically, something like this:
  df-tru $a |- T. $.

This doesn't qualify as a definition but would be an axiom.  The problem with adding it as an axiom is that it implies that ax-1,2,3 is not a complete axiomatization for prop calc because it can't prove this df-tru.  Or that df-tru is an extralogical notion beyond the reach of prop calc.

I think we should get beyond thinking that just because an axiom uses <-> means it's a definition. I think this new df-tru is no worse than the current df-tru as a definition. We have a simple check for conservativity of most set.mm definitions, but df-tru already doesn't qualify. This axiom is a conservative extension (whether it is stated like df-tru or tru), so in the broad sense it is still a definition, but neither one strictly follows the rules of definition construction. The set.mm convention is to name things df-* when they are a conservative extension, i.e. there is *some* way to justify they are conservative, even if they fail the syntactic check, so I'm comfortable with adopting Benoit's and David's suggestion.

We're already doing this with df-bi, by the way. Presumably you wouldn't argue the same thing about people worrying that <-> is an extralogical notion, yet it involves a new axiom different from ax-1,2,3.

As long as the new axiom is still labeled df-tru, there won't be any adverse affects - it will still be considered a definition by metamath.exe so it will be classed as such in the HTML webpages. The only downside is that mmj2 will need to have an exception added for df-tru. You might wonder why it's accepting it now, and that's because it's picking up on the justification theorem. But as I've tried to explain, the metatheory of the justification theorem approach leads to existential metavariables which, while possible, increases the logical strength of the metamath core in ways that we haven't really considered properly.

While we are on the subject of mind bending definitions, here's another one that works without moving to pred calc:

|- T. <-> ( T. -> T. )

I want to emphasize that if you think this is not a definition because it uses some trickery, you're right - now look at all the other definitions and notice similar trickery.

Another possibility is T. <-> A. x ( x = x <-> x = x ).  Then we would only need ax-gen to prove trutru (the only theorem we need from any df-tru).  Since ax-gen is the very first axiom in pred calc, this df-tru can be added as the very first section in pred calc, immediately after prop calc.  Even though we are using pred calc (very mildly), we aren't introducing any new axioms.

I disagree with moving it to pred calc. "T." is logically a part of prop calc, and this incurs a dependence of wtru on wceq and setvar and class(!). This will make the levels even more muddled than they are currently. I agree with Benoit that having any other expression for T. being privileged as the definition seems backwards.

Mario

[David A. Wheeler]

As I noted earlier, I like this definition of constant true:

df-tru $a |- T. $.

The intuition "true is true" makes a lot of sense to me :-).
It means that our propositional calc and predicate calculus
will have a much cleaner separation (vs. doing otherwise).
It eases moving information in & out of Metamath without
limiting the power of set.mm and it's certainly easy for us to do.
I also agree with Mario in that it's a conservative extension and thus
should be considered a definition, not an axiom (even though
it looks different from most definitions).

If we change to this (and I think we should), we should document
some of this discussion. Below is my first attempt at it,
based on text shamelessly cribbed from the mailing list discussion
so far. It's no doubt wrong, so corrections to what it SHOULD say
would be welcome :-).

--- David A. Wheeler

=====================================

$( Definition of the constant true value ` T. ` .
We simply declare that constant true value ` T. ` is true, which
is a very unusual way of defining a term.

An older definition of ` T. ` used
` ( T. <-> ( ph <-> ph ) ) ` , where the
definition ~ biid is used as an antecedent, though any true wff
(such as an axiom) could be used in its place.
This looks more like a normal definition (since it uses ` <-> ` ),
and this construct does work in Metamath.
However, while this older definition is similar to some
common ways of defining ` T. ` , there are subtle distinctions.
A common way in other systems to define
` T. ` is to have a set of wffs, with a countable
set of propositional variables, and define ` T. ` to be either (1)

p0 ` <-> ` p0, or (2) p ` <-> ` p for an arbitrary propositional variable
p, and then show that the result doesn't depend on the choice.

Approach (1) works, but it relies on the ability to make explicit
reference to p0. This is exactly what we can't do in Metamath (or
similar systems like Metamath Zero) where everything is a scheme

and parametricity over alpha equivalence is forced - nothing is

allowed to break the symmetry of variable names. Approach (2)

is misleading, because it suggests that we can define a term by
showing it is invariant under provable equivalence. But we have a
syntactic class here, we aren't talking about quotients by provable
propositions yet. We just want to set up a language of wffs, in
which things like ( p ` /\ ` p ) and p are distinct because they
are textually different. With this fine-grained notion of equality,
it's clear that option (2) doesn't work at all - p0 ` <-> ` p0 and p1
` <-> ` p1 are different strings of symbols - which one is ` T. `

supposed to abbreviate? Metamath's older approach is most similar
to approach (2). Invariance is proven in ~ trujust , but Metamath

doesn't provide a way to use this fact, so we then just introduced

~ df-tru as an axiom, from which ~ trujust can be proven.
Declaring it as an axiom works, but leads to a related problem.
This older definition is difficult to translate to many
other systems. Definitions are easier to exchange with other
systems if we require in a definition that every free variable in
the definiens is among the declared dependencies of the definition
(i.e. the return type is something like "wff x" if "x" is free in

the definiens and the sort of "x" is declared as "free").

We want to ease such exchanges, not make them difficult, when that
is not difficult to do. This older definition of ` T. ` was the
one major exception that made translation difficult.

An alternative definition would be
` T. <-> A. x ( x = x <-> x = x ) ` or similar.
This would bind the variables, eliminating the earlier concerns.
However, that would either (1) delay introduction
of constant true until predicate calculus (where it doesn't belong)
or (2) require moving many predicate calculus syntax definitions
(such as ` A. ` ) into the propositional calculus section
(where they don't belong).

In addition, while the older definition and its alternative
let us prove that ` T. ` is true,
in some philosophical sense that is backwards.
In some broad senses the constant true ( ` T. ` ) is true, and
we should then be able to prove other properties that, instead of
trying to prove that true is true given other statements.

Definitions are conservative extensions of axioms.
Most definitions use ` <-> ` or ` = ` , and follow other syntax rules
to ensure that they are conservative.
This definition of ` T. ` does not use ` <-> ` or ` = ` , but nevertheless
it is a conservative extension, so it is still a definition.
We also do something similar with ~ df-bi .

The definition given here is breathtaking short and obviously correct
("true is true"). It allows the definition of constant true
to be in propositional calculus (where it belongs) *without* requiring
that predicate calculus definitions be moved into the propositional
calculus section (where they don't belong).
It also eliminates some potential problems when translating our work
between other systems.
(Contributed by David A. Wheeler and Benoit Jubin, 6-May-2018.) $)

[Giovanni Mascellani]

Hi,

Il 07/05/19 01:48, Mario Carneiro ha scritto:

> While we are on the subject of mind bending definitions, here's another
> one that works without moving to pred calc:
>
> |- T. <-> ( T. -> T. )
>
> I want to emphasize that if you think this is not a definition because
> it uses some trickery, you're right - now look at all the other
> definitions and notice similar trickery.

I am very newbie with logic, so please correct me if I am saying
something stupid. I would like to propose another alternative:

$c ph_ T. $.
$a wff ph_ $.
$a |- ( T. <-> ( ph_ -> ph_ ) ) $.

No other axiom is given for ph_, so we will never know if that wff is
true or false and therefore plausibly no other theorem or axiom will
ever use it. At the same time it does not introduce variables on which
T. would depend, it does not require predicate logic and it should be ok
with mmj2 verification, since the definiens does not contain the
definiendum.

To me (again, not a logician) it does not look like too mind bending: we
are simply saying that there is a wff that is "more equal than the
others" and we called it ph_, although we are not saying which one it is
(so we can only derive from it the conclusions that do not actually
depend on what is ph_, like the definition of T.).

What do you think about it?

[Mario Carneiro]

There's nothing wrong with this implementation; indeed it's probably a better example than mine that the actual import of T. is the existence of a constant wff, and it doesn't matter what it is. That said, this is an axiom:

$a wff ph_ $.

Although we don't usually think of term formers as axioms, they can increase the strength of the system (for example, constants of "setvar" type increase the strength to the point of inconsistency). This is another way to understand what I was getting at with the modifiers "nonempty" and "free", which are explicitly referencing the existence of some value in the type from which other things, like T., can be defined.

From a practical standpoint, I don't think it is good to have uninterpreted terms hanging around, as although this is a conservative extension, it's not a definitional extension - you can't prove within the system itself that every expression in the extended language is equivalent to one in the original language. It's much harder to justify these things intuitively, and I think it clouds the issue when we just want to say "look, it's just True. You know what true is! Stop asking questions". The best thing is when there's only a few axioms, they are all plainly self evident, and only reference things that the reader is already familiar with and accords with their intuition. The trick is to achieve this while also having a solid logical foundation for people like me that aren't satisfied with less than a complete interpretation with a formalization that matches our intuitive descriptions.

By the way, I want to draw another parallel here, to category theory, where the |- T. kind of "definition" is actually pretty common. For example, we say that an object T. is terminal when there is a unique morphism ph -> T. for every object ph in the category. A terminal object, if it exists, is unique up to isomorphism; so now if I say that category C has a terminal object I will use T. with impunity without committing to any particular choice of a terminal object. (Usually they use 1 instead but this makes the parallel more obvious.) Similarly, like with a product in a category, we might "define AND" using the axioms

|- ( ph /\ ps ) -> ph

|- ( ph /\ ps ) -> ps

|- ph -> ( ps -> ( ph /\ ps ) )

where no <-> is used, yet the expression ( ph /\ ps ) is now completely determined up to logical equivalence. The fact that these objects are unique doesn't imply that they exist, though, so one has to be careful. For example these are some of the axioms from iset.mm, but if you remove them you don't get full intuitionistic logic, because you can't build /\ from the other connectives. In this case, T. is unique if it exists, and in fact if anything exists then T. exists, but the axioms don't allow you to show that anything exists until you get to pred calc or set theory when random constants like _V start showing up, and then you can say "aha, I will define T. <-> _V = _V" and the definition will work with no problems. (Even justifying a definition like T. <-> A. x x = x requires you to know that dropping set variables is okay when they are bound, which requires a proper analysis of binding variables that made its way into the core of MM0.)

--
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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/36864373-ee31-30c5-ff9c-e66c0d27f677%40gmail.com.

[Norman Megill]

On Monday, May 6, 2019 at 7:02:37 PM UTC-4, Benoit wrote:

  |- T. <-> ( A. x x = x <-> A. x x = x )

I think this should really be avoided. The current definition is better.  Apparently, my message from earlier didn't get through, so I copy it here, hoping this message does:

------------------------

Digression regarding "T.":

I think Mario described the situation clearly.  This is one of the reasons why I had proposed last year (attachment to https://groups.google.com/d/msg/metamath/mYchAks747s/TDntf_0CAAAJ) to introduce T. via the axiom

  ax-tru $a |- T. $.

Adding a new axiom for propositional calculus is an ugly solution.  The current ax-1,2,3,mp is a standard axiomatization, and it has a completeness theorem, meaning it is supposed to be sufficient to prove any propositional calculus theorem.  Gratuitously adding a non-standard axiom, just because it may be somewhat inconvenient to state as a definition, seems contrary to the philosophy of set.mm.  It would be rather weird to display it as the 4th prop calc axiom on the MPE home page, with the explanation "it was inconvenient to define it properly, so we added it as an axiom".

Norm

 

[Benoit]

Norm: I just saw your message while writing the paragraph below.  I agree not to add it as "ax-tru", but maybe the exact same statement as "df-tru" is ok?

David: I think all of this should be documented, as you proposed, but I think this is too long to be included in set.mm.  I propose, if Norm agrees to the change of definition, to take your first paragraph and add a link to a specific page (e.g. mpeuni/mmdftru.html, similar to mpeuni/mmnatded.html) where we can put the rest of your description, with possibly more detail, together with the alternate candidates given since by Giovanni ( _ph = _ph ) and Mario ( _V = _V ).  (Ironically, I had proposed on this group to define _V as { x | T. } ! --- and even stranger, this is less circular than it might appear at first, since whatever the value of _V, it is always equal to itself; this is the fact that Giovanni used for this definition)

Reworking a bit your first paragraph (most notably, using the word "provable" and adding the important keyword "conservative", which can be explained in mmdftru.html), this would give:

  $( Definition of the truth value "true", denoted by ` T. ` .  This definition
     simply declares that ` T. ` is provable.  It does not have the standard
     form of a definition (namely, ` |- ( T. <-> ... ) ` ) but it is
     conservative, so it is a legitimate definition.  The statement ~ dftru ,
     which has the standard form of a definition, used to be the definition of
     ` T. ` , but this choice has other drawbacks (although in practice, both
     are fine).  For a discussion of advantages and drawbacks of these and
     other choices, see ~ mmdftru.html .  (Contributed by David A. Wheeler and
     BJ, 6-May-2018.) $)

  df-tru $a |- T. $.

...

  $( An equivalence which used to be the definition of ` T. ` .  Note that
     ~ df-tru can be proved from this by using ~ biid and ~ mpbir .
     (Contributed by Anthony Hart, 13-Oct-2010.)  (Revised by David A. Wheeler
     and BJ, 6-May-2018.) $)
  dftru $p |- ( T. <-> ( ph <-> ph ) ) $= ? $.
## prove it from 2th, biid, df-tru

As for the credits, I think they would go more legitimately to "MC and DAW" than DAW and me.  What is certain, is that the explanations to be written in mmdftru.html, using David's draft, should be credited to these two (of course mentionning Giovanni for his candidate).  By the way: note my preference for using initials in set.mm (I think full names clutter the mmtheoremsXX.html pages, especially when there are revisions and proof shortenings).  The key to map initials to full names is already present at the beginning of set.mm.  Of course this in only my personal preference.

Benoit

[Norman Megill]

On Monday, May 6, 2019 at 7:49:12 PM UTC-4, Mario Carneiro wrote:

On Mon, May 6, 2019 at 3:38 PM Norman Megill wrote:

On Monday, May 6, 2019 at 3:22:42 PM UTC-4, David A. Wheeler wrote:

On Mon, 6 May 2019 12:00:21 -0700 (PDT), Norman Megill wrote:
> Early on there were objections to df-tru because it has a "free" wff
> variable on one side that isn't on the other.  Andrew Salmon felt that A. x
> x = x would be a better definition, but that would have required that
> df-tru be moved to the predicate calculus section.
>
> I have no fundamental objection to defining T. as A. x x = x and moving it
> to pred calc.  ...

That's rather unfortunate, because T. and F. really belong
in the propositional calculus section, not in the later predicate calculation section.
Is there no alternative for keeping T. and F. within propositional calculus?

Perhaps an alternative is to simply state it axiomatically, something like this:
  df-tru $a |- T. $.

This doesn't qualify as a definition but would be an axiom.  The problem with adding it as an axiom is that it implies that ax-1,2,3 is not a complete axiomatization for prop calc because it can't prove this df-tru.  Or that df-tru is an extralogical notion beyond the reach of prop calc.

I think we should get beyond thinking that just because an axiom uses <-> means it's a definition. I think this new df-tru is no worse than the current df-tru as a definition. We have a simple check for conservativity of most set.mm definitions, but df-tru already doesn't qualify. This axiom is a conservative extension (whether it is stated like df-tru or tru), so in the broad sense it is still a definition, but neither one strictly follows the rules of definition construction. The set.mm convention is to name things df-* when they are a conservative extension, i.e. there is *some* way to justify they are conservative, even if they fail the syntactic check, so I'm comfortable with adopting Benoit's and David's suggestion.

We're already doing this with df-bi, by the way. Presumably you wouldn't argue the same thing about people worrying that <-> is an extralogical notion, yet it involves a new axiom different from ax-1,2,3.

As long as the new axiom is still labeled df-tru, there won't be any adverse affects - it will still be considered a definition by metamath.exe so it will be classed as such in the HTML webpages. The only downside is that mmj2 will need to have an exception added for df-tru. You might wonder why it's accepting it now, and that's because it's picking up on the justification theorem. But as I've tried to explain, the metatheory of the justification theorem approach leads to existential metavariables which, while possible, increases the logical strength of the metamath core in ways that we haven't really considered properly.

Yes, I was wondering about mmj2 and df-tru.  Is df-tru the only one (not counting the 4 in the exception list, df-bi, df-clel, df-cleq, df-clab) that requires a separate set.mm justification theorem?

T. <-> ( A. x x = x <-> A. x x = x ) would not have that problem since no second-order metatheory would be needed for its justification.  Also, wouldn't this provide a cleaner interface with the mm0 translator (which is what brought this up in the first place)?  Maybe we should recognize that prop calc simply isn't well suited for definitions involving dummy variables (because of the 2nd order justification required).  I don't see anything wrong theoretically with defining it using pred calc syntax; it mainly seems an aesthetic issue.

The 4 exceptions for the mmj2 checker are very important definitions crucial for practical development of set.mm, and we go out of our way to provide extensive verbal explanations and justifications.  But df-tru is not that important in the big picture.  Except for 56 theorems about T. and F., set.mm would barely be affected if we got rid of df-tru completely.  To me doesn't seem worth making it a 5th exception or having special logic in the checking algorithm specifically for it, especially since (unlike the other 4) there _is_ a way to avoid putting in the exception list.

 

While we are on the subject of mind bending definitions, here's another one that works without moving to pred calc:

|- T. <-> ( T. -> T. )

I want to emphasize that if you think this is not a definition because it uses some trickery, you're right - now look at all the other definitions and notice similar trickery.

I'm not sure what trickery you mean.  mmj2 rejects this because the defined symbol appears in the definiens.

I'm excluding df-bi,df-clab,df-cleq,df-clel if that's what you mean.  We tolerate those 4 special cases because they are essential to the development and can't be replaced by the usual kind of definition.  In a couple of places we even tell the reader to treat them as new axioms if they are uncomfortable with their informal justification arguments.  I don't want this list to grow, especially for something as inconsequential as T. .

 

Another possibility is T. <-> A. x ( x = x <-> x = x ).  Then we would only need ax-gen to prove trutru (the only theorem we need from any df-tru).  Since ax-gen is the very first axiom in pred calc, this df-tru can be added as the very first section in pred calc, immediately after prop calc.  Even though we are using pred calc (very mildly), we aren't introducing any new axioms.

I disagree with moving it to pred calc. "T." is logically a part of prop calc, and this incurs a dependence of wtru on wceq and setvar and class(!). This will make the levels even more muddled than they are currently.

It is not really "moving it to pred calc" because no pred calc axioms are involved (for the T. <-> ( A. x x = x <-> A. x x = x ) variant).  We are just moving up some syntax definitions in order to make its justification first order instead of second order, so it can be checked with the same algorithm used to check pred calc definitions.  Most people wouldn't even notice the change outside of the definition itself, which we can explain in its description.  It's similar to how we moved up the set theory wceq, wcel into pred calc.  It affects only one definition and one proof, and if we decide it was a mistake it is easily reverted.

We could place the 56 theorems with T. and F. at the end of prop calc so that they are the only ones in the scope of the pred calc syntax.

This isn't new.  As I mentioned, in 2011 some people were uncomfortable with df-tru, and T. <-> A. x x = x was proposed as being much more in keeping with other definitions in set.mm that require dummy variables, so that the requirements for a sound definition are kept uniform and as simple as possible.

Since the reaction to this has been so negative here, though, I think we'll leave df-tru alone for now.

Norm
 

[Norman Megill]

On Monday, May 6, 2019 at 9:54:34 PM UTC-4, David A. Wheeler wrote:

As I noted earlier, I like this definition of constant true:

   df-tru $a |- T. $.

This would require adding df-tru to the mmj2 exception list, which I really, really want to avoid.  That list is reserved for a handful of definitions essential to the practical development of set.mm, which df-tru is not.  (Indeed, I put in a great deal of effort just to eliminate df-sbc from the exception list.)  Moreover, unlike the other 4 exceptions, there is a way to avoid putting it in that list.

Norm

[David A. Wheeler]

On Tue, 7 May 2019 05:50:59 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> It is not really "moving it to pred calc" because no pred calc axioms are
> involved (for the T. <-> ( A. x x = x <-> A. x x = x ) variant). We are
> just moving up some syntax definitions in order to make its justification
> first order instead of second order, so it can be checked with the same
> algorithm used to check pred calc definitions. Most people wouldn't even
> notice the change outside of the definition itself, which we can explain in
> its description. It's similar to how we moved up the set theory wceq, wcel
> into pred calc. It affects only one definition and one proof, and if we
> decide it was a mistake it is easily reverted.

> We could place the 56 theorems with T. and F. at the end of prop calc so
> that they are the only ones in the scope of the pred calc syntax.

Fair enough. I still prefer $a |- T. $. , but if the new df-tru were:

T. <-> ( A. x x = x <-> A. x x = x )

and the T. / F. stuff was at the end of the prop calc section,
then I think the concerns go down (since the scope of "mixture" is smaller).
I could live with that.

I think you're right that most people wouldn't notice as long as the
predicate calculus *axioms* weren't moved into the propositional calculus section.
You're also right that it's similar to wceq and wcel. We should explain, when
these syntax definitions are made, that we're introducing them early to make them
accessible for defining ` T. ` . I suspect many would be unsurprised that
there's be some "foreshadowing" of predicate calculus near the end of the
propositional calculus section.

So while this approach wouldn't be my *preference*, I think that'd be an improvement
over the current approach.

In addition: I suggest that if don't use $a |- T. $., then:
* df-tru should be marked as "(New usage is discouraged.)".
* The proof of tru ( ` |- T. ` ) would use df-tru (and be allowed to do so).
* all other theorems should be based (directly or indirectly) on tru, never df-tru.

Here's my rationale: In some sense "( A. x x = x <-> A. x x = x )"
is not really the "meaning" of constant true, it's just a placeholder and could
be replaced with any other true statement. What really matters is that
` T. ` is always true, which is what ~ tru proves.
If we migrate all other theorems to depend on ~ tru ,
then the exact definition of df-tru is mostly irrelevant.
(df-tru could be thought of as a temporary scaffolding.)
I think we should do this even if we kept the existing definition.
It retains most of the benefits of using $a |- T. $. as the definition of
constant true, if we're not going to use that $a statement,
and it means that the rest of the statements are independent
of the exact statement in df-tru.

I plan to start creating changes to make proofs depend on tru instead of df-tru,
unless there's some objection.

--- David A. Wheeler

[Jim Kingdon]

On 5/6/19 12:00 PM, Norman Megill wrote:

> There are another 361 uses of wtru beyond prop calc, and from a quick
> check it seems they are mainly used to convert deductions into inferences.

That's my recollection of how I've seen it used. Examples include
tanord, pige3, and zriotaneg.

Given that deductions are for many purposes the "standard" way of
stating things, this seems like to continue/expand.

I have much less of an opinion about how to define T. - as long as tru
ends up being a theorem, it should work the same way.

[David A. Wheeler]

Mario:

>So what is the consequence for the language? Let's drop the "free" sort
>modifier, and make it be always true. That is, definitions can't just
>drop
>variables like this. That means that wtru is no longer a valid
>definition.

Are there any other examples of this construct in set.mm besides wtru / df-tru ?

--- David A.Wheeler

[Mario Carneiro]

On Tue, May 7, 2019 at 8:51 AM Norman Megill <n...@alum.mit.edu> wrote:

On Monday, May 6, 2019 at 7:49:12 PM UTC-4, Mario Carneiro wrote:

As long as the new axiom is still labeled df-tru, there won't be any adverse affects - it will still be considered a definition by metamath.exe so it will be classed as such in the HTML webpages. The only downside is that mmj2 will need to have an exception added for df-tru. You might wonder why it's accepting it now, and that's because it's picking up on the justification theorem. But as I've tried to explain, the metatheory of the justification theorem approach leads to existential metavariables which, while possible, increases the logical strength of the metamath core in ways that we haven't really considered properly.

Yes, I was wondering about mmj2 and df-tru.  Is df-tru the only one (not counting the 4 in the exception list, df-bi, df-clel, df-cleq, df-clab) that requires a separate set.mm justification theorem?

Yes. Put another way, the reason df-tru is not in the exception list is because there is an entire section of the definition checker devoted to checking df-tru. The only other justification theorems in set.mm are eujust, which is the first definition with a dummy set variable, and vjust, which is the first definition with a dummy variable bound by a class abstraction. I guess these are merely illustrative, because there aren't nearly enough of them to support all of set.mm. MM0 is going to have to prove justification theorems for everything else, using either CondEq (which is theoretically sufficient but practically a bit cumbersome) or some more canonical proof style (which would require more explicit references to theorems and so more $j's). Unless you think it is worthwhile to require justification theorems for all new definitions? I want to avoid any set.mm hardcoded names this time because they tend to be inflexible since they don't move with the times (e.g. changing set -> setvar in mmj2).

 

T. <-> ( A. x x = x <-> A. x x = x ) would not have that problem since no second-order metatheory would be needed for its justification.  Also, wouldn't this provide a cleaner interface with the mm0 translator (which is what brought this up in the first place)?  Maybe we should recognize that prop calc simply isn't well suited for definitions involving dummy variables (because of the 2nd order justification required).  I don't see anything wrong theoretically with defining it using pred calc syntax; it mainly seems an aesthetic issue.

Using a definition based on pred calc would solve all the foundational issues, and of the options discussed thus far it's the only one that actually allows df-tru to be a proper definition supported by both mmj2 and the new MM0 definition checker.

 

The 4 exceptions for the mmj2 checker are very important definitions crucial for practical development of set.mm, and we go out of our way to provide extensive verbal explanations and justifications.  But df-tru is not that important in the big picture.  Except for 56 theorems about T. and F., set.mm would barely be affected if we got rid of df-tru completely.  To me doesn't seem worth making it a 5th exception or having special logic in the checking algorithm specifically for it, especially since (unlike the other 4) there _is_ a way to avoid putting in the exception list.

All of the things marked as df-* are believed to be conservative, and so if we wanted to get them out of the exception list it's just a matter of implementing a check that accomodates them. The problem is that they each have unique, one-off reasons for being conservative, and so the amount of new code added would be enough that you wouldn't get more assurance from the "automatic" result than you already had by hand-analysis of the axiom itself. The only thing that makes df-tru is that there *is* special logic in the mmj2 definition checker that supports df-tru, specifically, and no other definition.

This discussion originated with MM0, but I don't want you to think about this as simply "making translations easier". I'm basically rewriting the mmj2 definition checker here, but I'm doing it with a proper formalized theory this time, rather than just a bunch of ad hoc rules that I think should be enough. In the process of doing so, I identified that justification theorems aren't enough to ensure conservativity. A justification theorem will prove that the definition is unique, but it doesn't prove that the definition exists. You have to give values for the free metavariables to accomplish that, and so df-tru basically asserts "there exists a wff" that wasn't provable before df-tru.

As I see it, this is a subtle bug in the mmj2 definition checker, and if I fix it then mmj2 will no longer accept df-tru as it currently exists.

 

Another possibility is T. <-> A. x ( x = x <-> x = x ).  Then we would only need ax-gen to prove trutru (the only theorem we need from any df-tru).  Since ax-gen is the very first axiom in pred calc, this df-tru can be added as the very first section in pred calc, immediately after prop calc.  Even though we are using pred calc (very mildly), we aren't introducing any new axioms.

I disagree with moving it to pred calc. "T." is logically a part of prop calc, and this incurs a dependence of wtru on wceq and setvar and class(!). This will make the levels even more muddled than they are currently.

It is not really "moving it to pred calc" because no pred calc axioms are involved (for the T. <-> ( A. x x = x <-> A. x x = x ) variant).  We are just moving up some syntax definitions in order to make its justification first order instead of second order, so it can be checked with the same algorithm used to check pred calc definitions.  Most people wouldn't even notice the change outside of the definition itself, which we can explain in its description.  It's similar to how we moved up the set theory wceq, wcel into pred calc.  It affects only one definition and one proof, and if we decide it was a mistake it is easily reverted.

By the way, I talked to my advisor about this and he's in favor of using pred calc for the definition. From my point of view all the axioms will require justification anyway and "wff T.", "|- T." is short and sweet and is not hard to justify, but I can live with either one. I can live with |- T. <-> ( ph <-> ph ) too but it will be an axiom, not a definition, so it just looks like a more complicated axiom than |- T. to me.

I think it's important that we have T. as a symbol; as you've noted it gets used as the nullary context in natural deduction proofs. In a perfect world maybe we might have a prop calc database with an axiomatic T., and a pred calc / ZFC database where it's a definition. The issue seems to be having both of these at the same time.

 

Not in definitions. But there is another aspect to this that I haven't yet mentioned, and that's using free wff/class metavariables in proofs. Metamath allows it, but I think it's considered bad practice and once you have T. and _V, they are always eliminable. My HOL translation is almost to the point where it will report these as errors, so I will find out then what needs cleaning up.

A more contentious case is using free set variables. These are also permitted by Metamath, but they are probably necessary in some cases and will need support from the language. The ability to drop free set variables basically amounts to the assertion that the collection of all sets is nonempty, which is assumed pretty early on in pred calc. For example, we can prove the following (theorem 19.2):

1 |- ( A. x ph -> ph )

2 |- ( ph -> E. x ph )

3:1,2:syl |- ( A. x ph -> E. x ph )

Without a proper analysis of the variable dependencies here, it's not obvious what just happened, but this theorem claims that there exists an element in the universe (we can use T. for ph to discharge the assumption). The problem isn't with step 1 or step 2, which are both true in FOL without any nonempty assumption, and of course 3 can't be at issue because it's just prop calc, so where did the element come from? The answer comes if we view this under the HOL translation. Since ph is not disjoint with x it depends on x, so we get the following:

1 !x. |- ( all (\x. ph(x)) -> ph(x) )

2 !x. |- ( ph(x) -> ex (\x. ph(x)) )

3' !x. |- ( all (\x. ph(x)) -> ex (\x. ph(x)) )

3  |- ( all (\x. ph(x)) -> ex (\x. ph(x)) )

The key is the move from step 3' to 3, which we don't even have language for in metamath. Statements 1 and 2 have a free variable x (it is bound in A. x ph(x) but not in ph(x)) so the variable binding is outside the provability judgment (that's what the !x. meta-quantification means). When you compose those with syl you get 3', which still has a variable binding !x. outside, which is now binding nothing because x is already bound in all occurrences in the formula. So we deduce 3, throwing away the variable x using the fact that the sort that x ranges over is nonempty (i.e. there exists a set).

I've made some token efforts to support "free" sorts, in which we don't assume nonemptiness and thus we aren't permitted to drop dummy variables whenever we like, but I'm not sure about being able to track this properly through proofs without slowing the core down, which I don't want (I want the MM0 verification loop to be exactly as complicated as the MM check: direct substitute and check for equality, DV check, repeat.) Then again, I already have to keep track of the set of variables present in a formula, and the set of free variables is only marginally harder to calculate. I should do some tests to find out, but that will have to wait until I have the C verifier and binary format and can start playing with performance optimization (the Haskell verifier is built for correctness, not speed). The goal is to beat the performance of smm - verify set.mm (translated to MM0) in less than 800 ms.

Mario

[Norman Megill]

On Tuesday, May 7, 2019 at 8:28:26 PM UTC-4, Mario Carneiro wrote:
...

 

But there is another aspect to this that I haven't yet mentioned, and that's using free wff/class metavariables in proofs. Metamath allows it, but I think it's considered bad practice and once you have T. and _V, they are always eliminable. My HOL translation is almost to the point where it will report these as errors, so I will find out then what needs cleaning up.

A more contentious case is using free set variables. These are also permitted by Metamath, but they are probably necessary in some cases and will need support from the language. The ability to drop free set variables basically amounts to the assertion that the collection of all sets is nonempty, which is assumed pretty early on in pred calc. For example, we can prove the following (theorem 19.2):

1 |- ( A. x ph -> ph )

2 |- ( ph -> E. x ph )

3:1,2:syl |- ( A. x ph -> E. x ph )

Without a proper analysis of the variable dependencies here, it's not obvious what just happened, but this theorem claims that there exists an element in the universe (we can use T. for ph to discharge the assumption). The problem isn't with step 1 or step 2, which are both true in FOL without any nonempty assumption,

Steps 1 and 2 don't hold in a free logic (a logic that allows an empty domain).

An axiomatization for free logic very close to the Tarski's S2 we use (in fact is based on it, and it allows the use of free variables in the same way as we do) is on p. 277 of

Hugues LeBlanc, On Meyer and Lambert's Quantificational Calculus FQ, J. Symb. Logic 33 (1968) 275--280

It allows the use of free variables in the same way as we use them, restricted of course by weaker axioms (so we can't derive ~ sp for example).

Norm

 

[Mario Carneiro]

On Wed, May 8, 2019 at 1:08 AM Norman Megill <n...@alum.mit.edu> wrote:

On Tuesday, May 7, 2019 at 8:28:26 PM UTC-4, Mario Carneiro wrote:
...

 

But there is another aspect to this that I haven't yet mentioned, and that's using free wff/class metavariables in proofs. Metamath allows it, but I think it's considered bad practice and once you have T. and _V, they are always eliminable. My HOL translation is almost to the point where it will report these as errors, so I will find out then what needs cleaning up.

A more contentious case is using free set variables. These are also permitted by Metamath, but they are probably necessary in some cases and will need support from the language. The ability to drop free set variables basically amounts to the assertion that the collection of all sets is nonempty, which is assumed pretty early on in pred calc. For example, we can prove the following (theorem 19.2):

1 |- ( A. x ph -> ph )

2 |- ( ph -> E. x ph )

3:1,2:syl |- ( A. x ph -> E. x ph )

Without a proper analysis of the variable dependencies here, it's not obvious what just happened, but this theorem claims that there exists an element in the universe (we can use T. for ph to discharge the assumption). The problem isn't with step 1 or step 2, which are both true in FOL without any nonempty assumption,

Steps 1 and 2 don't hold in a free logic (a logic that allows an empty domain).

I disagree. If I'm wrong about this the HOL translation needs a major rewrite, but step 1 should hold in a free logic, because it's true for all values of the free argument x. Presumably you agree that the following statement is true in a free logic (this is just FOL, not metamath):

|- A. y (A. x P(x) -> P(y))

Under the interpretation of statements as their universal closures, this is the same as

!y. |- A. x P(x) -> P(y)

or

!x. |- A. x P(x) -> P(x)

and that's what I claim the metamath statement |- A. x ph -> ph (where there is no DV condition on x,ph) is claiming.

Possibly the confusion is that if ph does *not* depend on x, or it has a DV condition, then the translation is more like

|- A. x P -> P

which is already a closed formula, i.e. it has no outer x quantifier. I agree that this statement is not necessarily true in a free logic, so that for instance the following is not provable:

|- A. x F. -> F.

This suggests a restriction of substitution to predicates ph which *must* contain free x, in order to prevent the loss of the outer !x. quantifier. LeBlanc seems to have a similar restriction in his axiomatization (the rule A. x ( ph -> ps ) -> A. x ph -> A. x ps requires that ps contain a free x).

That said, this doesn't sound like the kind of restriction that is possible to achieve in metamath (at least not "for free") so I'll probably drop the "free" modifier for sorts because there isn't an easy way to implement it without affecting the core verifier.

Mario

[fl]

I disagree. If I'm wrong about this the HOL translation needs a major rewrite, but step 1 should hold in a free logic, because it's true for all values of the free argument x. Presumably you agree that the following statement is true in a free logic (this is just FOL, not metamath):

It would be easier to settle this issue with a formal definition of semantics. There must be one in Goldblatt's Topoi,chapter 11. For

me the meaning of an unquantified predicate with a variable is unclear. Especially if the statements can be identified with their

universal closure or not (if that's what you mean). 

-- 

FL

[David A. Wheeler]

> On 5/6/19 12:00 PM, Norman Megill wrote:
> > There are another 361 uses of wtru beyond prop calc, and from a quick
> > check it seems they are mainly used to convert deductions into inferences.

There are a lot of *indirect* uses of the definition of ` T. ` , though.
For example, constant false is defined in df-fal as ` ( F. <-> -. T. ) ` ,
and constant false shows up in many places.

I ran:
metamath 'read set.mm' 'show usage df-tru /recursive' quit
and it reported:
Statement "df-tru" directly or indirectly affects the proofs of 28606 statements:
...

So I think we definitely need to keep T. (and F.).

The latest set.mm now discourages the use of df-tru, and df-tru is only used to
prove tru which is ` |- T. ` . Everything else depends on tru.
That will make it easier to change the definition of T. if we do so.

Now we just need to decide
if we're going to change the definition of T. (and to what if it's changed).
There's actually a lot of use of T. and F. in the prop calc section,
beyond just their definitions and the truth tables.
Other sections that use T. or F. include:
* "Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms"
* "Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom"
* "Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom"
I'm warming up to the idea of moving the syntax definitions of
A. , x , and so on as needed (but only as needed).
They'd be "earlier than otherwise needed", but
it's really just the syntax that we'd be
moving earlier, and that syntax will be eventually be used anyway.
Moving them up, and leaving the rest where they are (even though it's longer),
might be the easiest approach.

--- David A. Wheeler

[Norman Megill]

On Wednesday, May 8, 2019 at 1:34:29 PM UTC-4, David A. Wheeler wrote:

> On 5/6/19 12:00 PM, Norman Megill wrote:
> > There are another 361 uses of wtru beyond prop calc, and from a quick
> > check it seems they are mainly used to convert deductions into inferences.

There are a lot of *indirect* uses of the definition of ` T. ` , though.
For example, constant false is defined in df-fal as ` ( F. <-> -. T. ) ` ,
and constant false shows up in many places. 

I ran:
  metamath 'read set.mm' 'show usage df-tru /recursive' quit
and it reported:
  Statement "df-tru" directly or indirectly affects the proofs of 28606 statements:

All indirect uses of df-tru would automatically disappear if the 361 uses in theorems which don't contain T. or F.  were eliminated.  That's what I meant.   So we would have to change only 361 proofs, not 28K proofs.

To eliminate a direct use of tru in a proof is trivial; we would replace T. by x=x for example, which is the kind of thing we did before df-tru was added.  The effect on the proof size would be minimal, maybe a few bytes longer in some cases and a few bytes shorter in others depending on how the compression reuses things.

I am by no means advocating that we stop using df-tru.  There is no danger that it will disappear.  This is just hypothetical, to show that df-tru, while it may be convenient, is not essential in the same way as say df-pw, which if eliminated would cause proof sizes to explode dramatically.

 

  ...

So I think we definitely need to keep T. (and F.).

The latest set.mm now discourages the use of df-tru, and df-tru is only used to
prove tru which is ` |- T. ` .  Everything else depends on tru.
That will make it easier to change the definition of T. if we do so.

Now we just need to decide
if we're going to change the definition of T. (and to what if it's changed).
There's actually a lot of use of T. and F. in the prop calc section,
beyond just their definitions and the truth tables.
Other sections that use T. or F. include:
* "Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms"
* "Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom"
* "Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom"

There are 83 theorems in prop calc including the above that depend directly or indirectly on df-tru and df-fal.  That isn't a huge number.  These would be moved to the end of prop calc if we decide to use the pred calc definition of df-tru.  (There are a few more assuming we want to keep each alternate axiomatization together in a section, but I don't think it's a lot.)

In the alternate axiomatizations, F. is typically primitive and -. ph is defined by ( pn -> F. ).  Care has to be taken not to "cheat" in their proofs, which are somewhat protected by "Proof modification is discouraged", but 100% confidence that they don't cheat can only be obtained by manual inspection.  An argument can be made that they don't really belong in set.mm because of this, but I'm ok with it for now.  Worst case they can be extracted into their own .mm files to show that they aren't contaminated.

Norm
 

[David A. Wheeler]

On Wed, 8 May 2019 12:45:58 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> I am by no means advocating that we stop using df-tru. There is no danger
> that it will disappear. This is just hypothetical, to show that df-tru,
> while it may be convenient, is not essential in the same way as say df-pw,
> which if eliminated would cause proof sizes to explode dramatically.

Thanks for clarifying that T. (and presumably F.) will stick around!

> There are 83 theorems in prop calc including the above that depend directly
> or indirectly on df-tru and df-fal. That isn't a huge number. These would
> be moved to the end of prop calc if we decide to use the pred calc
> definition of df-tru. (There are a few more assuming we want to keep each
> alternate axiomatization together in a section, but I don't think it's a
> lot.)

I agree, that doesn't sound like a huge number.

--- David A. Wheeler

[David A. Wheeler]

On Tue, 7 May 2019 20:27:37 -0400, Mario Carneiro <di....@gmail.com> wrote:
> Yes. Put another way, the reason df-tru is not in the exception list is
> because there is an entire section of the definition checker devoted to
> checking df-tru. The only other justification theorems in set.mm are
> eujust, which is the first definition with a dummy set variable, and vjust,
> which is the first definition with a dummy variable bound by a class
> abstraction. I guess these are merely illustrative, because there aren't
> nearly enough of them to support all of set.mm. MM0 is going to have to
> prove justification theorems for everything else, using either CondEq
> (which is theoretically sufficient but practically a bit cumbersome) or
> some more canonical proof style (which would require more explicit
> references to theorems and so more $j's).

> Unless you think it is worthwhile
> to require justification theorems for all new definitions?

Serious question: How hard would it be to require justification theorems in
set.mm / iset.mm after some period of time?

I think the general spirit of Metamath is to
prove "everything". Definitions are in some sense an exception,
because from the point-of-view of Metamath they are $a statements.
So if it's not too hard to add justifications for each definition over time,
and also routinely do it for all new definitions, there could be advantages.
E.g., the justifications could be checked by *all* Metamath
verifiers. not just mmj2 and/or Metamath Zero, so it'd be even
clearer that the definitions were fine. In addition, this might be
a way to speed definition checks: If the justification is already
provided, you just have to check the proof steps vs. re-figuring it out.

That said, if it's too hard then the status quo clearly works.
The risk of definitions being a problem is pretty small.
Definitions are a small percentage of the assertions,
and they're generally in a form that is easy for both humans and mmj2 to check.

If asking for justifications in set.mm is being seriously considered,
then I'd like to see a few examples. I'm not sure I understand what is
being justified & what it would take to prove those justifications.
I've never written a justification for set.mm, since mmj2 "checks automatically".
If we're talking about the mmj2 definition check specifically,
I don't see how we can easily prove the following, so I presume these
would not be handled by a justification theorem:
* I-PA-0201 The root symbol is not = or <->.
* I-PA-0202 The previous axiom %s uses the symbol being defined in this axiom.
* I-PA-0203 Variables %s in the definiendum are required NOT to be distinct.
* I-PA-0204 All dummy variables in the definiens are required to be distinct from each other and from variables in the definiendum. The following DJ conditions need to be added:\n%s

So it seems to that the justification theorem (or theorems)
is merely trying to prove that each dummy variable
is not free, that is, that ( ph -> A. x ph ) for each dummy variable x that's not a setvar.
That's the essence of:
* I-PA-0205 Non-set dummy variable found, and no justification theorem is available.
* I-PA-0206 Dummy variables %s are possibly free in the definiendum, and no justification is available.

Is that right? Are there examples? For example, what would you need to prove for df-ne ?

--- David A. Wheeler