501 views

Skip to first unread message

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

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

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

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

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

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

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.

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.

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

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:

http://wiki.planetmath.org/cgi-bin/wiki.pl/Distinctors_vs_binders

http://wiki.planetmath.org/cgi-bin/wiki.pl/Principal_instances_of_metatheorems

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

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

Search

Clear search

Close search

Google apps

Main menu