All Aliens on Earth Hate Donald J. Trump.

We are analyzing the proposition above from a classical predicate calculus perspective.

Source: Author using Perplexity AI

The proposition in the title looks like shameless clickbait. However, it could be true if you look at it from the perspective of classical first-order logic and if we propose a particular premise about the locations of aliens in the Universe. In this blog post, we will explore why this is the case.

To analyze the above proposition, we must translate it into predicate calculus, a formal language that utilizes logical and non-logical symbols.

Logical symbols include variables (x,y,z,…), connectives that link formulas (∧=’And’, ∨=’Or’, ¬=’Not’, ⭢=’Implies’, ≡=’Equivalent’), and the quantifier symbols (∃=’ exists’, ∀=’for all’) that quantify over variables only.

Note that variables like x are placeholders for objects in the domain of discourse. The domain of discourse represents the set of “things” we are reasoning about.

Note that in propositional logic, variables denote propositions that are either true or false. When looking at truth tables on connectives, we assume that variables are defined within propositional logic and therefore represent the truth value of an entire proposition (either true or false). While this dual role for variables might seem ambiguous, it is a standard convention in the study of logic.

Non-logical symbols are predicates that represent relations over variables and return a ‘true’ or ‘false’ truth value. The predicate ‘isGreen(x)’ returns true if the entity represented by the variable x is green and false otherwise. This is the way truth values are introduced into predicate calculus.

Of course, the real thing is much more involved, but beyond the scope of this blog post.

Formalizing The Premise We Hold

First, I must confess that I don’t believe — conspiracy theories put aside — that there are any aliens from other worlds on Earth. Therefore, we state our premise proposition (I):

(I)“There are no aliens on Earth.”.

How do we formalize our proposition (I)? Let x be any object or creature in the Universe, ‘Alien(x)’ a predicate that yields true if x is an alien, and ‘OnEarth(x)’ a predicate that yields true if the object is located on Earth. If the condition of a predicate is not met, it yields false. Then we can now formalize our premise proposition (I):

