This is the first time I have written down a meta logic theorem I proved while a student at Berkeley in 1955.
While studying early theorems based on the predicate logic axioms from Quine’s ‘Mathematical Logic’ I was startled at the theorem ∃x(x=x).
What thing is this x?
The axioms had no content yet about any universe.
Why should mathematical logic demand anything.
Set theory embraces the empty set.
Theretofore about the most powerful theorem had been ∀x∀y∀z(x=y∧y=z→x=z).
I quickly activated my meagre knowledge of model theory and located the axiom that was incompatible with the empty universe and saw that it was trivial to modify it at allow the empty universe.
I was then terrified of the consequences of meddling with at the very foundations of math; would all of math come tumbling down if we messed with the axioms?

Happily I could prove that:

- Any proof of a theorem beginning with ‘∀’ based on the old axioms could be mechanically modified to prove that theorem based on the new axioms.
- Any theorem ‘∀xφ’ could be proven with the new axioms thus refuting ‘~∀xφ’ or its equivalent ‘∃x~φ’.

Some theorems from the old axioms become false in the new, such as ∃x(x=x).
To refute ∃x(x=x) I prove ∀x~(x=x) ⇒ ~∃x(x=x).
In general φ → ψ is an old theorem only if either one of ψ or ~φ are old theorems.
(Recall that there are no implicit universal quantifiers in this world.)

xx
Google “empty domain”.
E.g. see Empty Domain.