User talk:Asalmon

Links to other pages

Some interesting results and a good start to establishing class theory.

However, a couple of things:

a) Please try to link to existing pages wherever possible. A case in point is Definition:Epsilon Relation which I looked at puzzled for a while till I realised that $\in$ means "is an element of".

b) Also, every page needs to be assigned to at least one category.

c) Certain statements are immediate consequences of the definition, and (particularly if one is completely familiar with the subject matter) it is tempting to just add them on the definition page, perhaps with some words along the lines of "this obviously follows". However, one of the purposes of this site is to be able to introduce concepts to those who may have not thought about the subject, and such statements are not obvious at all. Therefore, however trivial, all such statements are added as completely separate pages, linking to the definition page which would then have a link on the "Also see" section to that consequence. An example of this is the page Definition:Transitive Class.

I have going through some of your recent edits and amended as appropriate or added templates indicating work needed, so that you get the idea of how these things need to be presented. --prime mover 04:31, 26 November 2011 (CST)

Sources

Please note that the sources at the bottom of a page are intended to be in chronological order with respect to date of publication. The most recent work should be at the bottom. TIA. --Lord_Farin 21:53, 24 July 2012 (UTC)

Thank you for making me aware of this policy. I will keep this in mind. --Andrew Salmon 21:59, 24 July 2012 (UTC)

Talk pages

... and when you add a new topic to a talk page, (a) add it to the bottom, and (b) add a new heading by pressing the "Add topic" link (see above) otherwise it's irritatingly tedious to work out what's being said.

And while I'm about it, I reiterate the request to (a) add links to concepts used, and (b) add the category into which a page goes in. (I mention this because you added a page earlier this evening with neither.)

Always worth taking a look at what has been changed when a page of yours has been edited, to see what was needed to bring the page to house style. --prime mover 22:01, 24 July 2012 (UTC)

That being said, we still value your contributions; please don't be put off by our mercilessly enforced policies on stylistic intricacies. --Lord_Farin 22:03, 24 July 2012 (UTC)

OTOH you might want to read this. --prime mover 05:26, 25 July 2012 (UTC)

eqn template

I see your eqn template, but would suggest that in the "implies" version, the "implies" tag goes into the ll column, leaving the o column free for the operator (by default "equals". You might want to press "random proof" a few times till you find an appropriate example - they are very common. Failing that, I have a page full of proof structure templates which you may like to study. --prime mover 08:35, 29 July 2012 (UTC)

Axiomatic Set Theory

Since we are aiming to have more than one axiomatisation of set theory eventually, it is vital to specify in which axiom system one lives. In order to do so there needs to be a page like Definition:Zermelo-Fraenkel Axioms to explicate what the working assumptions are when one derives results in LST. --Lord_Farin 06:30, 7 August 2012 (UTC)

So far, everything except for what has specifically been marked Category:Axiom of Regularity is provable without the axiom of regularity or choice (of what is referenced in the Takeuti/Zaring book reference). It may be of some use to specify what cannot be proven without Replacement or Infinity. The theorems on ordinals require Replacement, and some require infinity (without infinity, there are no limit ordinals, so the proofs would be greatly simplified).

It really depends what other set theories you mean. If you mean something very similar to ZFC like NGB or MK set theory, then you can prove that NGB is a conservative extension of ZFC and simply transfer theorems from ZFC to NGB. Something similar can be done for MK. However, if you are thinking about something like New Foundations or Type Theory, then the behavior is really weird (you can't even prove Cantor's theorem in New Foundations), and you're practically forced to have a completely independent development. --Andrew Salmon 06:46, 7 August 2012 (UTC)

Additionally, let me voice some concerns on the use of $x$ and $A$. As it stands, predicate logic does not allow to discriminate multiple types of variables. Hence we would be forced to adopt that $A \in U$; I can see this is overcome by defining what a set is, namely a class $x$ with $\exists y: x \in y$ but one has to be very careful. *Please* try to be as rigorous as possible when deriving results in these basic realms, using the principles of reasoning coming with PredCalc and all. --Lord_Farin 06:38, 7 August 2012 (UTC)

I use $x,y,z,a,b,c,\dots$ as my set variables and $A,B,C,\dots$ as my class variables. Much of the recent development I have been trying has been to formalize this distinction between sets and classes. In Definition:Class (Class Theory), you can see that every statement involving $\{ x : P(x) \}$ can be reduced to simpler statements. So when we write a statement with classes, the $A$ is not necessarily a value of some variable $x$. It all depends on whether $\exists x: x = A$. See the definition of "small" under Definition:Class (Class Theory). Takeuti uses his own notation to say that $A$ is a set: $\mathscr{M} \left({A}\right)$ --Andrew Salmon 06:46, 7 August 2012 (UTC)

I got the part that you were trying to distinguish sets and classes. What I hadn't been able to derive from the posted results was that all of this is intended to take place in the ZF axiom system. In fact, what got obfuscated was that the notation $A$ is in fact a def.abbrev. (how tempting it is to identify a unary symbol $P$ with its class...) and that everything talked about is in fact rigorously defined. I haven't encountered a place where the stuff you elucidate here is actually developed; now it actually does make sense. Part of the confusion is the overloading of the symbol $\in$, but this is of course intended; nonetheless all of this needs to be put somewhere visibly and clearly, preferably on the page where this class model theory is introduced (Definition:Structure (Set Theory) is not adequate atm). Thanks for the responses. --Lord_Farin 06:57, 7 August 2012 (UTC)

Will do, but I must get some sleep. I may not get to it in the morning, but I will certainly try to get it done sometime tomorrow. --Andrew Salmon 07:03, 7 August 2012 (UTC)

Check out the new Category:Zermelo-Fraenkel Class Theory and Definition:Class (Class Theory)/Zermelo-Fraenkel which hopefully will help to structure and canonicalise the results you are putting up. --Lord_Farin 09:03, 7 August 2012 (UTC)

Suggested approach

I see plenty of material added from Takeuti, but what it seems like is that the work is being done in a non-rigorous order (i.e. you're now working on chapter 4, having done stuff from chapter 7 and 8, and now 12 etc.)

All well and good, but the problem we're seeing is that the language and symbology being employed is often taken for granted and not explained, thus making the page ambiguous and hard to understand without the full background.

What I have tried to do is to start from the very beginning of any book from which I am working (or, if appropriate, from an appendix, if it contains all the background material), taking the time to comb through the basic exposition of prerequisites, to ensure that all language used is explained, somewhere on a (probably already existing) page on ProofWiki. In that way, any extra idiosyncrasies of definition and/or notation can be appropriately linked to and documented, and so when a usage is needed, it can be take directly from there.

In that way it is much clearer at which point an exposition diverges from the thread of discourse as defined in ProofWiki, and a most closer control can be exerted over variants of existing pages, rather than (as tends to happen now) a completely parallel thread emerges containing the same information just in a different language.

So it might be a useful exercise to go through the early chapters of Takeuti with the above in mind. --prime mover 09:09, 7 August 2012 (UTC)

I hadn't realized that until very recently, I was using "set" to denote both small classes and set variables (the $x$ in $\forall x:$). I will be adding a few pages to try to resolve this ambiguity. --Andrew Salmon 15:21, 7 August 2012 (UTC)

I note that the standard of your writing has started to approach house style. Keep up the good work! --Lord_Farin 08:54, 9 August 2012 (UTC)

Well-founded relations and minimal elements

Can you check over Strictly Well-Founded Relation determines Strictly Minimal Elements? You created the page initially, apparently using a written source, but the proof was screwy. I think I've fixed it now, but I need more eyes. --Dfeuer (talk) 00:42, 30 December 2012 (UTC)

$\RR$ and $\RR'$ are identical when restricted to $B$; why not just use that to show that they have the same minimal elements? --Andrew Salmon (talk) 19:45, 30 December 2012 (UTC)

On Transitive Closure Always Exists (Set Theory)

Dfeuer's proof (currently at Set Contained in Smallest Transitive Set) yields the same set as yours, so there is no need to keep both. I am inclined to merge the stuff up into one nice proof. Would you mind if I so acted? --Lord_Farin (talk) 10:05, 31 December 2012 (UTC)

Q: Is there mileage in keeping both proofs, using the standard Proof 1, Proof 2 paradigm? --prime mover (talk) 10:11, 31 December 2012 (UTC)

They use practically the same approach, and the same set (but the latter is implicit). I think it not meaningful. --Lord_Farin (talk) 10:59, 31 December 2012 (UTC)

They're essentially duplicates, from what I see. I would not mind. --Andrew Salmon (talk) 20:06, 31 December 2012 (UTC)