# Is the last variable of any implicational tautology also the last variable of one of its premises?

I'll define my terminology via the following BNF grammar for implicational logical expressions:

<clause> ::= "(" <premise> <conclusion> ")"
<conclusion> ::= any variable
<premise> ::= (<clause> "$$\rightarrow$$")*

(In other words, the premise of a clause is any number of sub-clauses, separated from themselves and from the last variable of the clause by the right-associative implication connective, "$$\rightarrow$$".)

Example: $$(((p \rightarrow q) \rightarrow r) \rightarrow (r \rightarrow p) \rightarrow (s) \rightarrow p)$$ is a clause with premise clauses $$((p \rightarrow q) \rightarrow r)$$, $$(r \rightarrow p)$$, and $$(s)$$, and a conclusion of $$p$$.

I wrote a program to enumerate the classical implicational propositional tautologies, and noticed an interesting pattern that is true for (at least) the first 120,957,915 tautologies (i.e. all tautologies having up to 19 characters when converted to polish notation).

The pattern is as follows: every tautology's conclusion is the same variable as the conclusion of at least one of its premise clauses.

Does this pattern extend to every tautology in existence, and is there a proof of it?

• Does "premise clause" mean direct premises or does a premise of a premise, etc., count? For example, if you had $\bot$, then $((A\to\bot)\to\bot)\to A$ would be a counterexample if we were considering direct premises but not if we counted the (trivial) conclusion of a premise of a premise of premise. – Derek Elkins May 4 at 3:49
• @DerekElkins a premise of a premise does not count. Also, the falsum operand "$\bot$" is not allowed by my grammar, only variables and the "$\rightarrow$" connective. – Hans Brende May 4 at 3:55

Yes, and here's the proof: Suppose you have a clause with conclusion $$p$$, but $$p$$ is not the conclusion of any of its premises. Then if $$p$$ is false but every other propositional variable is true, we have that each premise of the clause is true, while the conclusion is false. So the clause is false under this valuation of the propositional variables, and hence the clause is not a tautology.