## 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)

• Object Theoretic Version: RealizesAt(u, x, w) =dfF((wFu) ≡ xF)
• TPTP Representation:
• ```fof(realizes_in_wrt,definition,
fof(realizes_in_wrt,definition,
(! [D,U,X,W] : ((point(D) & object(U) & object(X) & object(W)) =>
(realizes_in_wrt(U,X,W,D) <=> (world_wrt(W,D) & ex1_wrt(o,U,D)  & ex1_wrt(c,X,D) &
(! [F,P] : ((property(F)  & proposition(P) & plug1(P,F,U)) =>
(true_in_wrt(P,W,D) <=> enc_wrt(X,F,D))))))))).```

Definition: AppearsAt(x, w)

• Object Theoretic Version: AppearsAt(x, w) =dfuRealizesAt(u, x, w)
• TPTP Representation:
• ```fof(appears_in_wrt,definition,
(! [D,X,W] : ((point(D) & object(X) & object(W)) =>
(appears_in_wrt(X,W,D) <=>  (world_wrt(W,D) & ex1_wrt(c,X,D) &
(? [U] : (object(U) & ex1_wrt(o,U,D) & realizes_in_wrt(U,X,W,D)))))))).```

Definition: IndividualConcept(x)

• Object Theoretic Version: IndividualConcept(x) =dfwAppearsAt(x, w)
• TPTP Representation:
• ```fof(individual_concept_wrt,definition,
(! [X,D] : ((object(X) & point(D)) =>
(individual_concept_wrt(X,D) <=>
(? [W] : (object(W) & world_wrt(W,D) & appears_in_wrt(X,W,D))))))).```

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

• Object Theoretic Version: cu =df   ιx(Concept(x) & ∀F(xFFu)), i.e.,
ιx(A!x & ∀F(xFFu))
• TPTP Representation:
• ```fof(concept_of_individual_wrt,definition,
(! [X,U,D] : ((object(X) & object(U) & point(D)) =>
(concept_of_individual_wrt(X,U,D) <=>
(ex1_wrt(c,X,D) & ex1_wrt(o,U,D) & (! [F] : (property(F) =>
(enc_wrt(X,F,D) <=> ex1_wrt(F,U,D))))))))).```
• ```fof(is_the_concept_of_individual_wrt,definition,
(! [X,U,D] : ((object(X) & object(U) & point(D)) =>
(is_the_concept_of_individual_wrt(X,U,D) <=>
(concept_of_individual_wrt(X,U,D) &
(! [Z] : (concept_of_individual_wrt(Z,U,D) => object_equal_wrt(Z,X,D)))))))).```

Lemmas Used For Automated Proof of Theorem28:

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

• TPTP Representation:
```fof(u_realizes_in_wrt_the_concept_of_individual_u,conjecture,
(! [U,X,A] : ((object(U) & object(X) & object(A)) =>
((ex1_wrt(c,X,d) & ex1_wrt(o,U,d) & is_the_actual_world_wrt(A,d)) =>
(is_the_concept_of_individual_wrt(X,U,d)  => realizes_in_wrt(U,X,A,d)))))).```
• Input file: Theorem 28: Lemma 1

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

• TPTP Representation:
```fof(equivalence_truth_in_the_actual_world_and_truth,conjecture,
(! [X] : (object(X) & the_actual_world_wrt(X,d) &
(! [P] : (proposition(P) => (true_in_wrt(P,X,d) <=> true_wrt(P,d))))))).```
• Input file: Theorem 28: Lemma 2

Theorem 28: Lemma 3: PossibleWorld(wα)

• TPTP Representation:
```fof(the_actual_world_is_a_world,conjecture,
(! [X] : (object(X) =>
( is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).```
• Input file: Theorem 28: Lemma 3

Theorem 28: Lemma 4: Puwα ⊨ Pu