• Using Existential Quantification: ¬∃x( Alien(x)∧OnEarth(x) ) In plain English, this reads “There does not exist an x such that x is an alien and is located on Earth.”
• Using Universal Quantification: ∀x( (Alien(x)⟹¬OnEarth(x) ) In plain English, this reads “For all x holds: If x is an alien, then it is not located on Earth.”

The second version utilizes the connective ‘⟹’, which stands for material implication. Connectives like ‘∧’ and ‘∨’ are easy to grasp. It is a bit harder for the material implication, though. Using Wolfram Mathematica, the truth table of ‘x⟹y ‘ is as follows (recall that x and y denote propositions which are either true or false):

IN[1]:= tableForm := 
 TableForm[#, TableHeadings -> {None, {"x", "y", "x⟹y"}}] &

In[2]:= BooleanTable[{x,y,Implies[x,y]},{x,y}]//tableForm
Out[2]//TableForm=   x      y    x⟹y
                   -------------------
                   True   True   True
                   True   False  False
                   False  True   True
                   False  False  True

Note that three out of four times, the truth value (the third column) is true:

In[3]:= Cases[BooleanTable[{x,y,Implies[x,y]},{x,y}],{_,_,True}]//TableForm
Out[3]//TableForm=   x      y    x⟹y
                   -------------------
                   True   True   True
                   False  True   True
                   False  False  True

Formalizing The Conclusion We Seek

After this prelude, let’s jump right into the formalization of the conclusion, the title proposition, “All Aliens On Earth Hate Donald J. Trump.” We introduce a new predicate, ‘hateTrump(x),’ which is true if x hates Donald J. Trump or false otherwise.

What we want to demonstrate is the following:

(I)“There are no aliens on Earth.” Therefore: (II) “All Aliens On Earth Hate Donald J. Trump.”

More formally, we write using the “therefore” or “hence” symbol ∴:

(I) ∀x( Alien(x)⟹¬OnEarth(x) ) — — — — — — — — — — — — — — — — — — — — — — — — — (II) ∴ ∀x( (Alien(x)∧OnEarth(x)) ⟹ HateTrump(x) )

Finding The Truth, Nothing But The Truth

Let’s analyze the formalization (II): Note that the quantifier for x includes the entire implication. The predicate ‘Alien(x)’ is true if and only if x is an alien. The predicate OnEarth(x) is true if and only if x is located on Earth. If both conditions are met, then it is the case that an alien is on Earth hating Donald J. Trump, and this is valid for all aliens on Earth. However, we must consider premise (I). It states that there are no Aliens on Earth. So, we know that ‘Alien(x)∧OnEarth(x)’ of (II) is always false for aliens.

Given that the antecedent is false, it doesn’t matter whether the consequent is true or false; the material implication in (II) is always true. Therefore, it doesn’t matter whether an alien hates Donald J. Trump.

Looking above, we can confirm that in the truth table of the material implication, if x is false, it doesn’t matter whether y is true or false; the whole implication is true anyway.

Common Sense May Differ

We can look at it from a different perspective. Given the premise ∀x( Alien(x)⟹¬OnEarth(x) ), the subset of the domain of discourse satisfying Alien(x)∧OnEarth(x) is empty. What can follow from an empty set with no domain members in it? Common sense might suggest that nothing true can follow from a false premise; thus, the implication should be false.

However, the reasoning in formal logic differs. Utilizing formal logic, we need to find at least one counterexample to prove the implication false. A counterexample would be an x that is an alien and is on Earth. But there is no such x, given (I). Hence, the implication must be true.

Vacuous Truths

True material implications with false antecedents, regardless of the consequent’s truth values, are called “vacuous truths”. They make no claim about the truth value of the consequent.

But at least it could be true that all aliens on Earth hate Donald J. Trump. That is more than nothing to begin with.

Appendix

For readers interested in the formal verification of these claims, the following appendix demonstrates how to use the Wolfram Language (Mathematica) to test our formulas. This section is technical and not required to understand the main argument.

Defining the Formula in Mathematica

We have to formulate the formula within the predicate calculus to do this. We used “therefore” (∴) to reason about the formulae (I) and (II), and their relationship with each other. It is a metalogical symbol that is not part of the calculus. Within the predicate calculus, the material implication ⟹ denotes ∴. This is justified by the the *Deduction theorem*; hence we formulate the entire formula like this:

∀x( Alien(x) ⟹ ¬OnEarth(x) ) ⟹ ∀x( (Alien(x)∧OnEarth(x)) ⟹ HateTrump(x) )

In Mathematica:

In[4]:= 
premise=ForAll[x,Implies[Alien[x],Not[OnEarth[x]]]];
conclusion=ForAll[x,Implies[Alien[x]&&OnEarth[x],HateTrump[x]]];
formula=Implies[premise,conclusion];
formula//FullForm
Out[4]//FullForm= Implies[
  ForAll[x,Implies[Alien[x],Not[OnEarth[x]]]],
  ForAll[x,Implies[And[Alien[x],OnEarth[x]],HateTrump[x]]]
]

Is the Formula a Well-Formed Formula (WFF)?

To check whether our formula is a well-formed first-order logic formula, we write a Mathematica function makeWellFormedFormulaQ to create a checker function that examines the structure of the formula. Note that the implemented grammar is restricted, e.g., only connectives with exactly two operands are allowed, but it is sufficient for our purposes. The makeWellFormedFormulaQ function uses the Factory pattern to make and return a function that checks the WFF property.

ClearAll[MakeWellFormedFormulaQ];

makeWellFormedFormulaQ::nondisjoint = 
  "The predicate and function symbol sets must be disjoint. Symbol `1` was found in both lists.";

makeWellFormedFormulaQ[preds_List, funcs_List] := Module[
  {intersection, wffQ, termQ, atomicFormulaQ},

(* 1. Enforce disjointness at the time of creation *)
  intersection = Intersection[preds, funcs];
  If[
   Length[intersection] > 0,
   Message[MakeWellFormedFormulaQ::nondisjoint, First[intersection]];
   Return[$Failed];
   ];

(* 2.---Define Helper Functions within the private scope--- *)
  termQ[s_Symbol] := ! MemberQ[preds, s] && ! MemberQ[funcs, s];
  termQ[h_Symbol[args___]] := 
   MemberQ[funcs, h] && And @@ (termQ /@ {args});
  termQ[_] := False;

  atomicFormulaQ[p_Symbol] := MemberQ[preds, p];
  atomicFormulaQ[p_Symbol[args___]] := 
   MemberQ[preds, p] && And @@ (termQ /@ {args});
  atomicFormulaQ[_] := False;

(* 3.---Define the main checker logic using the private helpers--- *)
  wffQ[e_] /; atomicFormulaQ[e] := True;
  wffQ[Not[phi_]] := wffQ[phi];
  wffQ[(And | Or | Implies | Equivalent)[phi_, psi_]] := 
   wffQ[phi] && wffQ[psi];
  wffQ[(ForAll | Exists)[v_, phi_]] /; 
   Head[v] === Symbol && termQ[v] := wffQ[phi];
  wffQ[___] := False;

(* 4. Closure: Return the fully-formed checker function *)
  wffQ
   ]; 

We instantiate the WFF checker function isWFF for our formula and apply it to it. We provide the checker function factory with the list of names of our predicates. We do not use functions; hence, the function list is empty.

isWFF = makeWellFormedFormulaQ[{Alien, OnEarth, HateTrump}, {}]
In[5]:= isWFF[formula]
Out[5]= True

Mathematica confirms that our formula is a WFF according to the defined grammar.

Does (I) Imply (II)?

Let’s check with Mathematica whether our conclusion (II) is true given the premise (I). In the language of first-order logic, we test whether the formula is logically valid.

As a prerequisite, we define the domain of discourse in Mathematica as the set of all positive integers. All creatures and things in the Universe have a unique number assigned to them, which will help Mathematica’s algorithms to analyze our formula more precisely.

In[6]:= domain=Element[x, PositiveIntegers];
premiseDomain=ForAll[x, domain,Implies[Alien[x], !OnEarth[x]]];
conclusionDomain=ForAll[x,domain, Implies[Alien[x] && OnEarth[x], HateTrump[x]]];
formulaDomain=Implies[premiseDomain,conclusionDomain];
formulaDomain//FullForm
Out[6]//FullForm= 
Implies[
  ForAll[x,And[Element[x,Integers],Greater[x,0]],
    Implies[Alien[x],Not[OnEarth[x]]]],
  ForAll[x,And[Element[x,Integers],Greater[x,0]],
    Implies[And[Alien[x],OnEarth[x]],HateTrump[x]]]]
In[7]:= Resolve[formulaWithDomain]//FullForm
Out[7]//FullForm= 
Or[Exists[List[x],And[Element[x,Integers],Greater[x,0]],
     Not[Implies[Alien[x],Not[OnEarth[x]]]]],
   ForAll[List[x],And[Element[x,Integers],Greater[x,0]],
     Implies[And[Alien[x],OnEarth[x]],HateTrump[x]]]]

The Resolve function attempts to resolve the formula in a form that eliminates the quantifiers ∃ and ∀. Unfortunately, it doesn’t succeed because Mathematica doesn’t provide a full-blown first-order logic theorem prover. Therefore, we must employ an alternative approach, as outlined below.

Is The Formula A Tautology?

Let’s check next whether the entire formula is a tautology within propositional logic.

Tautology is a concept of propositional logic: Every possible combination of truth value assignment to the variables of the formula yields true as the formula’s result. Predicate logic only “knows” the concept of logically valid formulas, and tautological formulas are a subset of these.

We must substitute all predicates with variables and eliminate all quantifiers in our formula because propositional logic can’t represent them. Hence, we write a function replaceFOLSymbols in Mathematica that replaces all quantifiers and predicate names with variable names of the form “p`$p_i”, i=1,2,3,…. The variable names representing quantifiers will be removed automatically by Mathematica’s simplification algorithms because they are free and are not used in the resulting formula.

Clear[replaceFOLSymbols];
replaceFOLSymbols[formula_] := Module[
  {connectives, propForm, genRule, subFormulas, replacementRules, 
   renumberedRules},

  (* We must preserve the quantifiers "Exists" and "ForAll" to process 
     its arguments. Mathematica will remove them automatically because 
     they bind no variables after substitution. *)
   connectives = {And, Or, Not, Implies, Equivalent, Exists, ForAll};  

  (* We introduce a new context (namespace)'p' to avoid polluting the 
     'Global' context with unexpected symbol names.
     Propositional variables adhere to the convention 'p`$p<n>'. *) 
   genRule := #1 -> Symbol["p`$p" <> ToString[First[#2]]] &;

   subFormulas[form_] := Union@Cases[
       form,
       sub_ /; FreeQ[connectives, Head[sub]],
       {0, Infinity} (* Check the head of the expression, too *)
      ];

   replacementRules[subFormula_] := MapIndexed[
         genRule, 
         subFormula
       ];

   renumberedRules[rules_] := MapIndexed[
            genRule,
            DeleteDuplicates[Level[rules, {-1}]]
       ];

   (* Replace all subexpressions that are not connectives *)    
    propForm = formula /. replacementRules[subFormulas[formula]];

   (* Renumber the variables, starting at 1 *)
    propForm /. renumberedRules[propForm]
];

