Formal God-with-a-Mind Theory, and Proof of its Self-Contradictory State

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.

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 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₁() that depends on the universally quantified variable x. Thus, 1 becomes:

1a. "x (CanRemember (x) → Memory (Sk₁(x)) Λ IsPartOf (Sk₁(x), x))

ii. From 7 and 1a we get:

9. Memory (Sk₁(God)) Λ IsPartOf (Sk₁(God), God)

which we can write down as two separate conclusions:

9a. Memory (Sk₁(God))

9b. IsPartOf (Sk₁(God), God)

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

2a. "x (Memory (x) → Event (Sk₂(x)) Λ IsPartOf (Sk₂(x), x))

iv. From 9a and 2a we get:

10. Event (Sk₂(Sk₁(God))) Λ IsPartOf (Sk₂(Sk₁(God)), Sk₁(God)))

which we can write down as two separate conclusions:

10a. Event (Sk₂(Sk₁(God)))

10b. IsPartOf (Sk₂(Sk₁(God)), Sk₁(God)))

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

3a. "x (Event (x) → Space (Sk₃(x)) Λ IsPartOf (Sk₃(x), x) Λ Time (Sk₄(x)) Λ IsPartOf (Sk₄(x), x))

which we can write down as two separate implications:

3b. "x (Event (x) → Space (Sk₃(x)) Λ IsPartOf (Sk₃(x), x))

3c. "x (Event (x) → Time (Sk₄(x)) Λ IsPartOf (Sk₄(x), x))

vi. From 10a and 3c we get:

11. Time (Sk₄(Sk₂(Sk₁(God)))) Λ IsPartOf (Sk₄(Sk₂(Sk₁(God))), Sk₂(Sk₁(God)))

which we can write down as two separate conclusions:

11a. Time (Sk₄(Sk₂(Sk₁(God))))

11b. IsPartOf (Sk₄(Sk₂(Sk₁(God))), Sk₂(Sk₁(God)))

vii. From 11a and 4 we get:

12. Material (Sk₄(Sk₂(Sk₁(God))))

viii. From 11b and 5 we get:

13. Material (Sk₄(Sk₂(Sk₁(God)))) → Material (Sk₂(Sk₁(God)))

ix. From 12 and 13 we get:

14. Material (Sk₂(Sk₁(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₁(God))

xiii. From 10b and 5 we get:

17. Material (Sk₂(Sk₁(God))) → Material (Sk₁(God))

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

18. ¬ Material (Sk₂(Sk₁(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.

Reload the originating page