• TPTP Representation:
```fof(u_exemplifies_P_iff_plug1_Pu_is_true_in_the_actual_world,conjecture,
(! [P,Q,A,U] : (  (property(P) & proposition(Q) & object(A) & object(U) )  =>
((plug1(Q,P,U) & is_the_actual_world_wrt(A,d)) =>
(ex1_wrt(P,U,d) <=> true_in_wrt(Q,A,d) ) ) ) )).```
• Input file: Theorem 28: Lemma 4

Theorem 28:

• Object Theoretic Version: IndividualConcept(cu)
• TPTP Representation:
• ```fof(theorem28,conjecture,
( ! [U,Z] : ((object(U) & object(Z)) =>
((ex1_wrt(o,U,d) & ex1_wrt(c,Z,d)) =>
(is_the_concept_of_individual_wrt(Z,U,d) =>
individual_concept_wrt(Z,d)))))).```
• Input File: Theorem28

Lemmas Used For Automated Proof of Theorem29:

Theorem 29: Lemma 1: ∃xO!x

• TPTP Representation:
```fof(there_are_ordinary_objects,conjecture,
(? [X] : (object(X) & ex1_wrt(o,X,d)))).```
• Input file: Theorem 29: Lemma 1

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.]

• TPTP Representation:
```fof(any_concept_of_individual_is_an_individual_concept,conjecture,
( ! [U,Z] : ((object(U) & object(Z)) =>
((ex1_wrt(o,U,d) & ex1_wrt(c,Z,d)) =>
(concept_of_individual_wrt(Z,U,d) =>
individual_concept_wrt(Z,d)))))).```
• Input file: Theorem 29: Lemma 2

Theorem 29:

• Object Theoretic Version: ∃x[IndividualConcept(x)]
• TPTP Representation:
• ```fof(there_are_individual_concepts,conjecture,
(? [X] : (object(X) & individual_concept_wrt(X,d)))).```
• Input File: Theorem29

Definition:

• Object Theoretic Version: Mirrors(x, w) =dfp(xyp] ≡ wyp])
• TPTP Representation:
• ```fof(mirrors_wrt,definition,
(! [X,W,D] : ((object(X) & object(W) & point(D)) => (mirrors_wrt(X,W,D) <=>
(! [P] : (proposition(P) =>  (encp_wrt(X,P,D) <=> encp_wrt(W,P,D)))))))).```

Theorem 30: [Exercises]

• Object Theoretic Version: AppearsAt(x, w) → Mirrors(x, w)
• TPTP Representation:
• ```fof(appears_at_implies_mirrors,conjecture,
(! [X,W] : ((object(X) & object(W)) =>
(world_wrt(W,d) =>
(appears_in_wrt(X,W,d) => mirrors_wrt(X,W,d)))))).```
• Input File: [Exercise].

Lemma Used For Automated Proof of Theorem31:

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

• TPTP Representation:
```fof(necessity_of_being_a_concept,conjecture,
(! [X] : ((object(X) =>
(ex1_wrt(c,X,d) => (! [D] : (point(D) => ex1_wrt(c,X,D)))))))).```
• Input file: Theorem 31: Lemma 1

Theorem 31:

• Object Theoretic Version: IndividualConcept(x) → ∃!wAppearsAt(x, w)
• TPTP Representation:
• ```fof(every_individual_concept_appears_at_a_unique_world,conjecture,
(! [C] : (object(C)  =>  (individual_concept_wrt(C,d) =>
(? [W] : (object(W) & world_wrt(W,d) & appears_in_wrt(C,W,d) &
(! [W2] : ((object(W2) & world_wrt(W2,d) & appears_in_wrt(C,W2,d)) =>
W2 = W)))))))).```
• Input File: Theorem31

Definition:

• Object Theoretic Version: The world where individual concept c appears (‘wc’)
• TPTP Representation:
```fof(is_the_world_in_which_appears_wrt,axiom,
(! [W,C,D] : ( ( object(W) & object(C) & point(D) ) =>
(is_the_world_in_which_appears_wrt(W,C,D) <=>
(world_wrt(W,D) & individual_concept_wrt(C,D) & appears_in_wrt(C,W,D) &
(! [W2] : ( ( object(W2) & world_wrt(W2,D) & appears_in_wrt(C,W2,D) ) => W2=W ))))))).```

