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?

  • 3
    $\begingroup$ What about e.g. $\bot\to x$? $\endgroup$
    – Berci
    May 27 at 18:13
  • $\begingroup$ You are correct, I did not think about that. Thank you, I will remove absurdity from the question. $\endgroup$
    – Jason
    May 27 at 18:32
  • $\begingroup$ Do you mean that no variables are repeated? I.e. any variable that occurs in the formula only occurs once? $\endgroup$
    – Sambo
    May 27 at 18:36

2 Answers 2


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


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.

  • 4
    $\begingroup$ This is really an inductive argument, right? To find an assignment making $\varphi\implies \psi$ false, you need to find an assignment making $\psi$ false (which is possible by induction). It's interesting to note from unwinding this inductive argument that you can always set the right-most variable to false and all others to true. $\endgroup$ May 27 at 19:02
  • $\begingroup$ That's right, to prove it formally, you have to induct on the height of the sentence's syntax tree. $\endgroup$ May 27 at 19:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.