New $j commands; LTL section is not valid

[Mario Carneiro]

I've been working on a definition checker v2.0 using the new Scala verifier, backed up by the theory of http://us.metamath.org/ocat/defn/defn.pdf. Unlike the mmj2 definition checker, this one will rely less on automated theorem proving (which is I think antithetic to Metamath, particularly when we need to trust the result) and more on explicit annotations.

I'm not quite done yet, so the list may expand more, but for now here is the complete list of recognized $j commands. A statement of the form command 'string' ...; below means that commands of the form "command 'string1' 'string2' 'string3';" are valid and are shorthand for "command 'string1'; command 'string2'; command 'string3';".

* grammar; This database is grammatical

* unambiguous; The database is unambiguous, no proof

  * unambiguous "proof"; The database is unambiguous because the given parser works on it

* syntax 't1' as 't2'; Declare the non-variable typecode t1 to be parsed as variable typecode t2

  * syntax 't' ...; Declare variable typecode t.

-----> The above commands were already described earlier and are in set.mm. Now the new stuff:

* primitive 'p' ...; Declare several syntax axiom p as primitive, meaning that it will not be defined. This can in principle be derived by looking at which syntax axioms don't have definitions, but it is much more likely that this is a missing definition and we want to report this.

* equality 'eq' from 'refl' 'sym' 'trans'; Declare syntax axiom 'eq' to be an equality for its type, with the given theorems demonstrating that it is an equivalence. set.mm declares two of these:
  - equality 'wb' from 'biid' 'bicomi' 'bitri';
  - equality 'wceq' from 'eqid' 'eqcomi' 'eqtri';

  There's no need for any more of these unless we get a new typecode. But the three theorems is not all you need for an equality to be valid:

* congruence 'thm' ...; This registers thm as a congruence theorem. The checker is looking for a very specific signature for these; it should look like |- A = B & |- C = D => f(x,A,B) = f(x,C,D), where f is a primitive syntax operation. The variables that have a registered equality (that is, class and wff) need to be replaced, and the others (set) should not. Thus the congruence theorems declared in set.mm are notbii, imbi12i, albii, eqeq12i, eleq12i, and abbii. Although cv is also a primitive operation, it does not need an equality theorem because it has no non-set parameters.

* definition 'defn' for 'syn'; Declares that 'defn' is the definitional assertion corresponding to syntax axiom 'syn'. Since these are so common, they are automatically discovered, so it is generally not necessary to annotate this. It is only used explicitly once in set.mm: "definition 'dfbi1' for 'wb';" which allows us to discover the substitution that df-bi is supposed to represent.

* justification 'just' for 'thm'; I haven't fully worked out when this will be necessary, but for now it is being used to note "justification 'bijust' for 'df-bi';", with the intended meaning being that inlining the definition of wb in df-bi results in bijust, which is provable without df-bi. This leads to a justification of df-bi as conservative.

