distinct variables: df-uni.html vs eluni.html

616 views
Skip to first unread message

Mázsa Péter

unread,
Dec 17, 2012, 10:40:14 AM12/17/12
to meta...@googlegroups.com
First of all, thank you all, and especially Norman, for Metamath.

I'm not a mathematician: I'm sure it is my fault but I can't figure it
out how this works - I hope some of you are willing to help me:

1. In df-uni.html, where x and A are distinct, it is not possible that
x=A and so it is not possible that x e. y e. x=A either, where e.: "is
an element of". (In this case a general en3lp.html- and
elirr.html-like not(A e. B e. A) theorem may exist as well.)

2. In eluni.html it is not excluded by distinct variable groups that
A=B and so it is possible that A e. x e. B=A as well.

(Similarly, e.g., with df-int.html and elint.html)

Why 1. and 2. are not in contradiction?

Thank you:
Peter

Jason Orendorff

unread,
Dec 17, 2012, 1:27:22 PM12/17/12
to Metamath Mailing List
On Mon, Dec 17, 2012 at 9:40 AM, Mázsa Péter <pe...@mazsa.com> wrote:
1. In df-uni.html, where x and A are distinct, it is not possible that
x=A and so it is not possible that x e. y e. x=A either, where e.: "is
an element of". (In this case a general en3lp.html- and
elirr.html-like not(A e. B e. A) theorem may exist as well.)

2. In eluni.html it is not excluded by distinct variable groups that
A=B and so it is possible that A e. x e. B=A as well.

(Similarly, e.g., with df-int.html and elint.html)

Why 1. and 2. are not in contradiction?

You are right that eluni implies this:
    A ∈ ∪A ↔ ∃x(A ∈ x ∧ x ∈ A)

However all this says is that
    A ∈ ∪A
is true if and only if
    ∃x(A ∈ x ∧ x ∈ A)
is true.

It does not say that either one is possible. Perhaps both are false for all A.

On the other hand, df-uni doesn't say by itself that (A ∈ x ∧ x ∈ A) is impossible! In fact, all df-uni does is provide a nice convenient notation “∪A” for certain sets already fully defined by other axioms; it doesn't make any statement true or false except those that contain this new symbol ∪.

-j

Andrew Salmon

unread,
Dec 17, 2012, 1:24:19 PM12/17/12
to meta...@googlegroups.com
Hello Peter,

> 1. In df-uni.html, where x and A are distinct, it is not possible that
> x=A and so it is not possible that x e. y e. x=A either, where e.: "is
> an element of". (In this case a general en3lp.html- and
> elirr.html-like not(A e. B e. A) theorem may exist as well.)

Distinct variables mean, roughly, that x is not a free variable in A.
So we can't set A = { x }, for example.

They are important so that we can say things like A. x x e. A -> _V =
A. But A. x x e. { x } but _V =/= { x }. This does not produce
contradiction because x and { x } are not distinct.

Thanks,

Andrew

Mázsa Péter

unread,
Dec 19, 2012, 8:22:57 AM12/19/12
to meta...@googlegroups.com
Dear Andrew, Jason and group,

thank you for your answers: they clarified some concepts and helped me
to move out from a standstill (n2lp --> zfregfr.html --> zfreg2.html
--> non-well founded sets??, vs fixed points).

