A new axiom

[Benoit]

Hi all,

I propose introducing the following new axiom (a syntactic rule of inference) to set.mm, in Subsection 2.1.2:

${
$(
A syntactic rule of inference.
If there exists a set which is equal to the class A (in the sense that they have the same elements, see df-cleq), then A itself is a set.
$)
ax-set.1 $e |- E. x x = A $.
ax-set $a set A $.
$}

This would allow to prove for instance that { x } is a set, as well as { x e. y | ph } and ( F ` x ) and many other expressions.

Currently, since for instance { x } is not known to be a set, but only a class, one has to define many constructions for arbitrary classes in order to be able to simply write { { x } } or ( F ` { x } ) . So one has to define { A } , which is meaningless for proper classes, and similarly ( F ` A ) . Similarly for many other constructions.

With this new axiom, set.mm wouldn't be "plagued" with so many class variables, and class variables would appear only where necessary. This would also dramatically reduce the number of premises of the form A e. _V : one would simply use a set variable instead of A in the conclusion.

Any thoughts ?

--
Benoit

[Norman Megill]

No, because we can't quantify over class terms.  Otherwise we can derive a contradiction.  Example:  from a9e, conclude E. 1 1 = 0.  From id, 1 = 0 -> 1 = 0, then use exlimiv to get E. 1 1 = 0 -> 1 = 0.  ax-mp gives 1 = 0.

Norm

[Mario Carneiro]

I've mentioned more about why the axiom as stated doesn't work in another post, but here let me talk about how to have an actual syntactic typecode for sets. If the current "set" typecode was renamed to "var", then we could call this typecode "set", but for now let's call it "Set" for disambiguation. Here is an axiomatization of it:

$c Set $.
sA $f Set -A $.
sB $f Set -B $.
sC $f Set -C $.

$( A set variable is a set, and a set expression is a class. $)

sv $a Set x $.
cs $a class -A $.

$( A set expression is provably a set. There is no converse to this axiom,

   although you can use a set variable for this purpose, i.e. use isseti,

   since a set variable is also a set expression. $)

sset $a |- -A e. _V $.

$( Axioms of set theory $)

snul $a Set (/) $.

srep $a Set ( x e. -A |-> B ) $. $( Not quite replacement, but works with our expression ran ( x e. A |-> B ) for the replacement operation. $)

ssep $a Set { x e. -A | ph } $. $( I don't think this follows from srep the way axsep follows from ax-rep $)

spow $a Set ~P -A $.

sun $a Set U. -A $.

som $a Set om $.

spr $a Set { -A , -B } $.

To be useful, this scheme must also have a mechanism for introducing definitions conservatively (this is especially important because "Set A" makes an unconditional sethood assertion). The rule is easy, though: an axiom

sthing $a Set Thing x A -B $.

df-thing $a |- Thing x A -B = expr $.

is admissible if "Set expr" is derivable (i.e. the syntax derivation looks like wceq (cs (sthing ...)) (cs ..)), and it otherwise follows the rules for class definability (i.e. no free variables on the right that don't appear on the left). This allows for the definability of set-respecting operations like { -A }, dom -A, ran -A, <. -A , -B >. , ( iota x ph ), etc. It is conceivable that there are additional set constructors which are sets for non-obvious reasons, like df-har, but usually in these cases there is another way to write the expression that is obviously a set but not obviously the same as the original expression, so the proof work is pushed into the equality instead.

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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Benoit]

Yes, that's closer to what I had in mind (though I don't know why you keep changing threads!). I'd rather use x, A, _A for var, set, class respectively (or maybe, v_i (for integer i ) , x , A respectively).

Actually, I had thought of still introducing all things as classes, and then proving they are sets with the inference ax-set of my initial post. So the ZF axioms would still have the expressions they currently have, and ax-set would allow to deduce the versions you wrote.

--
Benoit

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

[Mario Carneiro]

On Fri, Oct 6, 2017 at 4:40 PM, Benoit <benoit...@gmail.com> wrote:

Yes, that's closer to what I had in mind (though I don't know why you keep changing threads!).

I was going to respond the set -> var stuff in this thread, but they are somewhat distinct proposals.

 

I'd rather use x, A, _A for var, set, class respectively (or maybe, v_i (for integer i ) , x , A respectively).

Actually, I had thought of still introducing all things as classes, and then proving they are sets with the inference ax-set of my initial post. So the ZF axioms would still have the expressions they currently have, and ax-set would allow to deduce the versions you wrote.

You will notice that there is no analogue of ax-set in this axiomatization. It is possible to have the axiom

ax-set.1 $e |- A e. _V $.

ax-set $a Set A $.

 

but there is a good reason to avoid it: it would make Set a logical typecode, which would make it difficult to also be a variable typecode (i.e. to have variables -A of type Set). To clarify: a logical typecode is one for which there are axioms that have hypotheses or disjoint variable conditions. A variable typecode is one which contains a $f axiom. Typecodes which are both are problematic, because logical typecodes are generally undecidable (because they depend on whether a certain theorem is derivable), while we want variable typecodes to be automatically proven by a CFG parser (which only works if the typecode is non-logical).

The typecode Set as I've described it consists of expressions that are *manifestly* a set, because they are formed from operations that are always sets. It is not possible to *prove* that an expression is a Set (in the sense of deducing a |- A e. _V type proof), it is either obviously a Set or not at all, which is why the computer can automatically derive such proofs.

Mario

[Benoit]

It is possible to have the axiom

ax-set.1 $e |- A e. _V $.

ax-set $a Set A $.

 

but there is a good reason to avoid it: it would make Set a logical typecode, which would make it difficult to also be a variable typecode (i.e. to have variables -A of type Set). To clarify: a logical typecode is one for which there are axioms that have hypotheses or disjoint variable conditions. A variable typecode is one which contains a $f axiom. Typecodes which are both are problematic, because logical typecodes are generally undecidable (because they depend on whether a certain theorem is derivable), while we want variable typecodes to be automatically proven by a CFG parser (which only works if the typecode is non-logical).

I agree with everything here (and thanks for putting clear words on my vague ideas), but why do you say "we want"? Is it simply for convenience when proving things? I have experimented a bit before proposing ax-set, and when proving things, the commmand

MM> improve all

was indeed not sufficient to complete the proof, even when all logical steps were completed: I had to do

MM> show new_proof /all

and then, assign ax-set to the steps starting with "set..." This seemed manageable with the very short proofs I tried, but I can't tell whether this would turn out to complicate things too much with later proofs.

My reason for doing this was that I felt that introducing things as sets (instead of classes) could be dangerous, but maybe your paragraph above about "sthing/df-thing" deals with that question. I'll have to think about it.

--

Benoît

[Mario Carneiro]

On Fri, Oct 6, 2017 at 7:54 PM, Benoit <benoit...@gmail.com> wrote:

It is possible to have the axiom

ax-set.1 $e |- A e. _V $.

ax-set $a Set A $.

 

but there is a good reason to avoid it: it would make Set a logical typecode, which would make it difficult to also be a variable typecode (i.e. to have variables -A of type Set). To clarify: a logical typecode is one for which there are axioms that have hypotheses or disjoint variable conditions. A variable typecode is one which contains a $f axiom. Typecodes which are both are problematic, because logical typecodes are generally undecidable (because they depend on whether a certain theorem is derivable), while we want variable typecodes to be automatically proven by a CFG parser (which only works if the typecode is non-logical).

I agree with everything here (and thanks for putting clear words on my vague ideas), but why do you say "we want"? Is it simply for convenience when proving things? I have experimented a bit before proposing ax-set, and when proving things, the commmand

MM> improve all

was indeed not sufficient to complete the proof, even when all logical steps were completed: I had to do

MM> show new_proof /all

and then, assign ax-set to the steps starting with "set..." This seemed manageable with the very short proofs I tried, but I can't tell whether this would turn out to complicate things too much with later proofs.

Not all proof assistants handle this situation gracefully, because it is an unspoken convention that variable typing should be context free and decidable. In particular, mmj2 will not like this, and I'm not even sure what it would do. It hides syntax proofs (with variable typecodes), and does all the proving of this stuff itself (and calls it parsing). If a variable typing condition became undecidable, then it would probably just fail to parse somehow, and not give you any opportunity to prove it yourself. By the way, "Inacc e. _V" is an example of a statement that is independent of ZFC. If sethood was decidable, it should also be complete, so these examples wouldn't exist.

I didn't give any axioms that correspond to ax-ac, but a (somewhat contrived) example of a definable set whose sethood depends on AC is the intersection of all choice functions on a given set X. This is one instance where you can fix it by the trick I mentioned, giving a different description that is obviously a set but not obviously the same: by replacing I^I A by ( |^| A i^i U. A ).

I should probably reiterate that I have no intention of actually implementing or endorsing the implementation of these things in set.mm, but I want to draw a good picture of what it would look like if we took this route.

 

My reason for doing this was that I felt that introducing things as sets (instead of classes) could be dangerous, but maybe your paragraph above about "sthing/df-thing" deals with that question. I'll have to think about it.

Another approach is to have a different equality for sets, wff -A = -B, so that you can't introduce a set except via another set construction. (This equality is really only for definition introduction, but we usually do double duty with the logical equality of the type, i.e. <-> or = .) But just as with equality between set variables now, we prefer to have just one equality relation rather than several, and use coercions on each side (cs or cv) to denote these specialized equalities, and cut down on the number of primitives.

Mario

[Benoit]

Not all proof assistants handle this situation gracefully, because it is an unspoken convention that variable typing should be context free and decidable. In particular, mmj2 will not like this, and I'm not even sure what it would do. It hides syntax proofs (with variable typecodes), and does all the proving of this stuff itself (and calls it parsing). If a variable typing condition became undecidable, then it would probably just fail to parse somehow, and not give you any opportunity to prove it yourself. By the way, "Inacc e. _V" is an example of a statement that is independent of ZFC. If sethood was decidable, it should also be complete, so these examples wouldn't exist.

Indeed, mmj2 returns

E-GR-0031 Syntax Axiom, Label = ax-set, has Logical Hypothesis ($e) in scope.

Can't we just say "well, types are undecidable, that's life" and carry on (not in set.mm, but in general) ? I mean: is it really unreasonable, or do there exist other systems for formal proofs that adopt this stance?