User ross duncan - MathOverflow

Answer by Ross Duncan for Categories of logical formulae

2012-09-06T14:57:34Z

I suspect the notion you are looking for is either a multicategory or a polycategory. 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

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.)

Polycategories generalise multicategories by allowing multiple objects in the codomain of an arrow. See

M. E. Szabo (1975) "Polycategories", Communications in Algebra 3.

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 http://arxiv.org/abs/1102.1313 However, for classical logics such categories always reduce to boolean algebras, so people tend to work with intuitionistic or linear logics.

Answer by Ross Duncan for Incidences of rigorous proofs used in legal proceedings

2012-07-11T09:42:15Z

This is not exactly an answer to the question but interesting none-the-less.

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.

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.

Details: http://news.bbc.co.uk/2/hi/5082546.stm

Presentation of the Clifford group by generators and relations?

2011-12-27T15:10:24Z

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 & 0 \\ 0 & i\end{pmatrix} \quad H = \frac{1}{\sqrt{2}}\begin{pmatrix} 1 & 1 \\ 1 & -1\end{pmatrix} \quad \wedge\! X = \begin{pmatrix}1 & 0 & 0 & 0 \\ 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 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$.

My question is:

is there an abstract presentation of this group by generators and relations?

Or the easier version:

is there a presentation of $\mathcal{C}_2$ or $\mathcal{C}_3$ by generators and relations?

I don't care which set of generators is used, although it would be nice if the generators were those given above.

Comment by Ross Duncan

2012-07-11T15:25:12Z

Even given A -> "10 years" and B -> "10 years", one would still need an (intuitionistic) proof of A v B to conclude "10 years" unconditionally, luckily for Moss.

Comment by Ross Duncan

2012-01-24T13:29:13Z

Sorry - just like the above answer - the group you mention here has the wrong order. Thanks anyway.

Comment by Ross Duncan

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.

Comment by Ross Duncan

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: arxiv.org/abs/0906.4725 ) decides the equality of Clifford circuits. If someone had already worked out which equations were necessary then this would have helped immensely. Cheers!

Comment by Ross Duncan

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.