In the course of this project, I'm discovering a number of subtle errors in set.mm which I'm fixing as I go along. There were two big issues that needed adjustments in many places. First, class constants that have no definition are not conservative. This often results when the definitional axiom is commented out, but the class constant is not. In these cases I just commented out the class constant. Second, unlike mmj2 this definition checker requires that the *class constants* appear in dependency order, not just the definitions. (In fact it doesn't require any ordering at all on the axioms, because the conservativity proof is "holistic", considering the effect of everything on everything else. The class constant introduction order indicates what sequence of language extensions is used.)

In the LTL section, there is some added complexity because it is an axiomatic extension, which requires new "primitive" annotations, and corresponding "congruence" proofs. What's more, it actually caught a real bug in the section: there is no congruence law for "until" (http://us2.metamath.org:88/mpegif/wunt.html), and from what I can tell it's not provable either.

For now, I've fixed the problem by adding the following axiom:

  ${
    ax-untbi12i.1 $e |- ( ph <-> ps ) $.
    ax-untbi12i.2 $e |- ( ch <-> th ) $.
    $( Congruence axiom for until.
       (Contributed by Mario Carneiro, 11-Aug-2016.) $)
    ax-untbi12i $a |- ( ( ph until ch ) <-> ( ps until th ) ) $.
    $( [11-Aug-2016] $)

    $( $j congruence 'ax-untbi12i'; $)
  $}

FL, you should find out what other axioms you would prefer in order to prove this - I couldn't find a source with your exact six axioms, so I'm not sure what it is supposed to look like.

Mario

[Norman Megill]

On 8/11/16 2:17 AM, Mario Carneiro wrote:
> I've been working on a definition checker v2.0 using the new Scala
> verifier, backed up by the theory of
> http://us.metamath.org/ocat/defn/defn.pdf. Unlike the mmj2 definition
> checker, this one will rely less on automated theorem proving (which is
> I think antithetic to Metamath, particularly when we need to trust the
> result) and more on explicit annotations.
>

...

> In the course of this project, I'm discovering a number of subtle errors

> in set.mm <http://set.mm> which I'm fixing as I go along. There were two

> big issues that needed adjustments in many places. First, class
> constants that have no definition are not conservative. This often
> results when the definitional axiom is commented out, but the class
> constant is not. In these cases I just commented out the class constant.

What do you mean by "not conservative"? Can you give an example?

...

> In the LTL section, there is some added complexity because it is an
> axiomatic extension, which requires new "primitive" annotations, and
> corresponding "congruence" proofs. What's more, it actually caught a
> real bug in the section: there is no congruence law for "until"
> (http://us2.metamath.org:88/mpegif/wunt.html), and from what I can tell
> it's not provable either.
>
> For now, I've fixed the problem by adding the following axiom:
>
> ${
> ax-untbi12i.1 $e |- ( ph <-> ps ) $.
> ax-untbi12i.2 $e |- ( ch <-> th ) $.
> $( Congruence axiom for until.
> (Contributed by Mario Carneiro, 11-Aug-2016.) $)
> ax-untbi12i $a |- ( ( ph until ch ) <-> ( ps until th ) ) $.
> $( [11-Aug-2016] $)
>
> $( $j congruence 'ax-untbi12i'; $)
> $}
>
> FL, you should find out what other axioms you would prefer in order to
> prove this - I couldn't find a source with your exact six axioms, so I'm
> not sure what it is supposed to look like.

FL sent me a new mathbox that strips out everything not related to
geometry, and this material has been deleted. Maybe you can wait a day
or so until I update set.mm.

Norm

[Mario Carneiro]

I'd like to replace df-sb with the axiom:

ax-clabsb $a |- ( A e. { x | ph } <-> ( ( x = A -> ph ) /\ E. x ( x = A /\ ph ) ) ) $.

This is the generalization of df-sb to a class argument, followed by an application of df-sbc. If this was taken as axiomatic (and also called an axiom), it would be more true to the reality of the set.mm axiomatization, in which cv and cab are primitive operations, and csb is only pretending to be primitive (due to connective overloading, the left hand side of df-sb is not a single axiom, but is actually grammatically parsed as (wsbc (cv vy) vx wph)).

[Mario Carneiro]

On Thu, Aug 11, 2016 at 2:33 AM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/11/16 2:17 AM, Mario Carneiro wrote: 

...

In the course of this project, I'm discovering a number of subtle errors
in set.mm <http://set.mm> which I'm fixing as I go along. There were two
big issues that needed adjustments in many places. First, class
constants that have no definition are not conservative. This often
results when the definitional axiom is commented out, but the class
constant is not. In these cases I just commented out the class constant.

What do you mean by "not conservative"?  Can you give an example?

Now that I come to think of it, perhaps "conservative" is not the right word. I mean the extension is not completely determined by its values on the primitive operations; in fact, an unconstrained class constant *is* a new (0-ary) primitive operation. For examples, that's easy enough:

$c Foo $.

cfoo $a class Foo $.

Here Foo has not been given a definition, so it could be anything, and a model of this formal system must assign some value to Foo. If it is given a definition, then in every model the value for Foo can be derived from the value at the other primitive operations.

Since it is a 0-ary primitive operation, there are no additional congruence obligations, but if a statement later appears containing a Foo, it can not be expanded into a statement not containing Foo. (That's not nonconservativity, but it's undesirable nonetheless.)

Mario

[Norman Megill]

On 8/11/16 2:33 AM, Mario Carneiro wrote:
> I'd like to replace df-sb with the axiom:
>
> ax-clabsb $a |- ( A e. { x | ph } <-> ( ( x = A -> ph ) /\ E. x ( x = A
> /\ ph ) ) ) $.
>
> This is the generalization of df-sb to a class argument, followed by an
> application of df-sbc. If this was taken as axiomatic (and also called
> an axiom), it would be more true to the reality of the set.mm

> <http://set.mm> axiomatization, in which cv and cab are primitive

> operations, and csb is only pretending to be primitive (due to
> connective overloading, the left hand side of df-sb is not a single
> axiom, but is actually grammatically parsed as (wsbc (cv vy) vx wph)).

The issue with adding an axiom is that it implies that the ZFC axioms
are inadequate for standard mathematics, which is a very wrong
impression to give the user. It is a ZFC "marketing" issue. :) See the
last subsection "Definitions or axioms?" at
http://us.metamath.org/mpegif/mmset.html#class .

The reason df-sbc is a definition is that it is an eliminable and
conservative ZFC extension. Because of the connective overloading, we
might need justification "outside" of Metamath or the definition checks
you are writing, but that is also the case with df-clel, df-cleq.

I would prefer using a separate connective for df-sbc rather than add a
new axiom, if that's what it takes. However, I don't see how the
overloading of df-sbc causes any problems that are different from the
overloading of df-clel, df-cleq.

Norm

[Mario Carneiro]

Ah, yeah I suppose we would want to do it for them too.

Here's the idea: set.mm is an axiomatization of ZFC *with classes*. That includes the fact that there are three typecodes, and enough axioms to make them all play well together. The right way to talk about conservative extension here from ZFC without classes is to have a separate spinoff database, in which "class" never makes an appearance, and then rigorously define the mapping from each primitive of standard set.mm to the reduced version. This would be backed up with an informal proof and/or a computer verification. As it is it's a bit of a muddled mess piecing out what is conservative and what isn't, and the df-* axioms aren't making it any better. I would much prefer, now that definition checking is on solid ground, for *all* our definitions to be definitions, *no exceptions* (to paraphrase a recent youtube video).

Additionally, I'm pretty sure that you will end up with *fewer* axioms (counting df-clel and friends as axioms) if you use classes through and through.

Mario

[Mario Carneiro]

On Thu, Aug 11, 2016 at 3:05 AM, Norman Megill <n...@alum.mit.edu> wrote:

I would prefer using a separate connective for df-sbc rather than add a new axiom, if that's what it takes.

On second thought, maybe this isn't such a bad idea. There is precedence with the <RR relation in the real number axioms: use some "axiomatic" non-overloaded basic connective for the initial definition, and then immediately show equivalence to the standard one and use that everywhere. We would still have to have cab and cv as primitives, but at least the total number of primitives would not go up, and df-cleq/df-clel would be actual definitions.

[Mario Carneiro]

Have you attempted to actually work out what is the actual "overloading" that you are doing with wceq and wcel? It is not at all obvious to me how to de-overload it.

Let's define two operations, x = y which acts on sets, and A =2 B for classes. For elementhood, we have three, x e. y, x e.2 A, and A e.3 B. I'm also going to write (x) to denote (cv x), so it is obvious when it occurs. There is a natural de-overloading coming from df-cleq and df-clel:

|- (x) =2 { y | y e. x }

|- ( A =2 B <-> A. x ( x e.2 A <-> x e.2 B ) )
|- ( A e.3 B <-> E. x ( (x) =2 A /\ x e.2 B ) )

(Note that the de-overloaded df-cleq does not need a hypothesis.) The first one is the definition of cv, which is implicitly there in order to promote x to a class on the left.

First, we can justify e.2 over e., which means we need to prove

|- ( x e. y <-> x e.2 (y) )

|- ( x e. y <-> x e.2 { z | z e. y } )
|- ( x e. y <-> [ x / z ] z e. y )

which is a theorem of pred calc.

Next, we justify the overloading of = with =2, which expands to

|- ( x = y <-> (x) =2 (y) )
|- ( x = y <-> A. z ( z e. x <-> z e. y ) )

which is the axiom of extensionality.

Finally, we want to justify the overloading of e.3 with e.2, which expands to

|- ( x e.2 A <-> (x) e.3 A )
|- ( x e.2 A <-> E. y ( y = x /\ y e.2 A ) )

but this is not cleljust at all! We need the theorem

ax-14c $a |- ( x = y -> ( x e.2 A -> y e.2 A ) )

and I'm not sure where we're getting that one from, because that's a stronger statement than ax-14. In other words, e.2 is conservative over e., but e.3 is not conservative over e.2 because with only e.2 (and the axiom df-clab) you are missing a congruence axiom. Also, keep in mind that e.2 does not have a definition; it must be a primitive operation. (By the way, this is one of those "metalogical completeness" issues: if the collection of classes is inductive, all generated by class builders on some wff, then ax-14c is provable; but in Metamath "class" is its own typecode, which can be inhabited by mystery classes that have no such expression.)

Any chance of upgrading ax-14 into ax-14c so that df-clel is actually conservative? Otherwise you will need to do the same trick of having df-clel take a hypothesis to ensure it is conservative.

[Norman Megill]

Class variables are intended to range over class builders, so there is
some ph such that A represents { z | ph }.

|- ( x e.2 { z | ph } <-> (x) e.3 { z | ph } )

The lhs reduces to [x/z]ph by df-clab. For the rhs we have

|- ( (x) e.3 { z | ph } ) <-> E. y ( y = x /\ y e.2 { z | ph } ) )
<-> E. y ( y = x /\ [y/z]ph ) ) by df-clab
<-> [x/z]ph by pred calc