I think this small community is one of the most important around (cf.
e.g. "Math is the foundation of all human thought, and set theory --
countable, uncountable, etc. -- that's the foundation of math. So even
if this class was about Sanskrit literature, it should still probably
start with set theory" Scott Aaronson).
Please keep up the good work.

P.

Raph Levien

unread,
Dec 19, 2012, 1:08:26 AM12/19/12
to meta...@googlegroups.com
I'll try to explain a bit more, especially the differences between the way Metamath and Ghilbert handles this.

The "distinct variable" conditions in Metamath are at the meta-logical level. In particular, they state that all valid instantiations of the theorem schema (or axiom schema) have variables that are distinct. Unlike the "distinct" predicate in SMT-LIB (for example), it is not saying that the values are distinct.

It is traditional in logic to assume that all variables are "fresh", that is to say that variables with different names are distinct. Most statements rely on this condition. For one special example, ∃x x≠y would generally be considered a theorem (in any universe with more than one value). In Metamath, it is a theorem whenever there is a distinct variable condition between x and y. (In contexts where there is no such distinct variable condition, it can be used as a "distinctor" - it has the value true when x and y are distinct variables, and false otherwise. This leads to fairly interesting byways where you can get surprisingly far with no concept of variable freeness or distinctness in the metalogic at all - see http://us.metamath.org/mpegif/mmzfcnd.html - but set.mm relies on the distinct variable conditions).

To say that a variable is distinct from a term (say x and A) means that it does not appear syntactically in the term at all. This is a stronger condition than what Andrew said above. For example, x is not distinct from ∀x x=x because x occurs syntactically in that term.

Metamath does not have a metalogical way to express "x does not appear free in A". Instead, when needed, this concept is expressed in the logic. For example, in predicate logic, ɸ→∀xɸ expresses "x does not effectively appear free in ɸ". The "effectively" bit means that there might be other ways to prove this, if the value of ɸ does not depend on x in any way. For example, it is true for x=x (see http://us.metamath.org/mpegif/hbequid2.html for the proof), even though in standard logic you would say that x does appear free in this term.

Moving from a variable not appearing (syntactically) in a term to a statement that the variable is not free in the term is usually axiom in the logic - in set.mm, it is ax-17, but there are other ways it could be done. For example, in some form of the lambda calculus, it might be a statement that λx.A is the constant function.

In theory, the ability to express theorems without the usual freshness constraints gives Metamath more expressive power, in that you can have effectively two (or more) theorems in one, depending on whether the variables are distinct or not. An example is http://us.metamath.org/mpegif/alcom.html , which proves ∀x∀yɸ ↔ ∀y∀xɸ. As it happens, this theorem is also true if x and y are not distinct, i.e. ∀x∀xɸ ↔ ∀x∀xɸ is also a theorem (although not a particularly deep one, in this case). As I understand it, Norm has made an effort to use as few distinct variable conditions as possible, when it is possible to omit them. Even so, I did an empirical study a few years back, and found only a handful of examples where this extra expressiveness was actually exploited.

Ghilbert uses a somewhat different approach, which is a bit closer to standard logic and I think more intuitive (although it is arguably at least as complex, and quite subtle when it gets into definitions). In Ghilbert, the concept of x appearing free in a term is in the metalogic, using pretty much the standard meaning from logic. So, in Ghilbert, a constraint "x not free in ɸ" would be satisfied by ∀x x=x (or ∀x anything) but not x=x. Also, in Ghilbert, any two binding variables are automatically considered distinct, and there's no direct way to express, for example, the version of alcom with the two variables "smooshed" together (of course, this particular theorem can simply be proved another way, for example as an instance of biid).

So this is one of the sticking points in doing the Metamath to Ghilbert translation. In theory, to do a complete mechanical translation, I'd need to replicate theorems into versions with and without the distinct variable conditions, and apply the appropriate version when needed. However, since the overwhelming majority of cases work the same as assuming variables are fresh, I'm most inclined to just assume that and then fix up the few cases that break.

One other motivation for doing things differently in Ghilbert than Metamath is that I think it will be much easier to translate theorems from Ghilbert into other frameworks (I've done a little work on HOL in particular) mechanically. But even if it weren't for this, I think the more traditional free variable approach is easier to understand, and easier to work with, than the distinct variable approach in Metamath. For one, while many of the Margaris 19.xx theorems have "v" variants in set.mm, for cases where the variable is syntactically distinct, most of these variants are not needed in Ghilbert.

A similar discussion came up a few years ago on AsteroidMeta:
Looking back, a lot of those discussions are fascinating. It'd be great if they were easier for new Metamath and Ghilbert users to find.

Hope this informs,

Raph




--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To post to this group, send email to meta...@googlegroups.com.
To unsubscribe from this group, send email to metamath+u...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/metamath?hl=en.


Reply all
Reply to author
Forward
0 new messages