Corollary (a) to Theorem 31: [Exercise]

• Object Theoretic Version: Mirrors(c, wc)
• TPTP Representation:
• Input File: [Exercise]

Corollary (b) to Theorem 31: [Exercise]

• Object Theoretic Version: c ≽ wc
• TPTP Representation:
• Input File: [Exercise]

Definition:

• Object Theoretic Version: Compossible(c1, c2) =df   ∃w(AppearsAt(c1, w) & AppearsAt(c2, w))
• TPTP Representation:
```fof(compossible_wrt,definition,
(! [X,Y,W,D] : ((object(X) & object(Y) & point(D)) =>
(compossible_wrt(X,Y,D) <=> (individual_concept_wrt(X,D) & individual_concept_wrt(Y,D) &
(? [W] : (object(W) & world_wrt(W,D)  &
appears_in_wrt(X,W,D)  &  appears_in_wrt(Y,W,D)))))))).```

Theorem 32:

• Object Theoretic Version: Compossible(c1, c2) ≡ wc1 = wc2
• TPTP Representation:
```fof(theorem32,conjecture,
(! [C1,C2,W1,W2] : ( (object(C1) & object(C2) & object(W1) & object(W2) ) =>
( (individual_concept_wrt(C1,d) & individual_concept_wrt(C2,d) & world_wrt(W1,d) & world_wrt(W2,d) ) =>
( (is_the_world_in_which_appears_wrt(W1,C1,d) & is_the_world_in_which_appears_wrt(W2,C2,d) ) =>
(compossible_wrt(C1,C2,d) <=> W1 = W2 ) ) ) ) )).```
• Input File: Theorem32

Theorem 33:

• Object Theoretic Version: Compossible(c1, c1)
• TPTP Representation:
```fof(compossibility_is_reflexive,conjecture,
(! [X] : (object(X)  =>
(individual_concept_wrt(X,d)  => compossible_wrt(X,X,d))))).```
• Input File: Theorem33

Theorem 34:

• Object Theoretic Version: Compossible(c1, c2) → Compossible(c2, c1)
• TPTP Representation:
```fof(compossibility_is_symmetric,conjecture,
(! [X,Y] : ((object(X) & object(Y)) =>
((individual_concept_wrt(X,d) & individual_concept_wrt(Y,d)) =>
(compossible_wrt(X,Y,d) => compossible_wrt(Y,X,d)))))).```
• Input File: Theorem34

Theorem 35:

• Object Theoretic Version: Compossible(c1, c2) & Compossible(c2, c3) → Compossible(c1, c3)
• TPTP Representation:
```fof(compossibility_is_transitive,conjecture,
(! [X,Y,Z] : ((object(X) & object(Y) & object(Z)) =>
((individual_concept_wrt(X,d) & individual_concept_wrt(Y,d) & individual_concept_wrt(Z,d)) =>
((compossible_wrt(X,Y,d) & compossible_wrt(Y,Z,d)) => compossible_wrt(X,Z,d)))))).```
• Input File: Theorem35

Definition:

• Object Theoretic Version: Complete(x) =dfF(xFxF)
• TPTP Representation:
```fof(complete_wrt,axiom,
( ! [X,D] : ((object(X) & point(D)) =>
(complete_wrt(X,D)  <=> (! [F,G] : ((property(F) & property(G) & a_property_negation_of(G,F)) =>
(enc_wrt(X,F,D) | enc_wrt(X,G,D)))))))).```

Theorem 36:

• Object Theoretic Version: IndividualConcept(x) → Complete(x)
• TPTP Representation:
```fof(individual_concepts_are_complete,conjecture,
( ! [X] : ( object(X) =>
( individual_concept_wrt(X,d) => complete_wrt(X,d) ) ) )).```
• Input File: Theorem36

Definition:

• Object Theoretic Version: Singular(x) =dfu, v, w(RealizesAt(u, x, w) & RealizesAt(v, x, w) → u=v)
• TPTP Representation:
```fof(singular_wrt,axiom,
( ! [X,U,V,W,D] : ((object(X) & object(U) & object(V) & object(W) & point(D)) =>
(singular_wrt(X,D)  <=> (ex1_wrt(o,U,D) & ex1_wrt(o,V,D) & world_wrt(W,D) &
((realizes_in_wrt(U,X,W,D) & realizes_in_wrt(V,X,W,D)) => U=V)))))).```

Theorem 37:

• Object Theoretic Version: IndividualConcept(x) → Singular(x)
• TPTP Representation:
```fof(individual_concepts_are_singular,conjecture,
( ! [X] : ( object(X) =>
( individual_concept_wrt(X,d) => singular_wrt(X,d) ) ) )).```
• Input File: Theorem37

Definition: (The concept of u at w)

• Object Theoretic Version: cwu =df ιx(Concept(x) & ∀F(xF ≡ (w ⊨ Fu))), i.e.,
ιx(A!x & ∀F(xF ≡ (w ⊨ Fu)))
• TPTP Representation:
```fof(is_the_concept_of_individual_in_wrt,axiom,
(! [X,U,Y,D,Q] : ((object(X) & object(U) & object(Y) & point(D) & property(Q)) =>
(is_the_concept_of_individual_in_wrt(X,U,Y,D) <=>
(concept_of_individual_in_wrt(X,U,Y,D) &
(! [Z] : (concept_of_individual_in_wrt(Z,U,Y,D) => object_equal_wrt(Z,X,D)))))))).```
```fof(concept_of_individual_in_wrt,axiom,
(! [X,U,D,W] : ( (object(X) & object(U) & point(D) & object(W)) =>
( concept_of_individual_in_wrt(X,U,W,D) <=>
( world_wrt(W,D) & ex1_wrt(c,X,D) & realizes_in_wrt(U,X,W,D) ) ) ) )).```

Lemmas Used For Automated Proof of Theorem 38:

Theorem 38: Lemma 1: ∀Fx(x = cF)

• TPTP Representation:
```fof(existence_of_is_the_concept_of_wrt,lemma,
(! [F] : (property(F) => (? [X] : (object(X) &
is_the_concept_of_wrt(X,F,d)))))).```
• Input file: Theorem 38: Lemma 1

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

• TPTP Representation:
```fof(existence_of_the_concept_of_individual_wrt,conjecture,
(! [U] : (object(U) => (ex1_wrt(o,U,d) =>
(? [X] : (object(X) & ex1_wrt(c,X,d) & is_the_concept_of_individual_wrt(X,U,d))))))).```
• Input file: Theorem 38: Lemma 2

[Exercises]

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

Theorem 38:

• Object Theoretic Version: Fucu ≽ cF
• TPTP Representation:
```fof(theorem38,conjecture,
(! [U,F] : ((object(U) & property(F)) =>
(ex1_wrt(o,U,d) =>
(? [Y,Z] : (object(Y) & object(Z) & ex1_wrt(c,Y,d) & ex1_wrt(c,Z,d) &
is_the_concept_of_individual_wrt(Y,U,d) & is_the_concept_of_wrt(Z,F,d) &
(ex1_wrt(F,U,d)  <=> contains_wrt(Y,Z,d)))))))).```
• Input File: Theorem38

Theorem 39a:

• Object Theoretic Version: cuFcu ≽ cF
• TPTP Representation:
```fof(theorem39a,conjecture,
(! [U,F] : ((object(U) & property(F) & ex1_wrt(o,U,d)) =>
(? [Y,Z] : (object(Y) & object(Z)  & ex1_wrt(c,Y,d) & ex1_wrt(c,Z,d) &
is_the_concept_of_individual_wrt(Y,U,d) &
is_the_concept_of_wrt(Z,F,d) &
(enc_wrt(Y,F,d) <=> contains_wrt(Y,Z,d))))))).```
• Input File: Theorem39a

Lemma Used For Automated Proof of Theorem39b:

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

