Can a formula with only unique variables be an intuitionistic tautology? Consider intuitionistic propositional formulae, using only the connective "$\rightarrow$"  and absurdity .
Can there exist a formula such that it is a theorem/tautology and every pair of variables contained in it, is a pair of different variables?
 A: No such formula is a tautology. Since the arguments to the outermost $\implies$ are independent, there is always a model where the antecedent is true and the consequent is false.
Let's do an example. Consider the sentence
$$ (a\implies b) \implies (c \implies (d \implies e)). $$
Because they share no variables, we can easily make $a\implies b$ true while $c \implies (d\implies e)$ is false. Consider any assignment with $a$ and $e$ false, and $c$ and $d$ true. Such an assignment gives the formula the form $T \implies F$, so it can't be a tautology.
A: You can prove this using the topological semantics for intuitionistic logic.
Our chosen topological space is $\mathbb{R}$ equipped with the standard topology. The open subsets of $\mathbb{R}$ are the truth values and $\mathbb{R}$ itself is the sole designated truth value. If you do this, you can construct explicit truth values for all of the variables in a well-formed formula that make the formula have a non-designated truth value.
Next I'll define a notion of a covariant position and a contravariant position.
In the well-formed formula, $a \to b$, $a$ is a contravariant position and $b$ is a covariant position.
In the well-formed formula $(a \to b) \to c$, $b$ is a contravariant position and $a$ and $c$ are covariant positions.
A position is covariant if and only if it is the antecedent of an even number of conditionals.
Consider a well-formed formula $\varphi$ with no repeated variable symbols. Let $A$ be the variables that appear covariantly and $B$ be the variables that appear contravariantly. Note that $A$ and $B$ are disjoint and their union is all the variables of $\varphi$.
Consider a variable $x$ that appears in $\varphi$.
If $x$ is in $A$, then give $x$ the truth value $\varnothing$.
If $x$ is in $B$, then give $x$ the truth value $\mathbb{R}$.
$\varphi$ will thus have the truth value $\varnothing$.
