List of Main Theorems (Automating Leibniz's Theory of Concepts)

The Theorems for Leibniz's Non-Modal Algebra of Concepts

Theorems 1 – 27 in Zalta 2000 are, for the most part, not needed for the proof of Leibniz's modal metaphysics of concepts. We've left these as exercises. Some of these were already proved as part of the project A Computational Implementation of Leibniz's Paper of 1690, though by taking concepts as primitive rather than by defining Leibnizian concepts as we've done using the theory of abstract objects.

The Theorems for Leibniz's Modal Metaphysics of Individual Concepts

In what follows, we use u,v as restricted variables ranging over ordinary objects, i.e., object x such that O!x. We also use w as a restricted variable ranging over the objects that meet the definition of a possible world. We use the following distinguished elements: d is the distinguished point, and e is the property of being concrete. The properties of being an ordinary object (o) and of being an abstract object (a) are defined in terms of the property of being concrete.

Definition: RealizesAt(u, x, w)

Definition: AppearsAt(x, w)

Definition: IndividualConcept(x)

Definition: The concept of individual u (‘cu’)

Lemmas Used For Automated Proof of Theorem28:

Theorem 28: Lemma 1: RealizesAt(u, cu, wα)

Theorem 28: Lemma 2: (wα ⊨ p)  ≡  p       (World Theory, Theorem 20)

Theorem 28: Lemma 3: PossibleWorld(wα)

Theorem 28: Lemma 4: Pu ≡ wα ⊨ Pu

Theorem 28:

Lemmas Used For Automated Proof of Theorem29:

Theorem 29: Lemma 1: ∃xO!x

Theorem 29: Lemma 2: [No simple way to express this in object theory because the function symbol cu is used and this is essentially a definite description. The indefinite version, c is a concept of individual u, doesn't appear in the paper.]

Theorem 29:

Definition:

Theorem 30: [Exercises]

Lemma Used For Automated Proof of Theorem31:

Theorem 31: Lemma 1: Concept(x) → □Concept(x)

Theorem 31:

Definition:

Corollary (a) to Theorem 31: [Exercise]

Corollary (b) to Theorem 31: [Exercise]

Definition:

Theorem 32:

Theorem 33:

Theorem 34:

Theorem 35:

Definition:

Theorem 36:

Definition:

Theorem 37:

Definition: (The concept of u at w)

Lemmas Used For Automated Proof of Theorem 38:

Theorem 38: Lemma 1: ∀F∃x(x = cF)

Theorem 38: Lemma 2: ∀x(O!x → ∃y(y = cx))

[Exercises]

Theorem 38: Lemma 3
Theorem 38: Lemma 4
Theorem 38: Lemma 5

Theorem 38:

Theorem 39a:

Lemma Used For Automated Proof of Theorem39b:

Theorem 39b, Lemma 1: IndividualConcept(x) → ∀F∀G(Implies(F,G) & xF → xG)

Theorem 39b:

Definition:

Lemmas Used For Automated Proofs of Theorem40a: [Exercises]

Theorem 40a:

Lemmas Used For Automated Proofs of Theorem40b: [Exercises]

Theorem 40b: