The “Mind-ful God”, or “God with a Mind” theory 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 only constant of the theory (“God”) is 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 simple enough to require no types (it is a type-less theory).

**Predicates**

IsPartOf (x, y); // to be interpreted as: x is part of y.

Material (x);

EntirelyImmaterial (x);

CanRemember (x);

Memory (x);

Event (x);

Time (x);

Space (x);

**Constants**

God;

**Axioms**

// 1. Any cognitive agent who can remember anything can do so
due to a memory,

// which the agent contains (i.e., the memory constitutes part of the agent’s
self):

"x (CanRemember (x) → $y (Memory (y) Λ IsPartOf (y, x)))

// 2. Every memory includes at least one event, which is part of that memory:

"x (Memory (x) → $y (Event (y) Λ IsPartOf (y, x)))

// 3. Every event x happens in space-time, i.e., it consists of spatial and temporal coordinates s and t:

"x (Event (x) → $s (Space (s) Λ IsPartOf (s, x)) Λ $t (Time (t) Λ IsPartOf (t, x)))

// 4. Time, according to modern physics, is material (i.e., just as material as space):

"t (Time (t) → Material (t))

// 5. If something material is part of something else, then that something else is also material:

"x "y (Material (x) Λ IsPartOf (x, y) → Material (y))

// 6. If something is entirely immaterial then it has no material part:

"x (EntirelyImmaterial (x) → ¬ $y (Material (y) Λ IsPartOf (y, x)))

// 7. God has the ability to remember things:

CanRemember (God)

// 8. God is entirely immaterial:

EntirelyImmaterial (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 variable y by introducing a Skolem functor Sk_{1}()
that depends on the universally quantified variable x. Thus, 1 becomes:

1a. "x (CanRemember (x) → Memory (Sk

_{1}(x)) Λ IsPartOf (Sk_{1}(x), x))

*ii.* From 7 and 1a we get:

9. Memory (Sk

_{1}(God)) Λ IsPartOf (Sk_{1}(God), God)

which we can write down as two separate conclusions:

9a. Memory (Sk

_{1}(God))9b. IsPartOf (Sk

_{1}(God), God)

*iii.* In proposition 2 we can eliminate the
existentially quantified variable y by introducing a Skolem functor Sk_{2}()
that depends on the universally quantified variable x. Thus, 2 becomes:

2a. "x (Memory (x) → Event (Sk

_{2}(x)) Λ IsPartOf (Sk_{2}(x), x))

*iv.* From 9a and 2a we get:

10. Event (Sk

_{2}(Sk_{1}(God))) Λ IsPartOf (Sk_{2}(Sk_{1}(God)), Sk_{1}(God)))

which we can write down as two separate conclusions:

10a. Event (Sk

_{2}(Sk_{1}(God)))10b. IsPartOf (Sk

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

*v.* In proposition 3 we can eliminate the existentially
quantified variables s & t by introducing two Skolem functors Sk_{3}()
and Sk_{4}(), respectively, each of which depends
on the universally quantified variable x. Thus, 3 becomes:

3a. "x (Event (x) → Space (Sk

_{3}(x)) Λ IsPartOf (Sk_{3}(x), x) Λ Time (Sk_{4}(x)) Λ IsPartOf (Sk_{4}(x), x))

which we can write down as two separate implications:

3b. "x (Event (x) → Space (Sk

_{3}(x)) Λ IsPartOf (Sk_{3}(x), x))3c. "x (Event (x) → Time (Sk

_{4}(x)) Λ IsPartOf (Sk_{4}(x), x))

*vi.* From 10a and 3c we get:

11. Time (Sk

_{4}(Sk_{2}(Sk_{1}(God)))) Λ IsPartOf (Sk_{4}(Sk_{2}(Sk_{1}(God))), Sk_{2}(Sk_{1}(God)))

which we can write down as two separate conclusions:

11a. Time (Sk

_{4}(Sk_{2}(Sk_{1}(God))))11b. IsPartOf (Sk

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

*vii.* From 11a and 4 we get:

12. Material (Sk

_{4}(Sk_{2}(Sk_{1}(God))))

*viii.* From 11b and 5 we get:

13. Material (Sk

_{4}(Sk_{2}(Sk_{1}(God)))) → Material (Sk_{2}(Sk_{1}(God)))

*ix.* From 12 and 13 we get:

14. Material (Sk

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

*x.* In proposition 6 we can reduce the scope of the
negation applying the rule ¬
$x P(x) ↔
"x
¬ P(x). Thus, 6 can be rewritten as:

6a. "x (EntirelyImmaterial (x) → "y ¬ (Material (y) Λ IsPartOf (y, x)))

and further reducing the scope of the negation (using de Morgan’s law) and moving the quantifier of y at the front, we get:

6b. "x "y (EntirelyImmaterial (x) → ¬ Material (y) V ¬ IsPartOf (y, x))

*xi.* From 6b and 8 we get:

15. "y (¬ Material (y) V ¬ IsPartOf (y, God))

*xii.* From 15 and 9b we get:

16. ¬ Material (Sk

_{1}(God))

*xiii.* From 10b and 5 we get:

17. Material (Sk

_{2}(Sk_{1}(God))) → Material (Sk_{1}(God))

*xiv.* From 17 and 16 (using *Modus Tollens*) we
get:

18. ¬ Material (Sk

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

*xv.* Finally, from 18 and 14 we get:

19.

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 and Time”. The prover will find a proof which is essentially the same as the one given above.