If abid2 A = { z | z e.2 A } can be proved with strict e., e.2, and e.3
all the way back to the definitions (I haven't checked), then we can
replace ph with z e.2 A and will have a direct proof for your original
(x) e. 3 A case. I think ax-ext will be needed for the proof; if so, we
should add ax-ext as a hypothesis to df-clel like we now do for df-cleq.

>
> but this is not cleljust at all! We need the theorem

As its comment indicates, cleljust provides only "part of the
justification", and is admittedly rather weak for the general case. :)

>
> ax-14c $a |- ( x = y -> ( x e.2 A -> y e.2 A ) )
>

This is ugly.

> and I'm not sure where we're getting that one from, because that's a
> stronger statement than ax-14. In other words, e.2 is conservative over
> e., but e.3 is not conservative over e.2 because with only e.2 (and the
> axiom df-clab) you are missing a congruence axiom. Also, keep in mind

(Why do you use "congruence" instead of "equality" as in set.mm?)

> that e.2 does not have a definition; it must be a primitive operation.
> (By the way, this is one of those "metalogical completeness" issues: if
> the collection of classes is inductive, all generated by class builders
> on some wff, then ax-14c is provable; but in Metamath "class" is its own
> typecode, which can be inhabited by mystery classes that have no such
> expression.)
>
> Any chance of upgrading ax-14 into ax-14c so that df-clel is actually
> conservative?

No. :)

Otherwise you will need to do the same trick of having
> df-clel take a hypothesis to ensure it is conservative.

This would be fine, since we already do that for df-cleq. Some of the
wording on the MPE home page class explanation will have to be changed
(as well as set.mm).

Norm

[Mario Carneiro]

On Thu, Aug 11, 2016 at 11:01 AM, Norman Megill <n...@alum.mit.edu> wrote:

Class variables are intended to range over class builders, so there is some ph such that A represents { z | ph }.

This is exactly the statement that the typecode "class" is inductively defined. The equivalent for wffs is "wff variables are intended to range over wffs, so there are some variables such that ph equals A. x ph, or x = y, or x e. y, or -. ph, or ( ph -> ps )". I'm playing your own arguments back at you here. ax-17 is provable in all of these cases, yet it is not a theorem in general, because *in Metamath typecodes are not inductively defined*. This is really important to understand. They can be inhabited by "atoms" which are not the result of any syntax construction. (Actually, I should say that typecodes are not coinductive, because I'm talking about a destructuring law which has no base case, but I don't think you're familiar with coinduction and it's not all that relevant anyway since this is what metamath isn't.)

If abid2 A = { z | z e.2 A } can be proved with strict e., e.2, and e.3 all the way back to the definitions (I haven't checked),

It can't. You have to prove

|- ( y e.2 A <-> y e.2 { z | z e.2 A } )
|- ( y e.2 A <-> [ y / z ] z e.2 A )

and the latter is going to need to relate y e.2 A to z e.2 A at some point.

Here's a specific model that should show what I'm talking about. Let A0 be an atomic class such that x e.2 A0 is true only for x = v0, but have otherwise behave according to standard set theory, i.e. x e.2 (y) iff x e. y, x e.2 { z | ph } iff [ x / z ] ph. The available class terms are A0, (y) for some y, and { x | ph } for some x,ph.

Obviously ax-14c is not satisfied, because ( v0 = v1 -> ( v0 e.2 A0 -> v1 e.2 A0 ) ) is false. Since A0 is not (y) for any y (because A0 is atomic), all the axioms of predicate calculus (which use x e.2 (y) pretending to be x e. y) are true. And ax-cleq, x e.2 { y | ph } <-> [ y / x ] ph is true.

In case you are curious how A0 can be different from { x | x e.2 A0 }: the value of this depends on x. If x = v0, then { v0 | v0 e. A0 } is _V, while if x =/= v0 then { x | x e. A0 } is (/). In both cases the result is different from A0: in the first case, v1 e. _V is true even though v1 e. A0 is false, and v0 e. (/) is false but v0 e. A0 is true. So abid2 is also not true in this model.

 

ax-14c $a |- ( x = y -> ( x e.2 A -> y e.2 A ) )

This is ugly.

I should note that need only be introduced in the class builder section, although obviously it subsumes ax-14. Axioms ax-14c and ax-clab completely cover the axiomatic part of class theory, and they are provably conservative over predicate calculus + ax-ext. Given these two, df-cleq and df-clel can be justified as definitions and not axioms.

and I'm not sure where we're getting that one from, because that's a
stronger statement than ax-14. In other words, e.2 is conservative over
e., but e.3 is not conservative over e.2 because with only e.2 (and the
axiom df-clab) you are missing a congruence axiom. Also, keep in mind

(Why do you use "congruence" instead of "equality" as in set.mm?)

The command "equality" is used to introduce an equality operator, that is, 'wb' and 'wceq'. Command 'congruence' is used to introduce an equality *theorem*, also known as a congruence law, like notbii. Obviously notbii is not itself an equality.

 

Otherwise you will need to do the same trick of having

df-clel take a hypothesis to ensure it is conservative.

This would be fine, since we already do that for df-cleq.  Some of the wording on the MPE home page class explanation will have to be changed (as well as set.mm).

Actually, this would not completely resolve the situation - you would still need ax-14c because it is (metalogically) independent of the other axioms, just as we currently need ax-ext to justify df-cleq. In case it wasn't obvious, currently ax-14c is getting snuck in through the "definition" df-clel, which is not what we want definitions to do.

Mario

[Mario Carneiro]

More LTL surprises: In order to formalize the not-free predicate, we need a metatheorem for proving ( x = y -> A(x) = A(y) ) for each expression A(x) in the language. Generally, this is done using theorems like eqeq12d. But for linear temporal logic, we need a theorem of the form

$e |- ( x = y -> ( ph <-> ps ) )

$a |- ( x = y -> ( [,] ph <-> [,] ps ) )

and this is actually *not true* in LTL and other modal logics. I haven't worked it all out, but I think this means that definitions like

$a |- Magic = { x | [,] x = (/) }

are actually not well-formed. Of course, the people who originally came up with modal logic weren't thinking about predicate calculus, but in set.mm everyone has to play in the same sandbox, which leads to... complications. I'm not sure how best to delimit "little theories" within set.mm, declaring that certain combinations of axioms are mutually exclusive. If we used includes more, this would be simple - the LTL section could just take from prop calc and stay away from the rest of set.mm. But as it is now, somehow it all has to be mutually consistent in order to formally verify that everything makes sense, regardless of how definitions attempt to use the axioms.

Maybe this is why people prefer the model theory of LTL to the proof theory. ;)

Mario

[Norman Megill]