• TPTP Representation:
```fof(ind_concept_encodes_properties_implied_by_what_it_encodes,lemma,
(! [X] : ((object(X) & ex1_wrt(c,X,d) & individual_concept_wrt(X,d))  =>
(! [F,G] : ((property(F) & property(G)) =>
((implies(F,G) & enc_wrt(X,F,d)) => enc_wrt(X,G,d))))))).```
• Input file: Theorem 39b, Lemma 1

Theorem 39b:

• Object Theoretic Version: IndividualConcept(x) → ∀F(xFx ≽ cF)
• TPTP Representation:
```fof(theorem39b,conjecture,
(! [X] : ((object(X) & ex1_wrt(c,X,d) & individual_concept_wrt(X,d))  =>
(! [F] : (property(F) =>
(? [Y] : (object(Y) & ex1_wrt(c,Y,d) & is_the_concept_of_wrt(Y,F,d) &
(enc_wrt(X,F,d) <=> contains_wrt(X,Y,d))))))))).
```
• Input File: Theorem39b

Definition:

• Object Theoretic Version: Counterparts(c, c′) =dfuw1w2(c = cw1u & c′ = cw2u)
• TPTP Representation:
```fof(counterparts_wrt,definition,
(! [X,Y,U,Z,W,D] : ((object(X) & object(Y) & object(U) & object(Z) & object(W) & point(D)) =>
(counterparts_wrt(X,Y,D) <=>
(ex1_wrt(c,X,D) & ex1_wrt(c,Y,D) & ex1_wrt(o,U,D) & world_wrt(Z,D) & world_wrt(W,D) &
is_the_concept_of_individual_in_wrt(X,U,Z,D) & is_the_concept_of_individual_in_wrt(Y,U,W,D)))))).```

Lemmas Used For Automated Proofs of Theorem40a: [Exercises]

Theorem 40a:

• Object Theoretic Version:
• TPTP Representation:
```fof(theorem_40a,conjecture,
(! [U,F] : ((object(U) & property(F)) =>
((ex1_wrt(o,U,d) & ex1_wrt(F,U,d) &
(? [D] : (point(D) & ~ex1_wrt(F,U,D)))) =>
(? [X,Y] : (object(X) & object(Y) &  ex1_wrt(c,X,d) &
ex1_wrt(c,Y,d) & is_the_concept_of_individual_wrt(X,U,d) &
is_the_concept_of_wrt(Y,F,d) & contains_wrt(X,Y,d) &
(? [Z] : (object(Z) & ex1_wrt(c,Z,d) &
counterparts_wrt(Z,X,d) & ~contains_wrt(Z,Y,d) &
(? [A,W] : (object(A) & object(W) &
is_the_actual_world_wrt(A,d) & world_wrt(W,d) &
~equal_wrt(W,A,d) & appears_in_wrt(Z,W,d))))))))))).```
• Input File: Theorem40a

Lemmas Used For Automated Proofs of Theorem40b: [Exercises]

Theorem 40b:

• Object Theoretic Version:
• TPTP Representation:
```fof(theorem_40a,conjecture,
(! [U,F] : ((object(U) & property(F)) =>
((ex1_wrt(o,U,d) & ~ex1_wrt(F,U,d) &
(? [D] : (point(D) & ex1_wrt(F,U,D)))) =>
(? [X,Y] : (object(X) & object(Y) &  ex1_wrt(c,X,d) &
ex1_wrt(c,Y,d) & is_the_concept_of_individual_wrt(X,U,d) &
is_the_concept_of_wrt(Y,F,d) & ~contains_wrt(X,Y,d) &
(? [Z] : (object(Z) & ex1_wrt(c,Z,d) &
counterparts_wrt(Z,X,d) & contains_wrt(Z,Y,d) &
(? [A,W] : (object(A) & object(W) &
is_the_actual_world_wrt(A,d) & world_wrt(W,d) &
~equal_wrt(W,A,d) & appears_in_wrt(Z,W,d))))))))))).```
• Input File: Theorem40b