Definition talk:Commutative Semigroup with respect to Equivalence Relation

Not sure if it is possible, but when semigroups on classes can also exist without equivalence relations, it might be better to have a 'Definition:Commutative Semigroup' and a 'Definition:Semigroup WRT Equivalence Relation'. --Lord_Farin 13:26, 23 January 2012 (EST)

One tricky

thing, I think, is that classes as they arise in ZF theory are more aspects of logical notation than they are mathematical objects,

per se, so to the extent that classes arise in other set theories, they may be somewhat different. The

Blah_Blah (Class Theory) approach thus seems odd. I do think

it's good to actually keep things consistent without banning any details of axiomatic set theory from the premises.

One approach (slightly unsavory, but I think more practical): since ZF theory is by far the most popular game in town, let it hold

by default everywhere, classes and all. Articles can then choose to have separate sections on how things go in

other systems, and ones specific to certain other systems can have some words saying so. Just a thought.

I haven't yet seen or heard of a really pleasant way to handle these matters. --Dfeuer (talk) 20:02, 16 December 2012 (UTC)

One of the things that I hold constantly in the back of my mind is that it ought to be possible to publish something that is pleasant. I want ProofWiki to be that pleasant thing. We've made a start at multi-axiom-schema definition (see the so-far 4 different approaches to the derivation of the natural numbers, for example. The same technique can be done for all else in the realms of axiomatics.

The fact that no such pleasant presentation has been done before is that before now all that has been available is books, and they are modelled by a linear (total) ordering and limited in size. ProofWiki is neither - it is a partial ordering and hence a directed acyclic graph (with extra structure complexity added as necessary). Has that aspect ever been analysed in detail? --prime mover (talk) 21:06, 16 December 2012 (UTC)

Is it possible to determine, automatically, what axioms, definitions, and theorems a given proof depends on? Is it possible to automatically propagate requirements? It may be that in axiom systems 1 and 2, theorem x holds, and theorem y is proven from theorem x (where y uses term t with definition t1), while in axiom system 3, theorem x does not hold, but theorems z and w do, and together those prove theorem y, where term t in y is given definition t2. I'm not saying it's impossible—not at all. But it's hard, and will probably require some additional software to navigate, along with massive refactoring. But the current situation, where definitions link to inconsistent ones, is much worse than just about any other option. --Dfeuer (talk) 22:05, 16 December 2012 (UTC)

Yes of course it's possible, you just have to construct the flow of linkages appropriately. This is one of the reasons why each page is intended to hold as atomic a fact as possible. However simple the statements, however trivial the proofs, if there are two on one page that is too many. Then you can link from one page to another and know exactly what is being linked to on each page.

When it comes to axiom schemata, each schema itself is considered to be an atom of reasoning. If you have, say, four axiom schemata which can be used as the basis of a definition (as we have with natural numbers) then you create the arguments for each one of these in four separate threads, each one with its own subcategory and naming conventions. Please feel free to investigate how this was done, if you're interested.

If we have a "current situation, where definitions link to inconsistent ones", which is "much worse than just about any other option" (I'd like to see evidence of such baseless and fatuous rhetoric) then something needs to be done about it beyond just using them as an example to point out the shortcomings of the website. --prime mover (talk) 22:16, 16 December 2012 (UTC)

The main place I'm seeing these problems is where class-theoretic definitions invoke set-theoretic

ones. "Let $C$ be a class, and let $\approx$ be an equivalence relation on $C$", for example, when we

define equivalence relations only on sets. Note also: I tried to figure out what the definition of semilattice

is supposed to mean, but it's deeply nested (hence confusing) and bottoms out in a stub definition

of groupoid. The deep nesting can probably be fixed by including some definitions it relies on in the page,

but I don't know how to fix the rest.--Dfeuer (talk) 22:28, 16 December 2012 (UTC)

Oh yeah, well that bunch of pages is rubbish anyway. Haven't worked out what to do with them yet so I'm just ignoring them. Suggest you do the same at the moment. May just delete the whole bag of rubbish and start again from a clean slate in due course. OTOH may just establish the isomorphism induced between the structures defined with an equals sign and those constructed by means of a generalised equivalence relation. Should be doable in a couple of pages. Then all the rest of that unholy crap can be deleted as just instances of that train of thought.

If there is a genuine train of thought here that leads to a whole new branch of as-yet unexplored mathematics then great, we can go away and explore the page of random ravings on the source website whence this material came, but don't hold your breath - instead there are plenty more areas of legitimate mathematics that need to be added.

BTW you may want to explore the formatting of material on a talk page. I for one would not have the patience to end every line with a CR and then tediously type a line of colons before the next line in my train of thought. You're not using NotePad as an external editor are you?? --prime mover (talk) 23:08, 16 December 2012 (UTC)

Oh, much worse. I'm typing directly on a smartphone at the moment. At home I don't have such problems. --Dfeuer (talk) 23:19, 16 December 2012 (UTC)