I'll define my terminology via the following BNF grammar for implicational logical expressions:
<clause> ::= "("
<conclusion> ::= any variable
<premise> ::= (
(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
Does this pattern extend to every tautology in existence, and is there a proof of it?