bio | website | |
---|---|---|
location | ||
age | ||
visits | member for | 2 years, 7 months |
seen | 12 hours ago | |
stats | profile views | 430 |
Mar 23 |
accepted | Good set theory in which to study ordinal-indexed sequences? |
Feb 25 |
awarded | Nice Question |
Feb 23 |
comment |
The groupoid of algebraic expressions and proofs
@SylvainJULIEN, that's an intense look question fella. What, in particular, do you think the connection might be? By the way, your previous comment made my day. :) |
Feb 20 |
comment |
The groupoid of algebraic expressions and proofs
@AndrejBauer, well the path category of a quiver is associative precisely because the domain of the forgetful functor $\mathbf{Cat} \rightarrow \mathbf{Quiv}$ is $\mathbf{Cat}$. It should be the same thing here; by choosing an appropriate forgetful functor, with the correct domain, its left adjoint should build an associative structure "automatically". |
Feb 16 |
comment |
How have mathematicians been raised?
Step 0. Don't force them to do math. Ever. Step 1. Tell them interesting puzzles at their current level of development. Step 2. Set up somewhere to lie outside, so they can gaze up at the heavens, and wonder. To quote Atiyah: "In the broad light of day mathematicians check their equations and their proofs, leaving no stone unturned in their search for rigour. But, at night, under the full moon, they dream, they float among the stars and wonder at the miracle of the heavens. They are inspired. Without dreams there is no art, no mathematics, no life." Step 4. Don't force them to do math. Ever. |
Feb 15 |
comment |
The groupoid of algebraic expressions and proofs
@PaulTaylor, now if you can see a way of describe the construction of interest by abstracting the concept "Lawvere theory" and considering "Lawvere theory objects in a $2$-category $\mathbf{C}$ with sufficient structure", and then choosing $\mathbf{C}$ carefully to explain the construction of interest, well this would be very interesting. I cannot currently see how to do this, however, and your answer offers absolutely no hints or suggestions in this direction. |
Feb 15 |
comment |
The groupoid of algebraic expressions and proofs
@PaulTaylor, you misunderstand me. I would very much like to be able to view this as a special case of a more fundamental construction, perhaps the left-adjoint to some $2$-functor or some such. Nonetheless, the point remains that this groupoid-like-object is not a Lawvere theory in the usual sense of the word, and it cannot be recovered from the Lawvere theory. The act of passing from the presentation to the Lawvere theory throws away too much information, and we can't recover the groupoid of interest. |
Feb 13 |
comment |
The groupoid of algebraic expressions and proofs
Interesting. There's definitely a strong connection there. |
Feb 13 |
comment |
The groupoid of algebraic expressions and proofs
@TheMaskedAvenger, do you mean absolutely free algebra? |
Feb 13 |
accepted | Has this construction, which builds a symmetric multicategory from a commutative monoid, been described or studied anywhere, and if so, where? |
Feb 13 |
asked | The groupoid of algebraic expressions and proofs |
Feb 6 |
comment |
Which mathematicians have influenced you the most?
@GerryMyerson, we can be both. :) |
Feb 6 |
comment |
Which mathematicians have influenced you the most?
@IgorRivin, why did s/he say that? |
Jan 23 |
comment |
Proofs without words
Also, I am afraid you have misunderstood me. If I were to post a truth-tree for some logical tautology, well that would be a literal example of a "proof without words"; but, you would surely reject it as a non-example. Hence what you really mean is not "proof without words" but "proof without logic." |
Jan 23 |
comment |
Proofs without words
@MarianoSuárez-Alvarez, oh the concept is well-known alright; these useless so-called "proofs without words" are all over YouTube, usually paired with a lot of downvotes, and rightly so. Its sad that so much effort went into discovering these beautiful arguments, and then producing pictures and even animations to illustrate the idea, only to have all that hard work spoilt by this proof without words nonsense. How much better those so-called "proofs" would have been with a few premises, some inferences, and a conclusion. |
Jan 23 |
comment |
Proofs without words
There is no such thing as a "proof without logic," and since words are usually the best tool for conveying logical relations, I'm going to have to reject the idea of "proof without words." Sorry, -1. |
Jan 23 |
revised |
Extensional theorems mostly used intensionally
added 523 characters in body |
Jan 23 |
answered | Extensional theorems mostly used intensionally |
Jan 19 |
accepted | Looking for interesting, natural models of this algebraic theory in which $x^\dagger$ is not always the multiplicative inverse of $x$ |
Jan 15 |
revised |
Has this construction, which builds a symmetric multicategory from a commutative monoid, been described or studied anywhere, and if so, where?
added 1 character in body |