Now it is easy to check whether our propositional formula is a tautology:

In[8]:= prepForm=replaceFOLSymbols[formulaWithDomain]
Out[8]= p`$p1&&p`$p2\[Implies](p`$p3&&!p`$p4\[Implies](p`$p3&&p`$p4\[Implies]p`$p5))
In[9]:= prepForm=prepForm /. 
              s_Symbol:>Symbol@StringReplace[
                 SymbolName[s],
                 "$"->""  
                 ]
Out[9]= p1&&p2\[Implies](p3&&!p4\[Implies](p3&&p4\[Implies]p5))
In[10]:= TautologyQ@prepForm
Out[10]= True

Note that all quantifiers are gone, and the resulting propositional formula is indeed a tautology.

It is also easy to check this employing a Boolean truth table.

In[11]:= targetVars=Take[Union@Level[prepForm,{-1}],-3];
          colExprs=Append[targetVars,prepForm];
          TableForm[
           BooleanTable[colExprs,targetVars],
           TableHeadings->{None,colExprs}
          ]
Out[11] //TableForm= p3     p4     p5   p1&&p2⭢(p3&&!p4⭢(p3&&p4⭢p5))
                    --------------------------------------------------
                    True   True   True                 True
                    True   True   False                True
                    True   False  True                 True
                    True   False  False                True
                    False  True   True                 True
                    False  True   False                True
                    False  False  True                 True
                    False  False  False                True

The variables p1 and p2 are not displayed to keep the output short.

As a side note, we emphasize that there is no causal relationship between a vacuous truth and a tautology. The inverse is also true, of course.

Are the Premises Logically Equivalent?

We suppose in the main text that the formulas I and II below are logically equivalent:

¬∃x( Alien(x)∧OnEarth(x) (I) ∀x( (Alien(x)⟹¬OnEarth(x) ) (II)

Let us show that this is indeed the case (≡ means equivalence).

(1) ¬∃x( Alien(x)∧OnEarth(x) ) ≡ (2) ∀x ¬(Alien(x) ∧OnEarth(x) ) ≡ (3) ∀x( ¬Alien(x)∨¬OnEarth(x) ) ≡ (4) ∀x( (Alien(x)⟹¬OnEarth(x) )

Which laws did we use?

(1) -> (2): Quantifier-negation law: ¬∃x φ ≡ ∀x ¬φ (2) -> (3): De Morgan’s Law: ¬(A∧B)≡¬A∨¬B (3) -> (4): Definition of implication: P⟹Q ≡ ¬P ∨ Q.

The derivation (4) is our formula (II). We showed (I)⟹ (II). The conversion (II)⟹ (I) follows from the fact that we used only equivalence relations in our derivations. Hence, (I) ⇔ (II).

Let’s check this with Mathematica:

In[12]:= InFAformula=ForAll[x,Implies[Alien[x],Not[OnEarth[x]]]];
In[13]:= ExistsFormula=ForAll[x,Not[And[Alien[x],OnEarth[x]]]];
In[14]:= proof=FindEquationalProof[FAformula,ExistsFormula]
Out[14]= ProofObject[Logic: Predicate/EquationalLogic Steps: 40 

The experimental Mathematica function FindEquationalProof finds a proof in 40(!) steps.