I have a quantified formula. I want to show what happens when the order of quantifiers is reversed. To do this, I like to use a two-headed arrow over the formula, like this:

Is it possible? I don't care if you use graphical packages (like TikZ), as long as I can place the arrow in the right place.

-
Interesting! This would also be useful for anyone using Bourbaki’s syntax for binders/quantifiers: to avoid using actual named variables and so having to deal with α-equivalence etc., he adds edges linking each binder to the occurrences of its bound ‘variables’; the edges are drawn much like your arrow but without the arrowheads, iirc. – Peter LeFanu Lumsdaine Dec 3 '10 at 22:09
@Peter: Thanks for your interest. Off-topic: Can you provide a link for "Bourbaki’s syntax"? – M.S. Dousti Dec 3 '10 at 22:38
books.google.com/… (p. 15) – Caramdir Dec 3 '10 at 23:16
@Caramdir: Thanks for the pointer. – M.S. Dousti Dec 4 '10 at 5:47

On way to do this with TikZ is the following:

\documentclass{minimal}
\usepackage{tikz}
\usetikzlibrary{positioning}
\begin{document}
a
% inner sep=0 removes unwanted padding in the nodes;
% baseline, anchor=base alignes the baseline of the text in the nodes
%      with the baseline of the sourrounding text;
% >=latex selects the arrow style (see the TikZ manual for which
%      arrows are available.
\begin{tikzpicture}[inner sep=0cm,baseline,anchor=base,>=latex]
% the first node, named 'left-node'
\node (left-node) {$(\forall x \in X)$};

% add a second node to the right of left-node
\node [right=0cm of left-node] (right-node) {$(\forall y \in Y)$};

% draw the connecting line between the north sides of the two nodes,
% 1.5ex above the nodes.
\draw[<->,red] (left-node.north) |- +(0,1.5ex) -| (right-node.north);

% alternatively, draw a line between the north sides of the two nodes, with
% starting angle 30° and ending at 150°.
%\draw[<->,red] (left-node.north) to[out=30,in=150] (right-node.north);
\end{tikzpicture}
b
\end{document}


Which gives or , depending on which of the lines starting with \draw you uncomment. Depending on where you want to use this, you might want to add \displaystyle in the math in the two nodes.

There seems to be interest in doing something like pst-node in TikZ. A first approximation would be (the following examples need to be compiled two times)

\newcommand\tikzmark[1]{\tikz[remember picture,overlay,baseline=-1ex] \node (#1) {};}

$(\forall x\tikzmark{a}\in X)(\forall y\tikzmark{b}\in Y)$
\tikz[remember picture,overlay] \draw[<->,red] (a.north) |- +(0,1.5ex) -| (b.north);


This is however not quite what one wants, in this case, as the mark is not in the middle:

Adding a second parameter to \tikzmark is not quite trivial as just putting the content into a node destroys all context (mathmode, spacing, etc.). I can't quite follow what pst-node does in \rnode (but judging from the result some space gets lost). If the usage is limited to simple cases, the following should work reasonably well (if necessary add \displaystyle):

\newcommand\tikzmark[2]{\tikz[remember picture,baseline,anchor=base] \node (#1) {$#2$};}

$(\forall x\tikzmark{a}{\in} X)(\forall y\tikzmark{b}{\in} Y)$
\tikz[remember picture,overlay] \draw[<->,red] (a.north) |- +(0,1.5ex) -| (b.north);


There is one more problem: overlayed pictures do not take any space, so the line and arrows might collide with text on the preceding line. I don't know how to fix this without manually adding some space.

With my first example, you can also do more fancy things, like

\documentclass{minimal}
\usepackage{tikz}
\usetikzlibrary{positioning,decorations.pathreplacing,calc}
\begin{document}
$\begin{tikzpicture}[inner sep=0cm,baseline,anchor=base,>=latex,decoration=brace] \node (left-node) {(\forall x \in X)}; \node [right=0cm of left-node] (right-node) {(\forall y \in Y)}; \draw[decorate,red] ((left-node.north west)+(0.3ex,0.2ex)) -- ((left-node.north east)+(-0.3ex,0.2ex)); \draw[decorate,red] ((right-node.north west)+(0.3ex,0.2ex)) -- ((right-node.north east)+(-0.3ex,0.2ex)); \draw[<->,red,transform canvas={yshift=1.2ex}] (left-node.north) to[out=30,in=150] (right-node.north); \end{tikzpicture}$
\end{document}


-
+1. Thanks a lot. The comments help a lot. I liked the idea of arc instead of straight line. – M.S. Dousti Dec 3 '10 at 22:41

Usually I also prefer pgf/tikZ. Nevertheless here comes a quick solution with pst-node.

\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{pst-node}

\begin{document}
$(\forall x\rnode{a}{\in} X)(\forall y\rnode{b}{\in} Y)$
\ncbar[angle=90,arrows=<->,nodesep=2pt]{a}{b}
\end{document}


-
I thought about doing something of this kind in TikZ, but then opted for automatic alignment of the arrow endpoints. But of course this is a lot more compact. – Caramdir Dec 3 '10 at 21:03
Furthermore it has the advantage that it can be used easily in common math environments. I tried »pgf/tikZ« with nodes and the remember picture option but couldn't make it work yet. – Thorsten Donig Dec 3 '10 at 21:26
I tried the exact same thing, and had the same result. I'd love to see a library like this for TikZ, because it definitely seems doable. Does anybody know of one? – Antal Spector-Zabusky Dec 3 '10 at 22:06
Thanks. I liked this solution for its compactness; but unfortunately pst-node does not work with pdflatex. In the environment I work, I can't compile to PS (because of using PDF-specific options). – M.S. Dousti Dec 3 '10 at 22:15
@Antal See my edited answer. – Caramdir Dec 3 '10 at 23:04