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.

// 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 t_{1} prior to t_{2}
does agent y know that x would take that action:

"x "y (HasFreeWill (x, y) → $a $t

_{2}"t_{1}(Prior (t_{1}, t_{2}) Λ TakesAction (x, a, t_{2}) → ¬KnowsChoice (y, x, a, t_{1}, t_{2})))

// 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 t_{2}

// such that agent x does not know, at any time t_{1}
prior to t_{2}, that y will take action a at t_{2}:

"x (Omniscient (x) → ¬ ($a $y $t

_{2}"t_{1}(Prior (t_{1}, t_{2}) Λ TakesAction (y, a, t_{2}) → ¬KnowsChoice (x, y, a, t_{1}, t_{2}))))

// 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 & t_{2} by introducing two Skolem functors Sk_{1}()
and Sk_{2}(), respectively, each of which depends
on the two universally quantified variables x & y, because they are the ones
that include a & t_{2} in their scopes. After
that, we can also move all universally quantified variables at the beginning. Thus,
1 becomes:

1a. "x "y "t

_{1}(HasFreeWill (x, y) → (Prior (t_{1}, Sk_{2}(x,y)) Λ TakesAction (x, Sk_{1}(x,y), Sk_{2}(x,y)) → ¬KnowsChoice (y, x, Sk_{1}(x,y), t_{1}, Sk_{2}(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 $t

_{2}"t_{1}(¬ (Prior (t_{1}, t_{2}) Λ TakesAction (y, a, t_{2})) V ¬KnowsChoice (x, y, a, t_{1}, t_{2}))))

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 "t

_{2}$t_{1}¬ (¬ Prior (t_{1}, t_{2}) V ¬ TakesAction (y, a, t_{2}) V ¬KnowsChoice (x, y, a, t_{1}, t_{2})))2c. "x (¬ Omniscient (x) V "a "y "t

_{2}$t_{1}(Prior (t_{1}, t_{2}) Λ TakesAction (y, a, t_{2}) Λ KnowsChoice (x, y, a, t_{1}, t_{2})))

We can also eliminate the existentially quantified variable t_{1} by introducing
a Skolem functor Sk_{3}(), which depends on x, a,
y, and t_{2}, since all of them include t_{1}
in their scopes:

2d. "x (¬ Omniscient (x) V "a "y "t

_{2}(Prior (Sk_{3}(x,a,y,t_{2}), t_{2}) Λ TakesAction (y, a, t_{2}) Λ KnowsChoice (x, y, a, Sk_{3}(x,a,y,t_{2}), t_{2})))

Now all quantifiers can be moved to the beginning, and t_{2}
can be renamed into t:

2e. "x "a "y "t (¬ Omniscient (x) V (Prior (Sk

_{3}(x,a,y,t), t) Λ TakesAction (y, a, t) Λ KnowsChoice (x, y, a, Sk_{3}(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 (Sk

_{3}(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, Sk

_{3}(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 (Sk

_{3}(God,a,y,t), t)

*v.* From 4 and 1a (and renaming t_{1}
into t) we get:

10. "t (Prior (t, Sk

_{2}(Human,God)) Λ TakesAction (Human, Sk_{1}(Human,God), Sk_{2}(Human,God))

→ ¬KnowsChoice (God, Human, Sk_{1}(Human,God), t, Sk_{2}(Human,God)))

*vi.* From 7 and 10 we get:

11. TakesAction (Human, Sk

_{1}(Human,God), Sk_{2}(Human,God))

→ ¬KnowsChoice (God, Human, Sk_{1}(Human,God), Sk_{3}(God,a,y,Sk_{2}(Human,God)), Sk_{2}(Human,God))

*vii.* From 11 and 8 we get:

12. ¬KnowsChoice (God, Human, Sk

_{1}(Human,God), Sk_{3}(God,a,y,Sk_{2}(Human,God)), Sk_{2}(Human,God))

*viii.* From 3 and 2h we get:

13. "a "y "t (KnowsChoice (God, y, a, Sk

_{3}(God,a,y,t), t))

*ix.* Finally from 12 and 13, by means of the
substitution set: {Human | y, Sk_{1}(Human,God) |
a, Sk_{2}(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.