Formal Omniscient-God-and-Free-Will Theory, and Proof of its Self-Contradictory State

by Harry Foundalis

The theory “God is omniscient and humans have free will” is given below as a set of propositions (axioms).
Below that, a proof is given that those axioms are self-contradictory.

Theory

// A note on syntax: everything on a line after a double slash (//), such as this one, is a comment.
// Comments play no role other than helping the reader interpret the formal symbols, and can be discarded.
// Lower-case letters are either variables or parameters of predicates.
// The two constants of the theory (“God” and “Human”) are given explicitly.
// The precedence of operators is the usual/expected one: logical AND (Λ) has precedence over the implication (→), etc.
// The scopes of quantifiers (" and $) are given either explicitly (with a pair of parentheses),
// or implicitly, understood to be applying on the next well-formed formula.
// The theory is stated through the use of types (it is a typed theory). It is straightforward to rephrase it without types.

Types

agent, action, time;

Predicates

HasFreeWill (agent, agent);
Omniscient (agent);
TakesAction (agent, action, time);
KnowsChoice (agent, agent, action, time, time);
Prior (time, time);		 // 1st agent has free will from the point of view of a 2nd agent.
// the agent has absolute knowledge of everything.
// the agent takes action at a given time.
// 1st agent at time 1 knows that the choice of 2nd agent at time 2 is action.
// time 1 is prior to time 2.

Constants

God, Human : agent;

Variables

x, y : agent;
a : action;
t1, t2 : time;

Axioms

// 1. What “having free will” implies:
// If an agent x has free will from the point of view of agent y, then there is an action a that x can take at time t2
// such that at no time t1 prior to t2 does agent y know that x would take that action:

"x "y (HasFreeWill (x, y) → $a $t2 "t1 (Prior (t1, t2) Λ TakesAction (x, a, t2) → ¬KnowsChoice (y, x, a, t1, t2)))

// 2. What “being omniscient” implies:
// If an agent x has absolute knowledge of everything (is omniscient) then there is no action a that any agent y can take at time t2
// such that agent x does not know, at any time t1 prior to t2, that y will take action a at t2:

"x (Omniscient (x) → ¬ ($a $y $t2 "t1 (Prior (t1, t2) Λ TakesAction (y, a, t2) → ¬KnowsChoice (x, y, a, t1, t2))))

// 3. God is an agent who has absolute knowledge of everything:

Omniscient (God)

// 4. Human is an agent who has free will from the point of view of God:

HasFreeWill (Human, God)

Theorem

The above set of propositions (axioms) is self-contradictory.

Proof

(Note: because the proof is formal, the numbers in the comments of each axiom will be used to identify the axiom, for the reader’s convenience. For the same reason, Roman numerals are used to number the steps of the proof.)

i. In proposition 1 we can eliminate the existentially quantified variables a & t2 by introducing two Skolem functors Sk1() and Sk2(), respectively, each of which depends on the two universally quantified variables x & y, because they are the ones that include a & t2 in their scopes. After that, we can also move all universally quantified variables at the beginning. Thus, 1 becomes:

1a. "x "y "t1 (HasFreeWill (x, y) → (Prior (t1, Sk2(x,y)) Λ TakesAction (x, Sk1(x,y), Sk2(x,y)) → ¬KnowsChoice (y, x, Sk1(x,y), t1, Sk2(x,y))))

ii. In proposition 2 we can eliminate the implication symbols by applying the definition of implication: P → Q ↔ ¬P V Q:

2a. "x (¬ Omniscient (x) V ¬ ($a $y $t2 "t1 (¬ (Prior (t1, t2) Λ TakesAction (y, a, t2)) V ¬KnowsChoice (x, y, a, t1, t2))))

Next, we can reduce the scope of the negation symbols by repeatedly applying the rules:
¬ $x P(x) ↔ "x ¬ P(x),
¬ "x P(x) ↔ $x ¬ P(x),
and de Morgan’s laws. Thus, 2a becomes:

2b. "x (¬ Omniscient (x) V "a "y "t2 $t1 ¬ (¬ Prior (t1, t2) V ¬ TakesAction (y, a, t2) V ¬KnowsChoice (x, y, a, t1, t2)))

2c. "x (¬ Omniscient (x) V "a "y "t2 $t1 (Prior (t1, t2) Λ TakesAction (y, a, t2) Λ KnowsChoice (x, y, a, t1, t2)))

We can also eliminate the existentially quantified variable t1 by introducing a Skolem functor Sk3(), which depends on x, a, y, and t2, since all of them include t1 in their scopes:

2d. "x (¬ Omniscient (x) V "a "y "t2 (Prior (Sk3(x,a,y,t2), t2) Λ TakesAction (y, a, t2) Λ KnowsChoice (x, y, a, Sk3(x,a,y,t2), t2)))

Now all quantifiers can be moved to the beginning, and t2 can be renamed into t:

2e. "x "a "y "t (¬ Omniscient (x) V (Prior (Sk3(x,a,y,t), t) Λ TakesAction (y, a, t) Λ KnowsChoice (x, y, a, Sk3(x,a,y,t), t)))

Finally, applying the distributive laws for disjunction and conjunction, we can break down 2e into three independent clauses:

2f. "x "a "y "t (¬ Omniscient (x) V Prior (Sk3(x,a,y,t), t))

2g. "x "a "y "t (¬ Omniscient (x) V TakesAction (y, a, t))

2h. "x "a "y "t (¬ Omniscient (x) V KnowsChoice (x, y, a, Sk3(x,a,y,t), t))

iii. From 3 and 2g we get:

8. "a "y "t TakesAction (y, a, t)

iv. From 3 and 2f we get:

7. Prior (Sk3(God,a,y,t), t)

v. From 4 and 1a (and renaming t1 into t) we get:

10. "t (Prior (t, Sk2(Human,God)) Λ TakesAction (Human, Sk1(Human,God), Sk2(Human,God))
→ ¬KnowsChoice (God, Human, Sk1(Human,God), t, Sk2(Human,God)))

vi. From 7 and 10 we get:

11. TakesAction (Human, Sk1(Human,God), Sk2(Human,God))
→ ¬KnowsChoice (God, Human, Sk1(Human,God), Sk3(God,a,y,Sk2(Human,God)), Sk2(Human,God))

vii. From 11 and 8 we get:

12. ¬KnowsChoice (God, Human, Sk1(Human,God), Sk3(God,a,y,Sk2(Human,God)), Sk2(Human,God))

viii. From 3 and 2h we get:

13. "a "y "t (KnowsChoice (God, y, a, Sk3(God,a,y,t), t))

ix. Finally from 12 and 13, by means of the substitution set: {Human | y, Sk1(Human,God) | a, Sk2(Human,God) | t}, we get:

14. CONTRADICTION

Q.E.D.

Note: the reader may verify the above proof mechanically by going to this page and (after the theorem-proving applet is loaded) opening and running the file:
“God, omniscience, and free will”. The prover will find a proof which is essentially the same as the one given above.

Reload the originating page