On 8/11/16 12:27 PM, Mario Carneiro wrote:
> (Why do you use "congruence" instead of "equality" as in set.mm

> <http://set.mm>?)

>
> The command "equality" is used to introduce an equality operator, that
> is, 'wb' and 'wceq'. Command 'congruence' is used to introduce an
> equality *theorem*, also known as a congruence law, like notbii.
> Obviously notbii is not itself an equality.

In set.mm we have been saying that things connected by <-> are
"(logically) equivalent" and by = are "equal". I only recall seeing
"congruence" used in the context of equivalence relations and quotient
structures but not for logical equivalence. Have you seen your usage in
the literature?

>
>
> Otherwise you will need to do the same trick of having
>
> df-clel take a hypothesis to ensure it is conservative.
>
>
> This would be fine, since we already do that for df-cleq. Some of
> the wording on the MPE home page class explanation will have to be

> changed (as well as set.mm <http://set.mm>).

>
>
> Actually, this would not completely resolve the situation - you would
> still need ax-14c because it is (metalogically) independent of the other
> axioms, just as we currently need ax-ext to justify df-cleq. In case it
> wasn't obvious, currently ax-14c is getting snuck in through the
> "definition" df-clel, which is not what we want definitions to do.

While this may be a useful exercise, I don't think we should change to
non-overloaded = and e. connectives for the standard set.mm. Our
present method is very convenient, and the various class theory proofs
(Levy, T&Z, Quine) show that df-clab/cleq/clel are an eliminable ZFC
extension, even if our present definition checking tools can't prove it.
They meet all of the things one expects of a definition: any theorem
using class theory, and all of its proof steps, can be unambiguously
translated to an equivalent theorem and proof steps in pure ZFC language
without class theory. The purpose of class theory is simply human
convenience, and it serves no mathematical purpose.

Adding a new axiom to ZFC just because of inadequate definition checkers
sends the very wrong message that ZFC itself is inadequate.

Norm

[Mario Carneiro]

On Thu, Aug 11, 2016 at 10:18 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/11/16 12:27 PM, Mario Carneiro wrote:

    (Why do you use "congruence" instead of "equality" as in set.mm
    <http://set.mm>?)

The command "equality" is used to introduce an equality operator, that
is, 'wb' and 'wceq'. Command 'congruence' is used to introduce an
equality *theorem*, also known as a congruence law, like notbii.
Obviously notbii is not itself an equality.

In set.mm we have been saying that things connected by <-> are "(logically) equivalent" and by = are "equal".  I only recall seeing "congruence" used in the context of equivalence relations and quotient structures but not for logical equivalence.  Have you seen your usage in the literature?

I remember Josef Urban calling my algorithm for proving x = y -> A(x) = A(y) a "congruence closure" algorithm. Dunno if that makes any sense, but it's the first thing that comes to mind. I also would agree that A(x) = A(y) is saying that each side is "equal", but x = y -> A(x) = A(y) is not equality itself but a conditional equality. But before you get too enamored of that term:

I've introduced a few new keywords for the $j statement, and a little section to make use of it. Rather than explain it I'll just use the existing comments.


$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
                    Conditional equality
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

  This is a very useless definition, which "abbreviates" ` ( x = y -> ph ) ` as
  ` CondEq ( x = y -> ph ) ` . What this display hides, though, is that the
  first expression, even though it has a shorter constant string, is actually
  much more complicated in its parse tree: it is parsed as
  (wi (wceq (cv vx) (cv vy)) wph), while the ` CondEq ` version is parsed as
  (wcdeq vx vy wph).  It also allows us to give a name to the specific 3-ary
  operation ` ( x = y -> ph ) ` .
 
  This is all used as part of a metatheorem: we want to say that
  ` |- ( x = y -> ( ph ( x ) <-> ph ( y ) ) ) ` and
  ` |- ( x = y -> A ( x ) = A ( y ) ) ` are provable, for any expressions
  ` ph ( x ) ` or ` A ( x ) ` in the language.  The proof is by induction, so
  the base case is each of the primitives, which is why you will see a theorem
  for each of the set.mm primitive operations.

  The metatheorem comes with a disjoint variables assumption: every variable in
  ` ph ( x ) ` is assumed disjoint from ` x ` except ` x ` itself.  For such a
  proof by induction, we must consider each of the possible forms of
  ` ph ( x ) ` .  If it is a variable other than ` x ` , then we have
  ` CondEq ( x = y -> A = A ) ` or ` CondEq ( x = y -> ( ph <-> ph ) ) ` ,
  which is provable by ~ cdeqth and reflexivity.  Since we are only working
  with class and wff expressions, it can't be ` x ` itself in set.mm, but if it
  was we'd have to also prove ` CondEq ( x = y -> x = y ) ` (where _set_
  equality is being used on the right).

  Otherwise, it is a primitive operation applied to smaller expressions.  In
  these cases, for each set variable parameter to the operation, we must
  consider if it is equal to ` x ` or not, which yields 2^n proof obligations.
  Luckily, all primitive operations in set.mm have either zero or one set
  variable, so we only need to prove one statement for the non-set constructors
  (like implication) and two for the constructors taking a set (the forall and
  the class builder).

  In each of the primitive proofs, we are allowed to assume that ` y ` is
  disjoint from ` ph ( x ) ` and vice versa, because this is maintained through
  the induction.  This is how we satisfy the DV assumptions of ~ cdeqab1 and
  ~ cdeqab .

$)

  $c CondEq $. $( conditional equality $)

  $( Extend wff notation to include conditional equality. This is a technical
     device used in the proof that ` NF ` is the not-free predicate, and that
     definitions are conservative as a result. $)
  wcdeq $a wff CondEq ( x = y -> ph ) $.

  $( Define conditional equality.  All the notation to the left of the ` <-> `
     is fake; the parentheses and arrows are all part of the notation, which
     could equally well be written ` CondEq x y ph ` . On the right side is the
     actual implication arrow. The reason for this definition is to "flatten"
     the structure on the right side (whose tree structure is something like
     (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy wph). $)
  df-cdeq $a |- ( CondEq ( x = y -> ph ) <-> ( x = y -> ph ) ) $.

  ${
    cdeqi.1 $e |- ( x = y -> ph ) $.
    $( Deduce conditional equality.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqi $p |- CondEq ( x = y -> ph ) $=
      ( wcdeq cv wceq wi df-cdeq mpbir ) ABCEBFCFGAHDABCIJ $.
      $( [11-Aug-2016] $)
  $}

  ${
    cdeqri.1 $e |- CondEq ( x = y -> ph ) $.
    $( Property of conditional equality.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqri $p |- ( x = y -> ph ) $=
      ( wcdeq cv wceq wi df-cdeq mpbi ) ABCEBFCFGAHDABCIJ $.
      $( [11-Aug-2016] $)
  $}

  ${
    cdeqth.1 $e |- ph $.
    $( Deduce conditional equality from a theorem.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqth $p |- CondEq ( x = y -> ph ) $=
      ( cv wceq a1i cdeqi ) ABCABECEFDGH $.
      $( [11-Aug-2016] $)
  $}

  ${
    cdeqnot.1 $e |- CondEq ( x = y -> ( ph <-> ps ) ) $.
    $( Distribute conditional equality over negation.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqnot $p |- CondEq ( x = y -> ( -. ph <-> -. ps ) ) $=
      ( wn wb cv wceq cdeqri notbid cdeqi ) AFBFGCDCHDHIABABGCDEJKL $.
      $( [11-Aug-2016] $)

    ${
      $d x z $.  $d y z $.
      $( Distribute conditional equality over quantification.

         (Contributed by Mario Carneiro, 11-Aug-2016.) $)

      cdeqal $p |- CondEq ( x = y -> ( A. z ph <-> A. z ps ) ) $=
        ( wal wb cv wceq cdeqri albidv cdeqi ) AEGBEGHCDCIDIJABEABHCDFKLM $.
        $( [11-Aug-2016] $)

      $( Distribute conditional equality over abstraction.

         (Contributed by Mario Carneiro, 11-Aug-2016.) $)

      cdeqab $p |- CondEq ( x = y -> { z | ph } = { z | ps } ) $=
        ( cab wceq cv wb cdeqri abbidv cdeqi ) AEGBEGHCDCIDIHABEABJCDFKLM $.
        $( [11-Aug-2016] $)
    $}

    ${
      $d x ps $.  $d y ph $.
      $( Distribute conditional equality over quantification.

         (Contributed by Mario Carneiro, 11-Aug-2016.) $)

      cdeqal1 $p |- CondEq ( x = y -> ( A. x ph <-> A. y ps ) ) $=
        ( wal wb cv wceq cdeqri cbvalv a1i cdeqi ) ACFBDFGZCDNCHDHIABCDABGCDEJK
        LM $.
        $( [11-Aug-2016] $)
 
      $( Distribute conditional equality over abstraction.

         (Contributed by Mario Carneiro, 11-Aug-2016.) $)

      cdeqab1 $p |- CondEq ( x = y -> { x | ph } = { y | ps } ) $=
        ( cab wceq cv wb cdeqri cbvabv a1i cdeqi ) ACFBDFGZCDNCHDHGABCDABICDEJK
        LM $.
        $( [11-Aug-2016] $)
    $}

    cdeqim.1 $e |- CondEq ( x = y -> ( ch <-> th ) ) $.
    $( Distribute conditional equality over implication.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqim $p |- CondEq ( x = y -> ( ( ph -> ch ) <-> ( ps -> th ) ) ) $=
      ( wi wb cv wceq cdeqri imbi12d cdeqi ) ACIBDIJEFEKFKLABCDABJEFGMCDJEFHMNO
      $.
      $( [11-Aug-2016] $)
  $}

  $( Conditional equality for set-to-class promotion.

     (Contributed by Mario Carneiro, 11-Aug-2016.) $)

  cdeqcv $p |- CondEq ( x = y -> x = y ) $=
    ( cv wceq id cdeqi ) ACBCDZABGEF $.
    $( [11-Aug-2016] $)

  ${
    cdeqeq.1 $e |- CondEq ( x = y -> A = B ) $.
    cdeqeq.2 $e |- CondEq ( x = y -> C = D ) $.
    $( Distribute conditional equality over equality.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqeq $p |- CondEq ( x = y -> ( A = C <-> B = D ) ) $=
      ( wceq wb cv cdeqri eqeq12d cdeqi ) CEIDFIJABAKBKICDEFCDIABGLEFIABHLMN $.
      $( [11-Aug-2016] $)

    $( Distribute conditional equality over elementhood.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    cdeqel $p |- CondEq ( x = y -> ( A e. C <-> B e. D ) ) $=
      ( wcel wb cv wceq cdeqri eleq12d cdeqi ) CEIDFIJABAKBKLCDEFCDLABGMEFLABHM
      NO $.
      $( [11-Aug-2016] $)
  $}

  ${
    $d x ps $.  $d y ph $.
    nfcdeq.1 $e |- NF ( x , ph ) $.
    nfcdeq.2 $e |- CondEq ( x = y -> ( ph <-> ps ) ) $.
    $( If we have a conditional equality proof, where ` ph ` is ` ph ( x ) `
       and ` ps ` is ` ph ( y ) ` , and ` ph ( x ) ` in fact does not have
       ` x ` free in it according to ` NF ` , then ` ph ( x ) <-> ph ( y ) `
       unconditionally.  This proves that ` NF ( x , ph ) ` is actually a
       not-free predicate.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    nfcdeq $p |- ( ph <-> ps ) $=
      ( cv wsbc nfri sbf nfd wb cdeqri sbie bitr3i ) AACDHIBACDACEJKABCDBCBCLJA
      BMCDGNOP $.
      $( [11-Aug-2016] $)
  $}

  ${
    $d x z B $.  $d y z A $.
    nfccdeq.1 $e |- NF_ ( x , A ) $.
    nfccdeq.2 $e |- CondEq ( x = y -> A = B ) $.
    $( Variation of ~ nfcdeq for classes.

       (Contributed by Mario Carneiro, 11-Aug-2016.) $)

    nfccdeq $p |- A = B $=
      ( vz cv wcel nfcri wceq equid cdeqth cdeqel nfcdeq eqriv ) GCDGHZCIQDIABA
      GCEJABQQCDQQKABGLMFNOP $.
      $( [11-Aug-2016] $)
  $}

  $( Let the computer know the theorems to look for to prove the metatheorem $)
  $( $j
    condequality 'wcdeq' from 'cdeqth';
    condcongruence 'cdeqnot' 'cdeqim' 'cdeqal1' 'cdeqal' 'cdeqcv' 'cdeqeq'
      'cdeqel' 'cdeqab1' 'cdeqab';
    notfree 'wnf' from 'nfcdeq';
    notfree 'wnfc' from 'nfccdeq';
  $)

The new keywords here are "condequality", which registers "CondEq" as a conditional equality, and then "condcongruence" for each of the primitive axioms. The existence of this definition is sufficient to prove, with the "notfree" invocation, that NF is a not-free predicate.

This definition is a little borderline, but the idea is that I want to offload as much of the work as possible into the .mm file, which is already set up to provide definitions and theorems. That's why it accepts subtrees only by way of definitions, and in order to specify them you have to make a new definition (whether or not you intend to use it significantly). The alternative would be something like condequality 'vx cv vy cv wceq wph wi', in which I give the tree explicitly, and then it reads it and looks for variables inside, to make a kind of "anonymous definition". This is just a little too magical for my taste, though.

Adding a new axiom to ZFC just because of inadequate definition checkers sends the very wrong message that ZFC itself is inadequate.

I think lying about what is a definition is a worse problem. Coq is (presumably) very nice to use, but when you hear about a bug in the foundation it rocks your whole understanding of the activity. *This is a bug in the axiomatization.* It is not a problem of inadequate definition checkers, in fact just the opposite: it was  the act of working on this more advanced and rigorous definition checker that revealed the bug, which is exactly what I want the definition checker to do.

While this may be a useful exercise, I don't think we should change to non-overloaded = and e. connectives for the standard set.mm.  Our present method is very convenient, and the various class theory proofs (Levy, T&Z, Quine) show that df-clab/cleq/clel are an eliminable ZFC extension, even if our present definition checking tools can't prove it.  They meet all of the things one expects of a definition:  any theorem using class theory, and all of its proof steps, can be unambiguously translated to an equivalent theorem and proof steps in pure ZFC language without class theory.  The purpose of class theory is simply human convenience, and it serves no mathematical purpose.

Actually, I'm not really suggesting we de-overload the = and e. of set.mm. In the ideal world, we get the best of everything: full confidence in the conservativity of definitions, while also reusing or overloading whatever we want. The trick is how to set it up so that we can have these, and that entails looking really closely at what we claim is a validly overloaded expression.

There's no limit to what you can do with this $j command style. The basic premise is: you come up with a semiformal proof along the lines "if X and Y are valid, then Z follows", then you annotate X and Y with a $j command, and then Z can be rigorously checked. I haven't tried overloading yet, but here's an attempt:

All our overloadings take the form of a certain expression which is conservative over one of its own special cases. For example, e.3 is conservative over e.2, but in set.mm that's saying that (wcel A B) is fully determined by the value at (wcel (cv x) A). We could write the subtree by means of a syntax theorem, although I find these just a little weird:

wcel2 $p wff x e. A $= vx cv cA wcel $.

From this we get the equivalence (wcel2 vx cA) = (wcel (cv vx) cA). Now for the overloading:

$( $j overload 'wcel2' in 'df-clel' justification 'justel'; $)

We pretend that the left side of df-clel uses a different symbol, and check all previous axioms to ensure that this A e. B thing has never appeared directly before (except for wcel itself), but always in the shape x e. A or a substitution of this. We also check the right side of df-clel this way.

For the justification, we use wcel2 to form a special case of df-clel:

df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.
justel $p |- ( x e. A <-> E. y ( y = x /\ y e. A ) ) $.

and now theorem just needs to be proven (and it should also appear before df-clel is introduced). Once we have this, df-clel becomes a 100% kosher definition. For another example, we consider df-cleq:

weq $a wff x = y $= vx cv vy cv wceq $.
${
  df-cleq.1 $e |- ( A. x ( x e. y <-> x e. z ) -> y = z ) $.

  justeq $p |- ( u = v <-> A. x ( x e. u <-> x e. v ) ) $.
  df-cleq $a |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $.

  $( $j overload 'weq' in 'df-cleq' justification 'justeq'; $)
$}

In this case, we want df-cleq to have a hypothesis, so let's say that the justification theorem gets the same hypothesis as the definition (although you have to be careful about what variable renames occur).

Each new keyword is associated with another page in defn.pdf, but the result is that we can do this kind of trickery and still have confidence in the results.

Once more, let me note that justel is not currently provable, so we need to have an axiom for it such as ax-14c. I'm not sure why this is such a surprise to you; x e. A is genuinely new primitive notation introduced in the class abstractions section, regardless of how you justify it. Obviously it's going to need an equality axiom, just like everything else in the language. For the right form of the hypothesis, you have to be careful since you can't quantify over classes, so a trick like df-cleq won't work here. I suggest:

 df-clel.1 $e |- ( y = z -> ( y e. B -> z e. B ) ) $.
 df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.

because df-clel can only be used to prove equality for the class B on the right.

Mario

[David A. Wheeler]

On Fri, 12 Aug 2016 00:31:28 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I've introduced a few new keywords for the $j statement, and a little
> section to make use of it. Rather than explain it I'll just use the
> existing comments.

Whew. My mind is exploding from the meta-meta-nature of this.

So let me step back. Metamath by itself proves theorems from axioms;
axioms, of course, are simply accepted without proof.
This discussion is about "$j" statements, along with at least one verifier of them,
so that certain assertions about the *axioms* can also be checked. Right?

It seems to me that these $j statements have similarities to
introspective operations in some programming languages.
Would any of those techniques in the other languages be helpful?
I'm speaking imprecisely because I honestly don't know.
It seems like this $j language basically exists to allow checked assertions
that certain properties of the axioms hold.

> This definition is a little borderline, but the idea is that I want to
> offload as much of the work as possible into the .mm file, which is already
> set up to provide definitions and theorems.

That makes sense.

> That's why it accepts subtrees
> only by way of definitions, and in order to specify them you have to make a
> new definition (whether or not you intend to use it significantly). The
> alternative would be something like condequality 'vx cv vy cv wceq wph wi',
> in which I give the tree explicitly, and then it reads it and looks for
> variables inside, to make a kind of "anonymous definition". This is just a
> little too magical for my taste, though.

I can see the argument both directions. It's little ugly to give the tree
explicitly, but then you don't create a highly-visible "CondEq" definition
that you don't intend to use directly. That said, since metamath in general
tries to be explicit, it would be consistent to have the explicit definitions
as you've done.

--- David A. Wheeler

[Mario Carneiro]

On Fri, Aug 12, 2016 at 6:59 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Fri, 12 Aug 2016 00:31:28 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I've introduced a few new keywords for the $j statement, and a little
> section to make use of it. Rather than explain it I'll just use the
> existing comments.

Whew.  My mind is exploding from the meta-meta-nature of this.

So let me step back.  Metamath by itself proves theorems from axioms;
axioms, of course, are simply accepted without proof.
This discussion is about "$j" statements, along with at least one verifier of them,
so that certain assertions about the *axioms* can also be checked. Right?

Yes, that's right. Once upon a time we accepted definitions the same as axioms, but this means that trusting a metamath proof means trusting hundreds of axioms, many of them obtuse. The original definition checker allows us to have more confidence that some of the axioms are not really axioms, so that we don't have to trust them in order to trust proofs that use them.

But in the original definition checker I made lots of references to named theorems or syntax, which I thought was inelegant, since it breaks the general nature of the tool. Most of this project has been investigating the question "what makes set.mm special?". In general metamath, there is no real distinction between set and wff, they are just two typecodes with some variables, but in FOL they are very different. Why is this? What particular axioms force this behavior to arise? As it stands, the forall is a binary function (set, wff) -> wff, but in FOL it's the completely different (set -> bool) -> bool, because of binding. What causes the forall to act like a binder? These are just a few of the questions that need answering.

 

It seems to me that these $j statements have similarities to
introspective operations in some programming languages.
Would any of those techniques in the other languages be helpful?
I'm speaking imprecisely because I honestly don't know.
It seems like this $j language basically exists to allow checked assertions
that certain properties of the axioms hold.

This would be very nice, but it goes quite a bit beyond the current capability of the system. This basically means expanding Metamath-in-Metamath to encompass all the $j rules and the proofs of correctness, i.e. formalizing defn.pdf. This is a reasonable project exactly because it is done in full generality. In the next stage, the verifier would read and understand the formalism, and translate chosen theorems into $j commands that can then be checked. At that point we really are using Metamath (or more precisely set.mm) as a metalanguage over some other metamath database (or possibly set.mm itself). *That* would be true introspection. But I should stop now before I get sidetracked trying to implement it. ;)

 

Mario

[Norman Megill]

On 8/12/16 12:31 AM, Mario Carneiro wrote:
> Once more, let me note that justel is not currently provable, so we need
> to have an axiom for it such as ax-14c. I'm not sure why this is such a
> surprise to you; x e. A is genuinely new primitive notation introduced
> in the class abstractions section, regardless of how you justify it.

I don't get why we need to prove justel without df-clel. There is an
implicit invisible function cv that takes in x and puts out a class
expression "cv(x)". This is made explicit in the mm solitaire applet,
where cv(x) must be explicit in the internal definition and is replaced
by a blank symbol on the screen. It is a just a special case of B e. A
where B is replaced with a compound class expression.

> Obviously it's going to need an equality axiom, just like everything
> else in the language. For the right form of the hypothesis, you have to
> be careful since you can't quantify over classes, so a trick like
> df-cleq won't work here.

We aren't quantifying over classes. We are quantifying x in the
invisible cv(x).

The algorithm for eliminating class expressions is unambiguous, and
every class expression can be eliminated with it. It has been proved
(on paper) by several authors using only FOL and ax-ext, There is no
mention of your additional axiom in those proofs. Are those proofs
wrong? What is an example of a theorem in class notation that would
lead to a contradiction or extend the language in a non-eliminable way?

Norm

[fl]

FL, you should find out what other axioms you would prefer in order to prove this - I couldn't find a source with your exact six axioms, so I'm not sure what it is supposed to look like.

The system looks like that. It is sound and complete. But your objection is serious.

[.] ph -> ps -> ( ( ph until ch ) -> ( ps until ch) ) is referenced as a theorem of the system.

But as you have noticed

it is definitely impossible to prove that. Then either it is proved at the metalogical level, or there

is something obscure in the logical framework. I'd like to buy a book on the subject. But it must be ordered in the USA.

A nightmare!

--

FL

[fl]

But as you have noticed

it is definitely impossible to prove that.

It is possible that it is impossible to prove that. I need to look at it thoroughly. Modal logic is diabolic.

--

FL

[Mario Carneiro]

On Fri, Aug 12, 2016 at 7:54 PM, Norman Megill <n...@alum.mit.edu> wrote:

On 8/12/16 12:31 AM, Mario Carneiro wrote:

Once more, let me note that justel is not currently provable, so we need
to have an axiom for it such as ax-14c. I'm not sure why this is such a
surprise to you; x e. A is genuinely new primitive notation introduced
in the class abstractions section, regardless of how you justify it.

I don't get why we need to prove justel without df-clel.   There is an implicit invisible function cv that takes in x and puts out a class expression "cv(x)".  This is made explicit in the mm solitaire applet, where cv(x) must be explicit in the internal definition and is replaced by a blank symbol on the screen.  It is a just a special case of B e. A where B is replaced with a compound class expression.

Right, this cv thing is why I've tried to be explicit about its uses, but trust that I am aware of where it comes up in my previous posts. As for "why we need to prove justel without df-clel", isn't that obvious? You can't justify a definition using the definition, that would be circular. When you say "it is just a special case of B e. A", that's exactly what overloading is all about: we start out with A e. B but only ever use it in the special case (x) e. (y), so no theorems about A e. B generally can be proven except tautologies like ( A e. B -> A e. B ). (These cases can be detected in principle, because this is not the most general form; a la MM solitaire, the same proof could be used to prove ( ph -> ph ) instead.)

We then "define A e. B" in df-clel, by which I mean we make the first use of general A e. B and introduce it in the manner of a definition. Even though A e. B was previously available, it was totally unconstrained except in the special case (x) e. (y). But there is an intermediate stage, after df-clab, when we are introducing "axioms of classes". This includes the definition of the constant "class", the syntax axioms "cab", "cv", and (in principle) the primitive x e. A (note there is no cv here). The definition df-clel is a definitional extension over x e. A, which is a conservative extension (but not a definitional extension) over the x e. y of predicate calculus.

In order to justify writing (x) e. A when we mean x e. A, we need a proof that these are the same; this is the justification proof and it cannot use the general definition A e. B (df-clel). There is nothing to prove when identifying x e. (y) with x e. y, because it is not a definitional extension; x e. A is (initially) totally unconstrained except for the axioms we already have for x e. (y), and the new axiom for x e. { y | ph }. The general case x e. A is left undefined, and indeed can be anything (we treat the value of this expression for varying x as the meaning of the class A). But A e. B is definitional over x e. A, and justel concerns the proof that this is in fact a definitional extension.

Obviously it's going to need an equality axiom, just like everything
else in the language. For the right form of the hypothesis, you have to
be careful since you can't quantify over classes, so a trick like
df-cleq won't work here.

We aren't quantifying over classes.  We are quantifying x in the invisible cv(x).

I mean that from the hypothesis |- ( x = y -> ( x e. A -> y e. A ) ) you don't know that the expression is true for all A, but you do know it is true for all x,y (because of chvar). Or at least, you would if substitution worked; but since we are missing this axiom you would have problems changing this into |- ( z = w -> ( z e. A -> w e. A ) ) anyway.

The algorithm for eliminating class expressions is unambiguous, and every class expression can be eliminated with it.  It has been proved (on paper) by several authors using only FOL and ax-ext,  There is no mention of your additional axiom in those proofs.  Are those proofs wrong?

Not wrong, incomplete. They use a different formalism: Metamath is not FOL + ax-ext, although it acts fairly similar in places. Metamath is different in that it gives you variables of type class, which are assumed not to be present in the proofs you are talking about.

In metamath, every class expression (not counting definitions) is of one of three types: (cv x) for some set variable x, { x | ph } for some variables x,ph; or A where A is a class variable. You seem to not recognize the existence of the third possibility, and it's not a possibility in those proofs.

 

What is an example of a theorem in class notation that would lead to a contradiction or extend the language in a non-eliminable way?

ax-14c itself: |- ( x = y -> ( x e. A <-> y e. A ) ) is not provable in pred calc + df-clab. The expression "x e. A" is not eliminable. You can try replacing it with x e. { y | y e. A }, but you still have an embedded y e. A, and there's no way to get rid of it.

Yes, it is a conservative extension, but I'm beginning to realize that that's not as useful of a notion as I originally thought: anything is a conservative extension of the empty language. Conservative extensions that are not definitional can certainly make the language "more powerful", but only within the new language. What we want is a definitional extension, which is an extension in which all expressions in the new language expand to expressions in the original language. "x e. A" is one of these non-definitional extensions.

When I said that "x e. A is (initially) totally unconstrained", I meant it: there are no axioms concerning it at all. When we introduce elementhood (x e. y) in predicate calculus, it is *almost* totally unconstrained, but at least we have an equality axiom, namely ax-13 and ax-14. Here we also want equality to be provable, and on the right that's easy, because ( A = B -> ( x e. A <-> x e. B ) ) follows directly from the definition (since class equality is as yet undefined we can do that). On the left, there's no such luck; we are forced to have a new axiom for it.

[Stefan O'Rear]

On Sat, Aug 13, 2016 at 10:13 AM, Mario Carneiro <di....@gmail.com> wrote:
> ax-14c itself: |- ( x = y -> ( x e. A <-> y e. A ) ) is not provable in pred
> calc + df-clab. The expression "x e. A" is not eliminable. You can try
> replacing it with x e. { y | y e. A }, but you still have an embedded y e.
> A, and there's no way to get rid of it.

At the FOL object level, ax-14c is not an axiom, it's a metatheorem.
It can be proven for cv using ax-14, it can be proven for abstractions
after unwinding df-clab, and it can be proven for defined constants
similarly.

-sorear

[Mario Carneiro]

Right. This requires that the object level not have any class variables in it. Obvious, I know, and of course true for all the FOL proofs, but this is what's not true for metamath; we have to support also metavariables that drop out of the blue. It's effectively the same situation as for class constants that have no definition. Norm has been calling this "metalogical completeness", in contrast to "logical completeness" in which the metavariable case doesn't happen.

Mario

[Stefan O'Rear]

On Sat, Aug 13, 2016 at 12:11 PM, Mario Carneiro <di....@gmail.com> wrote:
> On Sat, Aug 13, 2016 at 2:52 PM, Stefan O'Rear <sor...@gmail.com> wrote:
>> At the FOL object level, ax-14c is not an axiom, it's a metatheorem.
>> It can be proven for cv using ax-14, it can be proven for abstractions
>> after unwinding df-clab, and it can be proven for defined constants
>> similarly.
>
>
> Right. This requires that the object level not have any class variables in
> it. Obvious, I know, and of course true for all the FOL proofs, but this is
> what's not true for metamath; we have to support also metavariables that

I assume you're talking about dummy variables in proofs here. Dummy
variables in completed are very different from variables that exist
inside a proof because they can be substituted. If you have a
contradiction, you can have the same contradiction without wff or
class metavars by replacing all of them with F. and (/) respectively.
So the metatheorem handling of ax-14c can treat all class metavars as
(/).

> drop out of the blue. It's effectively the same situation as for class
> constants that have no definition. Norm has been calling this "metalogical
> completeness", in contrast to "logical completeness" in which the
> metavariable case doesn't happen.

As you have noticed, ax-14c or something equivalent, like df-clel, is
needed for metalogical completeness in the proof theory.

-sorear

[Mario Carneiro]

On Sat, Aug 13, 2016 at 3:26 PM, Stefan O'Rear <sor...@gmail.com> wrote:

On Sat, Aug 13, 2016 at 12:11 PM, Mario Carneiro <di....@gmail.com> wrote:
> On Sat, Aug 13, 2016 at 2:52 PM, Stefan O'Rear <sor...@gmail.com> wrote:
>> At the FOL object level, ax-14c is not an axiom, it's a metatheorem.
>> It can be proven for cv using ax-14, it can be proven for abstractions
>> after unwinding df-clab, and it can be proven for defined constants
>> similarly.
>
>
> Right. This requires that the object level not have any class variables in
> it. Obvious, I know, and of course true for all the FOL proofs, but this is
> what's not true for metamath; we have to support also metavariables that

I assume you're talking about dummy variables in proofs here.

No, I mean free class variables, i.e. the goal would be to prove $p |- ( x = y -> ( x e. A <-> y e. A ) ), and since the "A"  is exposed here, you can't replace it with a substitution instance.

 

  Dummy
variables in completed are very different from variables that exist
inside a proof because they can be substituted.  If you have a
contradiction, you can have the same contradiction without wff or
class metavars by replacing all of them with F. and (/) respectively.

This is true, and is the reason why the class extension generally is a conservative, but not definitional, extension.
 

So the metatheorem handling of ax-14c can treat all class metavars as
(/).

This isn't generally valid as a proof technique in Metamath, because it doesn't have to ever "bottom out". For an extreme example, consider the "set" typecode. There are no constructors for this type, so you might think that there are no set vars at all, but of course there are, we use them all the time. Whenever we substitute one of these, there's always another variable in the substitution, so we never seem to get anywhere with the substitutions. The exact same situation happens with class, the only difference is that we also have the option of using the constructors. But you can have some class variable A, which is replaced with B, which is replaced with C, and you're waiting to find out what expression is being denoted here but the answer never comes. That's why you have to treat variables themselves as possible elements of the object logic.

Mario

[Norman Megill]

I think ax-14c will be puzzling to a lot of people. I don't think the
technical subtleties that make the Metamath representation different
"under the hood" from what textbooks are doing "under the hood" is going
to be of interest to most readers, who just want to see the "math",
whose notation is essentially identical in set.mm and textbooks.

Rather than adding ax-14c, I would much prefer that df-clab, df-cleq,
and df-clel become axioms. Since this is done in Levy's book, at least
it is not without precedent. We just have to make it clear that they
are eliminable, conservative extensions of ZFC and aren't true axioms,
but the proof of conservation is outside of the scope of what can be
done within the Metamath framework.

Am I correct that this would satisfy your definitional checking
requirements?

As for df-sbc, we can introduce a new notation rather than calling it an
axiom. Or we could change the notation for df-sb instead. I'm open to
suggestions.



On 8/11/16 3:16 AM, Mario Carneiro wrote:
> Here's the idea: set.mm <http://set.mm> is an axiomatization of ZFC

> *with classes*. That includes the fact that there are three typecodes,
> and enough axioms to make them all play well together. The right way to
> talk about conservative extension here from ZFC without classes is to
> have a separate spinoff database, in which "class" never makes an
> appearance, and then rigorously define the mapping from each primitive

> of standard set.mm <http://set.mm> to the reduced version. This would be

> backed up with an informal proof and/or a computer verification. As it
> is it's a bit of a muddled mess piecing out what is conservative and
> what isn't, and the df-* axioms aren't making it any better. I would
> much prefer, now that definition checking is on solid ground, for *all*
> our definitions to be definitions, *no exceptions* (to paraphrase a
> recent youtube video).
>
> Additionally, I'm pretty sure that you will end up with *fewer* axioms
> (counting df-clel and friends as axioms) if you use classes through and
> through.

I think it would be a major mistake to mix up pure ZFC and class theory
at the axiomatic level, even if it means fewer axioms. It would
certainly be very confusing to beginners. We should be able to discard
df-clab, df-cleq, df-clel (and all that depends on them - most of
set.mm, to be sure) and be left with the $a's of pure ZFC set theory in
the primitive language. It will still be contaminated with wceq and
wcel, but that is easy to eliminate if the class stuff is stripped out.

Having to maintain two set.mm's with and without classes would be a big
inconvenience. We just need to ensure that in principle we can break
out a pure ZFC set theory without classes.

My goal has always been to show pure ZFC set theory first in its native
language (which is very simple) and then later introduce the
complication of classes as a definitional mechanism for the benefit of
humans. It should be made clear that classes are not part of ZFC
proper, and that there is an algorithm for translating class notation
into the primitive language of ZFC. Ideally, we'd present all $a's of
ZFC first in set.mm before getting into classes (as was done a long time
ago), although we now introduce the ZFC $a's as the need arises, as a
practical means to prevent unnecessary uses of stronger axioms. In the
mmset.html presentation we do introduce them all at once, independent of
class theory

Norm

[Mario Carneiro]

On Tue, Aug 23, 2016 at 2:49 PM, Norman Megill <n...@alum.mit.edu> wrote:

I think ax-14c will be puzzling to a lot of people.  I don't think the technical subtleties that make the Metamath representation different "under the hood" from what textbooks are doing "under the hood" is going to be of interest to most readers, who just want to see the "math", whose notation is essentially identical in set.mm and textbooks.

Rather than adding ax-14c, I would much prefer that df-clab, df-cleq, and df-clel become axioms.  Since this is done in Levy's book, at least it is not without precedent.  We just have to make it clear that they are eliminable, conservative extensions of ZFC and aren't true axioms, but the proof of conservation is outside of the scope of what can be done within the Metamath framework.

Am I correct that this would satisfy your definitional checking requirements?

As for df-sbc, we can introduce a new notation rather than calling it an axiom.  Or we could change the notation for df-sb instead.  I'm open to suggestions.

Yes, this would save a lot of headaches with overloading as well. It's cheating a bit, but it's certainly easier to justify than the alternative.

If this leaves df-sb as the only overloaded definition, I would suggest using a new notation for df-sb only. It never gets used anyway once the class version is introduced.

 

I think it would be a major mistake to mix up pure ZFC and class theory at the axiomatic level, even if it means fewer axioms.  It would certainly be very confusing to beginners.  We should be able to discard df-clab, df-cleq, df-clel (and all that depends on them - most of set.mm, to be sure) and be left with the $a's of pure ZFC set theory in the primitive language.  It will still be contaminated with wceq and wcel, but that is easy to eliminate if the class stuff is stripped out.

The paper napkin proof in my head says this should work. Basically, after removing the class axioms, you replace (wceq (cv x) (cv y)) with (weq x y) and similarly for wcel; then you can remove wceq, wcel, cv, and the typecode class. This latter removal should only cause the loss of theorems containing a class metavariable, and since there are no class axioms these will never appear in "most general" theorem proofs. (In other words, the extension is conservative.)

Mario