User ross duncan - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T10:01:12Z http://mathoverflow.net/feeds/user/2138 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/50888/categories-of-logical-formulae/106518#106518 Answer by Ross Duncan for Categories of logical formulae Ross Duncan 2012-09-06T14:57:34Z 2012-09-06T14:57:34Z <p>I suspect the notion you are looking for is either a <em>multicategory</em> or a <em>polycategory</em>. Multicategories generalise categories by allowing more than one object in the domain of an arrow. These were introduced by Lambek specifically for the study of logical derivations. See</p> <blockquote> <p>J. Lambek (1969) "Deductive Systems and Categories (II)" in Category Theory, Homology Theory and their Applications I, Springer Lecture Notes in Mathematics 87, R. J. Hilton (ed.)</p> </blockquote> <p>Polycategories generalise multicategories by allowing multiple objects in the codomain of an arrow. See </p> <blockquote> <p>M. E. Szabo (1975) "Polycategories", <em>Communications in Algebra</em> 3.</p> </blockquote> <p>Of course there is a rich history of looking at categories whose objects are formula and whose arrows are proofs, coming mostly from the computer science literature. Lambek and Scott's book may be a good place to start, or for a more modern take try this introductory article <a href="http://arxiv.org/abs/1102.1313" rel="nofollow">http://arxiv.org/abs/1102.1313</a> However, for classical logics such categories always reduce to boolean algebras, so people tend to work with intuitionistic or linear logics.</p> http://mathoverflow.net/questions/101893/incidences-of-rigorous-proofs-used-in-legal-proceedings/101931#101931 Answer by Ross Duncan for Incidences of rigorous proofs used in legal proceedings Ross Duncan 2012-07-11T09:42:15Z 2012-07-11T09:42:15Z <p>This is not exactly an answer to the question but interesting none-the-less.</p> <p>In 2005 the British model Kate Moss was filmed putting some kind of white powder, allegedly cocaine, up her nose. The police wanted to press charges for possessing illegal drugs. However the pictures could not demonstrate exactly what the substance was, in particular whether it was a Class A or Class B drug, each of which would require different charges to be brought. The British legal system does not allow a person to be tried on a disjunction of two charges so the case was dropped.</p> <p>Legal reasoning is often different to mathematical reasoning, but I found it amusing to see the courts employing intuitionist logic in this case, whereas mathematicians would usually be satisfied with a classical proof.</p> <p>Details: <a href="http://news.bbc.co.uk/2/hi/5082546.stm" rel="nofollow">http://news.bbc.co.uk/2/hi/5082546.stm</a></p> http://mathoverflow.net/questions/84388/presentation-of-the-clifford-group-by-generators-and-relations Presentation of the Clifford group by generators and relations? Ross Duncan 2011-12-27T15:10:24Z 2012-01-02T13:30:59Z <p>The Clifford group $\mathcal{C}_n$ is a matrix group on $\mathbb{C}^{2^n}$ generated by tensor products of the following matrices: $$P = \begin{pmatrix} 1 &amp; 0 \\ 0 &amp; i\end{pmatrix} \quad H = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 &amp; 1 \\ 1 &amp; -1\end{pmatrix} \quad \wedge\! X = \begin{pmatrix}1 &amp; 0 &amp; 0 &amp; 0 \\ 0 &amp; 1 &amp; 0 &amp; 0 \\ 0 &amp; 0 &amp; 0 &amp; 1 \\ 0 &amp; 0 &amp; 1 &amp; 0\end{pmatrix}$$ For my purposes I take equality up to a complex unit, i.e., if $A = e^{i\alpha}B$ then $A = B$.</p> <p>My question is: </p> <blockquote> <p>is there an abstract presentation of this group by generators and relations?</p> </blockquote> <p>Or the easier version: </p> <blockquote> <p>is there a presentation of $\mathcal{C}_2$ or $\mathcal{C}_3$ by generators and relations?</p> </blockquote> <p>I don't care which set of generators is used, although it would be nice if the generators were those given above.</p> http://mathoverflow.net/questions/101893/incidences-of-rigorous-proofs-used-in-legal-proceedings/101931#101931 Comment by Ross Duncan Ross Duncan 2012-07-11T15:25:12Z 2012-07-11T15:25:12Z Even given A -&gt; &quot;10 years&quot; and B -&gt; &quot;10 years&quot;, one would still need an (intuitionistic) proof of A v B to conclude &quot;10 years&quot; unconditionally, luckily for Moss. http://mathoverflow.net/questions/84388/presentation-of-the-clifford-group-by-generators-and-relations/84431#84431 Comment by Ross Duncan Ross Duncan 2012-01-24T13:29:13Z 2012-01-24T13:29:13Z Sorry - just like the above answer - the group you mention here has the wrong order. Thanks anyway. http://mathoverflow.net/questions/84388/presentation-of-the-clifford-group-by-generators-and-relations/84400#84400 Comment by Ross Duncan Ross Duncan 2012-01-24T13:28:33Z 2012-01-24T13:28:33Z Hi Adam, thanks for the response, but we are not talking about the same group - this can easily be seen by looking at the order. http://mathoverflow.net/questions/84388/presentation-of-the-clifford-group-by-generators-and-relations/84744#84744 Comment by Ross Duncan Ross Duncan 2012-01-24T13:27:28Z 2012-01-24T13:27:28Z Thanks for this answer David, and the very interesting paper you linked to. I (still!) have not had enough time to digest it properly. It doesn't seem to help me much for my current problem though, because I am really interested in the qubit case. The reason that I am asking for a generators and relations is because I want to prove that a certain formal system (a variation on the one here: <a href="http://arxiv.org/abs/0906.4725" rel="nofollow">arxiv.org/abs/0906.4725</a> ) decides the equality of Clifford circuits. If someone had already worked out which equations were necessary then this would have helped immensely. Cheers! http://mathoverflow.net/questions/84388/presentation-of-the-clifford-group-by-generators-and-relations/84391#84391 Comment by Ross Duncan Ross Duncan 2012-01-24T12:07:55Z 2012-01-24T12:07:55Z Thanks for this Boris - I had seen that survey, but sadly I don't find what I was looking for there or in the references. Gottesman's thesis was the most useful for my actual purpose.