conceptual

We must not forget that variables are a very recent development within modern mathematics (from late XVI century). We are so used to them that it is easy to forget how artificial they are. Natural language does not have variables. How does it manage? Most people respond with “pronouns”. But there are also reference shifting markers. Traditionally, reference shifting markers track whether and how the referents of two related clauses are coordinated. The most basic sort of coordination is plain coreference, but there are reference shifting markers for other sort of relations, like disjointness, simultaneity, etc. In any case, markers are linguistic resources we have not exploited in formal languages, but we could, i.e., we could use them instead of variables.  So, for example, instead of the formula  (P → Q ) → (R → P),  we could just have the sequence  →2 → →   where that 2 is a reference shifting marking that tells us how the arguments of the basic operators are coordinated, and in pa