[mizar] Re: Urelements?

[Jesse Alama <jesse.alama@gmail.com>]

trybulec@math.uwb.edu.pl writes:

> I would like to start with Polish "Nie przesadzajmy, jak mawiał leniwy
> ogrodnik", I do not know how to translate it. I wonder what Google
> does with it.

Something funny:

  Do not exaggerate, as he would say lazy gardener.

> It seems that we exaggerated with the statement that everything is a set.
> Actually numbers and structures behave rather like urelements (I am
> aware  that
> elements of structures are supposed to be urelements, not the
> structures themselves).

I don't entirely see the motivation for rejecting the idea that
everything is a set.

  2 + 2 is set;

seems valid to me.  Of course, my acceptance of it as "valid" is
somewhat biased, since I'm so accustomed to working in the Mizar/set
theory world for so long.  That is a defensible point of view.  There
is a definition of 2 as the von Neumann ordinal {0,1}, which is a set.
There are of course acceptable developments of set theory using
urelements, but what happens to statements such as

  2 + 2 is set;

and 

  2 + 2 is non set

if the urelement approach is adopted?

As for structures, the status quo seems to be that structures are in
fact sets, but we don't know any of their elements (or, at least no
membership statement is obvious for the Mizar checker) and thus
(accepting extensionality as globally valid) we don't know their
identities:

  {} in 1-sorted (# {} #)
  ::>                   *4
  ::> 4: This inference is not accepted

  not {} in 1-sorted (# {} #)
  ::>                       *4
  ::> 4: This inference is not accepted

  1-sorted (# 1 #) = 1-sorted (# 2 #);
  ::>                               *4

This seems fine to me as an approximation of the idea that they are
urelements.  A stricter approach would be to say reject as malformed
a membership statement whose right-hand side is a structure:

  {} in 1-sorted (# {} #)
  ::> *143,321 
  ::> 143: No implicit qualification
  ::> 321: Predicate symbol or "is" expected

Is that what is being proposed?

> In old Mizar the root type (and mode) was 'Any'. The type 'set' was a
> subtype of 'Any', the first axiom in TARSKI said that 'everything is a
> set'. One of the reason was that we planned to develop other
> repositories based e.g. on arithmetics, in which probably the first
> axiom would be 'everything is a natural number'. Then we decided that
> it is enough trouble with one MML, and keeping two different types
> with the same denotation is useless.
>
> Recently Artur started to experiment with definitional expansion of
> atomic sentences in the Inference Checker (CHECKER in the Mizar
> jargon) and the results are disgusting. Verifying some articles
> becomes longer by more than two orders. One of the reason was the lack
> of the type discipline. If e.g. 'x <> y' is among premises the poor
> thing will append to premises both 'not x c= y' and 'not y c= x' even
> when x and y are real numbers and such inclusions are (almost)
> meaningless.

I don't understand fully Artur's experiment.  Are things already slow,
or do they become slower when something is done (or not done)?

Anyway, why not weed out such inferences when

  requirements NUMERALS, REAL

are present in the environment?  Or perhaps add heuristics to CHECKER
to disprefer using such inclusions statements when the environment
gives numbers their standard meanings.  I think keeping the semantics
of the MML unchanged but improving the performance of CHECKER is
laudable.

> Therefore it is necessary to recover the old root type, under the new
> name 'element'. When identifying 'Any' and 'set' was easy, going back
> is a little bit harder. The first obvious step was done (by Czeslaw
> and Artur):
>
> i. in HIDDEN the mode 'element' is introduced and it is the mother
> type of the mode 'set'. The equality is introduced for elements, but
> the membership needs the second argument to be a set.
> ii. default types for numerals and structures are put to 'set' (temporarily)
> iii. when in the functor or mode definition qualification was empty,
> it was by default set, it was necessary, again for a while, to insert
> the qualification '-> set'.
>
> We should now discuss what should be a set, and what should
> not. E.g. ordered pairs are probably elements, not sets?

Of course, ordered pairs are sets (and robustly so: one can choose
from various notions of "ordered pair" and still get the same
conclusion).

Do we really want to try to demarcate such a line in the mathematical
universe?

To the extent that I appreciate your question, it seems that you're
proposing a rather major change to the whole MML.  If ordered pairs
are no longer sets, then I have to wonder in what sense the MML would
any longer be a body of knowledge based on set theory.

I see many important disadvantages with the current proposal:

* throwing out the idea that everything is a set throws out some of
  the conceptual clarity of developing everything from the axioms of
  set theory.  Of course, this doesn't really matter for virtually all
  of mathematics.  But the *existence* of a foundation, spelled out in
  the MML, is important.

* Are we prepared for the natural question from users: "if it's not a
  set, then what is it?  Are you saying there's no definition, or no
  properties, for the things that are elements-but-not-sets?"  Much
  clearer in my mind is to stick with the dogma that everything is a
  set.

* calling (almost) everything "element" when we used to say "set"
  would make the MML uglier.

* How do deal with the fact that real numbers are Dedekind cuts, which
  are...sets?  Is a real number a set, or isn't it?  (I'm not
  *commited* to this, in the sense that I am willing to stand behind a
  judgment about its truth; I don't think there's a fact of the matter
  about it, if you want my opinion.  However, I am *invested* in this
  view, as are lots of other mathematicians.)

* Such a change (if I understand correctly the full consequences of
  it) would make proof analysis harder.  If someone wants to study the
  MML, one natural question is: how are real numbers defined, how does
  the proof go, and what set theoretic principles are used where?
  Proof analysis for anything that is about numbers (directly or
  indirectly) would get cut off.

* Structures are another matter.  I don't see the problem with viewing
  them as "urelements" in an 'epistemic' sense (I don't know what
  their elements are, nor does the Mizar checker).

Please correct me if I'm wrong.

Jesse

--
Jesse Alama
http://centria.di.fct.unl.pt/~alama/