A (Leibnizian) theory of concepts

Contents

  1. Axioms
  2. Definitions
  3. Sorting
  4. Lemmas
  5. Theorems
  6. Symbols
  7. Consistency Check

unproved lemmas

Undefined terms appearing in proofs

See a later section. Make sure that that list contains only truly primitive predicates, such as ex1_wrt.

Axioms

being_a_concept_is_being_abstract
Comment: The property of being a concept is defined to be the property of being abstract
Representation: c = a
Used in the proof of:
existence_vac
Comment: To every proposition there corresponds a property which is its vacuous expansion
Representation: ∀P(proposition(P) ⟶ ∃Q((property(Q) ∧ is_being_such_that(Q,P))))
Used in the proof of:
truth_wrt_vac
Comment: The 1-place exemplification conditions wrt a point for a property (Q) of being such that P
Representation: ∀P,Q((proposition(P) ∧ property(Q)) ⟶ is_being_such_that(Q,P) ⟶ ∀D,X((point(D) ∧ object(X)) ⟶ (ex1_wrt(Q,X,D) ⟷ true_wrt(P,D))))
Used in the proof of: (nothing)
rigidity_of_encoding
Comment: (nothing to say).
Representation: ∀X,F((object(X) ∧ property(F)) ⟶ ∃D((point(D) ∧ enc_wrt(X,F,D))) ⟶ ∀D(point(D) ⟶ enc_wrt(X,F,D)))
Used in the proof of:
existence_proposition_plug1
Comment: (nothing to say).
Representation: ∀X,F((object(X) ∧ property(F)) ⟶ ∃P((proposition(P) ∧ plug1(P,F,X))))
Used in the proof of:
proposition_plug1_truth
Comment: (nothing to say).
Representation: ∀X,F,P((object(X) ∧ (property(F) ∧ proposition(P))) ⟶ plug1(P,F,X) ⟶ ∀D(point(D) ⟶ (true_wrt(P,D) ⟷ ex1_wrt(F,X,D))))
Used in the proof of:
necessarily_a_equal_wrt_implies_identity
Comment: (nothing to say).
Representation: ∀X,Y((object(X) ∧ object(Y)) ⟶ ∀D(point(D) ⟶ a_equal_wrt(X,Y,D)) ⟶ X = Y)
Used in the proof of:
necessarily_o_equal_wrt_implies_identity
Comment: (nothing to say).
Representation: ∀X,Y((object(X) ∧ object(Y)) ⟶ ∀D(point(D) ⟶ o_equal_wrt(X,Y,D)) ⟶ X = Y)
Used in the proof of:
comprehension_for_concept_of_individual_wrt
Comment: (nothing to say).
Representation: ∀D(point(D) ⟶ ∀U((object(U) ∧ ex1_wrt(o,U,D)) ⟶ ∃X((object(X) ∧ (ex1_wrt(a,X,D) ∧ ∀F(property(F) ⟶ (enc_wrt(X,F,D) ⟷ ex1_wrt(F,U,D))))))))
Used in the proof of:
property_of_necfalse
Comment: (nothing to say).
Representation: ∀D(point(D) ⟶ ¬true_wrt(necfalse,D))
Used in the proof of: (nothing)
sort_world
Comment: (nothing to say).
Representation: ∀W,D(world_wrt(W,D) ⟶ (object(W) ∧ point(D)))
Used in the proof of:
instance_of_comprehension_for_an_actual_world
Comment: (nothing to say).
Representation: ∀D(point(D) ⟶ ∃X((object(X) ∧ (ex1_wrt(a,X,D) ∧ ∀F(property(F) ⟶ (enc_wrt(X,F,D) ⟷ ∃P((proposition(P) ∧ (true_wrt(P,D) ∧ is_being_such_that(F,P))))))))))
Used in the proof of:
universalized_comprehension_instance_38_1
Comment: (nothing to say).
Representation: ∀G(property(G) ⟶ ∃Z((object(Z) ∧ (ex1_wrt(a,Z,d) ∧ ∀F(property(F) ⟶ (enc_wrt(Z,F,d) ⟷ implies_wrt(G,F,d)))))))
Used in the proof of:
instance_of_comprehension_for_concept_of_individual_in_wrt
Comment: (nothing to say).
Representation: ∀U,W((object(U) ∧ object(W)) ⟶ (ex1_wrt(o,U,d) ∧ world_wrt(W,d)) ⟶ ∀D(point(D) ⟶ ∃X((object(X) ∧ (ex1_wrt(a,X,D) ∧ ∀F(property(F) ⟶ (enc_wrt(X,F,D) ⟷ that_ordinary_object_ex1_property_is_true_in_wrt(F,U,W,D))))))))
Used in the proof of:
proposition_negations_exist
Comment: (nothing to say).
Representation: ∀P(proposition(P) ⟶ ∃Q((proposition(Q) ∧ is_a_negation_of(Q,P))))
Used in the proof of:
proposition_negation_truth
Comment: (nothing to say).
Representation: ∀P,Q((proposition(P) ∧ proposition(Q)) ⟶ is_a_negation_of(Q,P) ⟶ ∀D(point(D) ⟶ (true_wrt(Q,D) ⟷ ¬true_wrt(P,D))))
Used in the proof of:
possible_existence_of_concrete_object
Comment: (nothing to say).
Representation: ∃D, X((point(D) ∧ (object(X) ∧ ex1_wrt(e,X,D))))
Used in the proof of:
possibly_there_are_concrete_objects
Comment: (nothing to say).
Representation: ∃D((point(D) ∧ ∃X((object(X) ∧ ex1_wrt(e,X,D)))))
Used in the proof of:
theorem7_world_theory
Comment: (nothing to say).
Representation: ∀P,R,X,W,D,Q((object(W) ∧ (proposition(P) ∧ (proposition(R) ∧ (object(X) ∧ (point(D) ∧ property(Q)))))) ⟶ (world_wrt(W,D) ∧ (is_being_such_that(Q,P) ∧ plug1(R,Q,X))) ⟶ (true_in_wrt(P,W,D) ⟷ true_in_wrt(R,W,D)))
Used in the proof of:
existence_of_plug1_propositions
Comment: (nothing to say).
Representation: ∀X,F((object(X) ∧ property(F)) ⟶ ∃P((proposition(P) ∧ plug1(P,F,X))))
Used in the proof of:
truth_of_plug1_propositions
Comment: (nothing to say).
Representation: ∀X,F,P((object(X) ∧ (property(F) ∧ proposition(P))) ⟶ plug1(P,F,X) ⟶ ∀D(point(D) ⟶ (true_wrt(P,D) ⟷ ex1_wrt(F,X,D))))
Used in the proof of:
def_ex1
Comment: (nothing to say).
Representation: ∀X,F((ex1(F,X) ⟷ ex1_wrt(F,X,d)))
Used in the proof of: (nothing)
def_enc
Comment: (nothing to say).
Representation: ∀X,F((enc(X,F) ⟷ enc_wrt(X,F,d)))
Used in the proof of: (nothing)
distinguished_proposition_necfalse
Comment: (nothing to say).
Representation: proposition(necfalse)
Used in the proof of: (nothing)
sort_true_in_wrt
Comment: (nothing to say).
Representation: ∀P,X,D(true_in_wrt(P,X,D) ⟶ (proposition(P) ∧ (object(X) ∧ point(D))))
Used in the proof of:

Definitions

o
Comment: The definition of the property of being ordinary
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (ex1_wrt(o,X,D) ⟷ ∃D2((point(D2) ∧ ex1_wrt(e,X,D2)))))
Used in the proof of:
a
Comment: The definition of the property of being abstract
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (ex1_wrt(a,X,D) ⟷ ¬∃D2((point(D2) ∧ ex1_wrt(e,X,D2)))))
Used in the proof of:
ex1
Comment: (nothing to say).
Representation: ∀X,F((ex1(F,X) ⟷ ex1_wrt(F,X,d)))
Used in the proof of:
enc
Comment: Encoding simpliciter is encoding with respect to the distinguished point
Representation: ∀X,F((enc(X,F) ⟷ enc_wrt(X,F,d)))
Used in the proof of:
o_equal_wrt
Comment: The definition of identity for ordinary objects with respect to a point
Representation: ∀X,Y,D((object(X) ∧ (object(Y) ∧ point(D))) ⟶ (o_equal_wrt(X,Y,D) ⟷ (ex1_wrt(o,X,D) ∧ (ex1_wrt(o,Y,D) ∧ ∀D2(point(D2) ⟶ ∀F(property(F) ⟶ (ex1_wrt(F,X,D2) ⟷ ex1_wrt(F,Y,D2))))))))
Used in the proof of:
o_equal
Comment: The definition of identity for ordinary objects
Representation: ∀X,Y((object(X) ∧ object(Y)) ⟶ (o_equal(X,Y) ⟷ o_equal_wrt(X,Y,d)))
Used in the proof of:
a_equal_wrt
Comment: The definition of identity for abstract objects with respect to a point
Representation: ∀X,Y,D((object(X) ∧ (object(Y) ∧ point(D))) ⟶ (a_equal_wrt(X,Y,D) ⟷ (ex1_wrt(a,X,D) ∧ (ex1_wrt(a,Y,D) ∧ ∀D2(point(D2) ⟶ ∀F(property(F) ⟶ (enc_wrt(X,F,D2) ⟷ enc_wrt(Y,F,D2))))))))
Used in the proof of:
a_equal
Comment: The definition of identity for abstract objects
Representation: ∀X,Y((object(X) ∧ object(Y)) ⟶ (a_equal(X,Y) ⟷ a_equal_wrt(X,Y,d)))
Used in the proof of:
object_equal_wrt
Comment: The definition of identity for objects with respect to a point
Representation: ∀X,Y,D((object(X) ∧ (object(Y) ∧ point(D))) ⟶ (object_equal_wrt(X,Y,D) ⟷ (o_equal_wrt(X,Y,D) ∨ a_equal_wrt(X,Y,D))))
Used in the proof of:
object_equal
Comment: The definition of identity for objects
Representation: ∀X,Y((object(X) ∧ object(Y)) ⟶ (object_equal(X,Y) ⟷ object_equal_wrt(X,Y,d)))
Used in the proof of:
encp_wrt
Comment: Encoding of propositions is defined in terms of encoding of properties
Representation: ∀X,P,D((object(X) ∧ (proposition(P) ∧ point(D))) ⟶ (encp_wrt(X,P,D) ⟷ ∃F((property(F) ∧ (is_being_such_that(F,P) ∧ enc_wrt(X,F,D))))))
Used in the proof of:
true_in_wrt
Comment: The definition of a proposition being true in a world with respect to a point
Representation: ∀P,X,D((proposition(P) ∧ (object(X) ∧ point(D))) ⟶ (true_in_wrt(P,X,D) ⟷ (situation_wrt(X,D) ∧ encp_wrt(X,P,D))))
Used in the proof of:
appears_in_wrt
Comment: (nothing to say).
Representation: ∀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))))))))
Used in the proof of:
concept_of_individual_in_wrt
Comment: (nothing to say).
Representation: ∀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(o,U,D) ∧ (ex1_wrt(c,X,D) ∧ realizes_in_wrt(U,X,W,D))))))
Used in the proof of:
is_the_concept_of_individual_in_wrt
Comment: (nothing to say).
Representation: ∀X,U,Y,D((object(X) ∧ (object(U) ∧ (object(Y) ∧ point(D)))) ⟶ (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)))))
Used in the proof of:
realizes_in_wrt
Comment: (nothing to say).
Representation: ∀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))))))))
Used in the proof of:
included_in_wrt
Comment: (nothing to say).
Representation: ∀X,Y,D((object(X) ∧ (object(Y) ∧ point(D))) ⟶ (included_in_wrt(X,Y,D) ⟷ (ex1_wrt(c,X,D) ∧ (ex1_wrt(c,Y,D) ∧ ∀F(property(F) ⟶ enc_wrt(X,F,D) ⟶ enc_wrt(Y,F,D))))))
Used in the proof of:
is_an_actual_world_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (is_an_actual_world_wrt(X,D) ⟷ (world_wrt(X,D) ∧ actual_wrt(X,D))))
Used in the proof of:
actual_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (actual_wrt(X,D) ⟷ (situation_wrt(X,D) ∧ ∀P(proposition(P) ⟶ true_in_wrt(P,X,D) ⟶ true_wrt(P,D)))))
Used in the proof of:
is_the_actual_world_wrt
Comment: The definition the property of being the unique actual world with respect to a point
Representation: ∀X,D((point(D) ∧ object(X)) ⟶ (is_the_actual_world_wrt(X,D) ⟷ (is_an_actual_world_wrt(X,D) ∧ ∀Y((object(Y) ∧ is_an_actual_world_wrt(Y,D)) ⟶ object_equal_wrt(X,Y,D)))))
Used in the proof of:
individual_concept_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (individual_concept_wrt(X,D) ⟷ ∃W((object(W) ∧ (world_wrt(W,D) ∧ appears_in_wrt(X,W,D))))))
Used in the proof of:
concept_of_individual_wrt
Comment: (nothing to say).
Representation: ∀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)))))))
Used in the proof of:
is_the_concept_of_individual_wrt
Comment: (nothing to say).
Representation: ∀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)))))
Used in the proof of:
sum_of_wrt
Comment: (nothing to say).
Representation: ∀X,Y,Z,D((object(X) ∧ (object(Y) ∧ (object(Z) ∧ point(D)))) ⟶ (sum_of_wrt(Z,X,Y,D) ⟷ (ex1_wrt(c,Z,D) ∧ ∀F(property(F) ⟶ (enc_wrt(Z,F,D) ⟷ (enc_wrt(X,F,D) ∨ enc_wrt(Y,F,D)))))))
Used in the proof of:
is_being_such_that
Comment: (nothing to say).
Representation: ∀P,Q((proposition(P) ∧ property(Q)) ⟶ (is_being_such_that(Q,P) ⟷ ∀D(point(D) ⟶ ∀X(object(X) ⟶ (ex1_wrt(Q,X,D) ⟷ true_wrt(P,D))))))
Used in the proof of: (nothing)
implies_wrt
Comment: (nothing to say).
Representation: ∀F,G,D((property(F) ∧ (property(G) ∧ point(D))) ⟶ (implies_wrt(F,G,D) ⟷ ∀D1(point(D1) ⟶ ∀X(object(X) ⟶ ex1_wrt(F,X,D1) ⟶ ex1_wrt(G,X,D1)))))
Used in the proof of:
implies
Comment: (nothing to say).
Representation: ∀F,G((property(F) ∧ property(G)) ⟶ (implies(F,G) ⟷ implies_wrt(F,G,d)))
Used in the proof of:
is_the_sum_of_wrt
Comment: (nothing to say).
Representation: ∀X,Y,Z,D((object(X) ∧ (object(Y) ∧ (object(Z) ∧ point(D)))) ⟶ (is_the_sum_of_wrt(Z,X,Y,D) ⟷ (sum_of_wrt(Z,X,Y,D) ∧ ∀W(object(W) ⟶ sum_of_wrt(W,X,Y,D) ⟶ object_equal_wrt(W,Z,D)))))
Used in the proof of:
a_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (ex1_wrt(a,X,D) ⟷ ¬∃D2((point(D2) ∧ ex1_wrt(e,X,D2)))))
Used in the proof of:
o_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (ex1_wrt(o,X,D) ⟷ ∃D2((point(D2) ∧ ex1_wrt(e,X,D2)))))
Used in the proof of:
counterparts_wrt
Comment: (nothing to say).
Representation: ∀X,Y,D((object(X) ∧ (object(Y) ∧ point(D))) ⟶ (counterparts_wrt(Y,X,D) ⟷ (ex1_wrt(c,X,D) ∧ (ex1_wrt(c,Y,D) ∧ ∃U, Z, W((object(U) ∧ (object(Z) ∧ (object(W) ∧ (ex1_wrt(o,U,D) ∧ (world_wrt(Z,D) ∧ (world_wrt(W,D) ∧ (is_the_concept_of_individual_in_wrt(Y,U,W,D) ∧ is_the_concept_of_individual_in_wrt(X,U,Z,D)))))))))))))
Used in the proof of:
world_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (world_wrt(X,D) ⟷ (situation_wrt(X,D) ∧ ∃D2((point(D2) ∧ ∀P(proposition(P) ⟶ (true_in_wrt(P,X,D) ⟷ true_wrt(P,D2))))))))
Used in the proof of:
concept_of_wrt
Comment: (nothing to say).
Representation: ∀Z,G,D((object(Z) ∧ (property(G) ∧ point(D))) ⟶ (concept_of_wrt(Z,G,D) ⟷ (ex1_wrt(c,Z,D) ∧ ∀F(property(F) ⟶ (enc_wrt(Z,F,D) ⟷ implies_wrt(G,F,D))))))
Used in the proof of:
is_the_concept_of_wrt
Comment: (nothing to say).
Representation: ∀Z,G,D((object(Z) ∧ (property(G) ∧ point(D))) ⟶ (is_the_concept_of_wrt(Z,G,D) ⟷ (concept_of_wrt(Z,G,D) ∧ ∀Y(object(Y) ⟶ concept_of_wrt(Y,G,D) ⟶ object_equal_wrt(Y,Z,D)))))
Used in the proof of:
contains_wrt
Comment: (nothing to say).
Representation: ∀X,Y,D((object(X) ∧ (object(Y) ∧ point(D))) ⟶ (contains_wrt(Y,X,D) ⟷ included_in_wrt(X,Y,D)))
Used in the proof of:
that_ordinary_object_ex1_property_is_true_in_wrt
Comment: (nothing to say).
Representation: ∀F,U,W,D((property(F) ∧ (object(U) ∧ (object(W) ∧ point(D)))) ⟶ (that_ordinary_object_ex1_property_is_true_in_wrt(F,U,W,D) ⟷ (world_wrt(W,D) ∧ (ex1_wrt(o,U,D) ∧ ∃P((proposition(P) ∧ (plug1(P,F,U) ∧ true_in_wrt(P,W,D))))))))
Used in the proof of:
negated_propositions
Comment: (nothing to say).
Representation: ∀P,Q((proposition(P) ∧ proposition(Q)) ⟶ (is_a_negation_of(Q,P) ⟷ ∀D(point(D) ⟶ (¬true_wrt(Q,D) ⟷ true_wrt(P,D)))))
Used in the proof of:
mirrors_wrt
Comment: (nothing to say).
Representation: ∀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)))))
Used in the proof of:
compossible_wrt
Comment: (nothing to say).
Representation: ∀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)))))))))
Used in the proof of:
is_the_world_in_which_appears_wrt
Comment: (nothing to say).
Representation: ∀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))))))
Used in the proof of:
compossibility_wrt
Comment: (nothing to say).
Representation: ∀X,Y,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)))))))))
Used in the proof of:
situation_wrt
Comment: (nothing to say).
Representation: ∀X,D((object(X) ∧ point(D)) ⟶ (situation_wrt(X,D) ⟷ (ex1_wrt(a,X,D) ∧ ∀F(property(F) ⟶ enc_wrt(X,F,D) ⟶ ∃P((proposition(P) ∧ is_being_such_that(F,P)))))))
Used in the proof of:
complete_wrt
Comment: (nothing to say).
Representation: ∀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)))))
Used in the proof of:
property_negation
Comment: (nothing to say).
Representation: ∀F,G((property(F) ∧ property(G)) ⟶ (a_property_negation_of(G,F) ⟷ ∀X,D((point(D) ∧ object(X)) ⟶ (ex1_wrt(G,X,D) ⟷ ¬ex1_wrt(F,X,D)))))
Used in the proof of:
haecceity_of_wrt
Comment: (nothing to say).
Representation: ∀P,X,D((point(D) ∧ (object(X) ∧ property(P))) ⟶ (haecceity_of_wrt(P,X,D) ⟷ (ex1_wrt(o,X,D) ∧ ∀Y(object(Y) ⟶ (ex1_wrt(P,Y,D) ⟷ o_equal_wrt(Y,X,D))))))
Used in the proof of:
singular_wrt
Comment: (nothing to say).
Representation: ∀D(point(D) ⟶ ∀X(object(X) ⟶ (singular_wrt(X,D) ⟷ (ex1_wrt(c,X,D) ∧ ∀W(object(W) ⟶ world_wrt(W,D) ⟶ ∀U,V((object(U) ∧ object(V)) ⟶ (ex1_wrt(o,U,D) ∧ ex1_wrt(o,V,D)) ⟶ (realizes_in_wrt(U,X,W,D) ∧ realizes_in_wrt(V,X,W,D)) ⟶ U = V))))))
Used in the proof of:

Sorting

sort_is_an_actual_world_wrt
Comment: (nothing to say).
Representation: ∀X,D(is_an_actual_world_wrt(X,D) ⟶ (object(X) ∧ point(D)))
Used in the proof of:
sort_plug1
Comment: (nothing to say).
Representation: ∀P,F,X(plug1(P,F,X) ⟶ (object(X) ∧ (property(F) ∧ proposition(P))))
Used in the proof of: (nothing)
lemma_kinds_for_the_concept_of_individual_in
Comment: (nothing to say).
Representation: ∀X,Y,Z,W(is_the_concept_of_individual_in_wrt(X,Y,Z,W) ⟶ (ex1_wrt(c,X,d) ∧ (ex1_wrt(o,Y,d) ∧ (world_wrt(Z,d) ∧ point(W)))))
Used in the proof of: (nothing)
distinguished_point_d
Comment: The distinguished point in the underlying modal logic
Representation: point(d)
Used in the proof of:
sort_properties_not_points
Comment: (nothing to say).
Representation: ∀X(property(X) ⟶ ¬point(X))
Used in the proof of:
sort_properties_not_objects
Comment: (nothing to say).
Representation: ∀X(property(X) ⟶ ¬object(X))
Used in the proof of: (nothing)
sort_propositions_not_points
Comment: (nothing to say).
Representation: ∀X(proposition(X) ⟶ ¬point(X))
Used in the proof of: (nothing)
sort_propositions_not_objects
Comment: (nothing to say).
Representation: ∀X(proposition(X) ⟶ ¬object(X))
Used in the proof of: (nothing)
sort_propositions_not_properties
Comment: (nothing to say).
Representation: ∀X(proposition(X) ⟶ ¬property(X))
Used in the proof of: (nothing)
sort_points_not_objects
Comment: (nothing to say).
Representation: ∀X(point(X) ⟶ ¬object(X))
Used in the proof of: (nothing)
sort_ex1_wrt
Comment: The relata of 1-place exemplification with respect to a point are sorted
Representation: ∀F,X,D(ex1_wrt(F,X,D) ⟶ (property(F) ∧ (object(X) ∧ point(D))))
Used in the proof of:
sort_enc_wrt
Comment: The relata of encoding predication with respect to a point are sorted
Representation: ∀X,F,D(enc_wrt(X,F,D) ⟶ (object(X) ∧ (property(F) ∧ point(D))))
Used in the proof of:
sort_concept_of_individual_in_wrt
Comment: (nothing to say).
Representation: ∀X,U,W,D(concept_of_individual_in_wrt(X,U,W,D) ⟶ (object(X) ∧ (object(U) ∧ (object(W) ∧ point(D)))))
Used in the proof of:
sort_concept_of_individual_wrt
Comment: (nothing to say).
Representation: ∀X,U,D(concept_of_individual_wrt(X,U,D) ⟶ (object(X) ∧ (object(U) ∧ point(D))))
Used in the proof of:
sort_is_the_concept_of_individual_wrt
Comment: (nothing to say).
Representation: ∀X,U,D(is_the_concept_of_individual_wrt(X,U,D) ⟶ (object(X) ∧ (object(U) ∧ point(D))))
Used in the proof of: (nothing)
sort_individual_concept_wrt
Comment: (nothing to say).
Representation: ∀X,D(individual_concept_wrt(X,D) ⟶ (object(X) ∧ point(D)))
Used in the proof of:
distinguished_property_e
Comment: The primitive property of concreteness
Representation: property(e)
Used in the proof of:
sort_is_the_sum_of_wrt
Comment: (nothing to say).
Representation: ∀X,Y,Z,D(is_the_sum_of_wrt(Z,X,Y,D) ⟶ (object(X) ∧ (object(Y) ∧ (object(Z) ∧ point(D)))))
Used in the proof of:
sort_implies_wrt
Comment: (nothing to say).
Representation: ∀F,G,D(implies_wrt(F,G,D) ⟶ (property(F) ∧ (property(G) ∧ point(D))))
Used in the proof of:
sort_is_the_concept_of_wrt
Comment: (nothing to say).
Representation: ∀X,F,D(is_the_concept_of_wrt(X,F,D) ⟶ (ex1_wrt(c,X,D) ∧ (object(X) ∧ (property(F) ∧ point(D)))))
Used in the proof of:

Lemmas

u_realizes_in_wrt_the_concept_of_individual_u
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
equivalence_truth_in_the_actual_world_and_truth
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
the_actual_world_is_a_world
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
u_exemplifies_P_iff_plug1_Pu_is_true_in_the_actual_world
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
the_concept_of_individual_wrt_and_the_concept_of_individual_in_wrt_are_counterparts
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
existence_of_is_the_concept_of_wrt
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
existence_of_the_concept_of_individual_wrt
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
theorem38
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
existence_and_property_of_the_concept_of_individual_in_wrt
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
if_Z_does_not_encode_F_then_Z_does_not_contain_the_concept_of_F
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
the_concept_of_individual_in_w_wrt_appears_in_w_wrt
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
possibly_not_Fu_implies_a_world_where_not_Fu_is_true
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
facts_about_negated_propositions_and_true_in_wrt
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
not_f_u_implies_not_f_u_is_true_in_the_actual_world
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
f_u_implies_f_u_is_true_in_the_actual_world
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
true_in_A_but_not_true_in_B_then_A_not_B
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
the_actual_world_exists
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
an_actual_world_exists
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
the_concept_of_F_wrt_encodes_G_if_and_only_F_implies_G
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
the_concept_of_individual_wrt_encodes_exactly_what_it_exemplifies
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
uniqueness_of_concept_of_individual_in_wrt
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
any_concept_of_individual_wrt_encodes_exactly_what_it_exemplifies
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
possibly_Fu_implies_a_world_where_Fu_is_true
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
if_the_concept_of_individual_u_in_w_wrt_does_encode_K_then_it_does_contain_the_concept_K
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
lemma_concept_of_individual_wrt
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
sum_lemma
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
there_are_ordinary_objects
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
any_concept_of_individual_is_an_individual_concept
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
necessity_of_being_a_concept
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
an_individual_concept_mirrors_the_world_in_which_it_appears
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
co_realizers_are_identical
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
possibly_o_equal_wrt_implies_necessarily_o_equal_wrt
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
Actions:
existence_of_haecceity_for_ordinary_objects
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
(logical truth)
Actions:
co_realizers_are_ordinary_object_equal
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
co_realizers_co_exemplify
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
the_concept_of_an_individual_is_its_concept_in_the_actual_world
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
kinds_for_truth_in
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
being_abstract_and_being_ordinary_are_mutually_exclusive
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:

Theorems

theorem01
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem02
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem03
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem04
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem05
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem28
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
principia_019
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem_40a
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem_40b
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
possibly_p_iff_there_is_a_world_where_p_is_true
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of:
(logical truth)
Actions:
theorem39a
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem39b
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
ind_concept_encodes_properties_implied_by_what_it_encodes
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
theorem06
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
theorem07
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
there_are_individual_concepts
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
appears_at_implies_mirrors
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
every_individual_concept_appears_at_a_unique_world
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of:
Actions:
theorem32
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
compossibility_is_reflexive
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
an_individual_concept_contains_the_world_in_which_it_appears
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
compossibility_is_symmetric
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
compossibility_is_transitive
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
individual_concepts_are_complete
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
individual_concepts_are_singular
Comment: (see TPTP representation below).
Dependencies:
Raw TPTP representation:
Used in the proof of: (nothing)
Actions:
distinguished_property_a
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of: (nothing)
(logical truth)
Actions:
distinguished_property_o
Comment: (see TPTP representation below).
Dependencies: (none)
Raw TPTP representation:
Used in the proof of: (nothing)
(logical truth)
Actions:

Symbols

Constants (function symbols of arity 0)

necfalse
Defined by: (no known definition)
Used in:
e
Defined by: (no known definition)
Used in:
c
Defined by: (no known definition)
Used in:
a
Defined by: a
Used in:
o
Defined by: o
Used in:
d
Defined by: (no known definition)
Used in:

Function symbols (positive arity)

(No function symbols with non-zero arity.)

Primitive predicates (sorting)

Points
Objects
Properties
Propositions

Equality predicate

Used in:

Primitive predicates (non-sorting, non-equality)

Defined Predicates

o_equal (arity 2)
Defined by: o_equal
Used in:
a_equal (arity 2)
Defined by: a_equal
Used in:
object_equal (arity 2)
Defined by: object_equal
Used in:
actual_wrt (arity 2)
Defined by: actual_wrt
Used in:
is_the_disj_concept_of_wrt (arity 4)
Defined by: (no known definition)
Used in:
sum_of_wrt (arity 4)
Defined by: sum_of_wrt
Used in:
is_an_actual_world_wrt (arity 2)
Defined by: is_an_actual_world_wrt
Used in:
is_an_actual_world (arity 2)
Defined by: (no known definition)
Used in:
concept_of_wrt (arity 3)
Defined by: concept_of_wrt
Used in:
object_equal_wrt (arity 3)
Defined by: object_equal_wrt
Used in:
included_in_wrt (arity 3)
Defined by: included_in_wrt
Used in:
that_ordinary_object_ex1_property_is_true_in_wrt (arity 4)
Defined by: that_ordinary_object_ex1_property_is_true_in_wrt
Used in:
counterparts_wrt (arity 3)
Defined by: counterparts_wrt
Used in:
equal_wrt (arity 3)
Defined by: (no known definition)
Used in:
is_a_negation_of (arity 2)
Defined by: (no known definition)
Used in:
implies (arity 2)
Defined by: implies
Used in:
a_equal_wrt (arity 3)
Defined by: a_equal_wrt
Used in:
encp_wrt (arity 3)
Defined by: encp_wrt
Used in:
mirrors_wrt (arity 3)
Defined by: mirrors_wrt
Used in:
appears_in_wrt (arity 3)
Defined by: appears_in_wrt
Used in:
is_the_world_in_which_appears_wrt (arity 3)
Defined by: is_the_world_in_which_appears_wrt
Used in:
contains_wrt (arity 3)
Defined by: contains_wrt
Used in:
is_being_such_that (arity 2)
Defined by: is_being_such_that
Used in:
compossible_wrt (arity 3)
Defined by: compossible_wrt
Used in:
complete_wrt (arity 2)
Defined by: complete_wrt
Used in:
a_property_negation_of (arity 2)
Defined by: (no known definition)
Used in:
plug1 (arity 3)
Defined by: (no known definition)
Used in:
true_wrt (arity 2)
Defined by: (no known definition)
Used in:
haecceity_of_wrt (arity 3)
Defined by: haecceity_of_wrt
Used in:
o_equal_wrt (arity 3)
Defined by: o_equal_wrt
Used in:
singular_wrt (arity 2)
Defined by: singular_wrt
Used in:
world_wrt (arity 2)
Defined by: world_wrt
Used in:
realizes_in_wrt (arity 4)
Defined by: realizes_in_wrt
Used in:
ex1 (arity 2)
Defined by: ex1
Used in:
enc (arity 2)
Defined by: enc
Used in:
enc_wrt (arity 3)
Defined by: (no known definition)
Used in:
concept_of_individual_in_wrt (arity 4)
Defined by: concept_of_individual_in_wrt
Used in:
concept_of_individual_wrt (arity 3)
Defined by: concept_of_individual_wrt
Used in:
individual_concept_wrt (arity 2)
Defined by: individual_concept_wrt
Used in:
is_the_sum_of_wrt (arity 4)
Defined by: is_the_sum_of_wrt
Used in:
implies_wrt (arity 3)
Defined by: implies_wrt
Used in:
is_the_concept_of_wrt (arity 3)
Defined by: is_the_concept_of_wrt
Used in:
is_the_actual_world_wrt (arity 2)
Defined by: is_the_actual_world_wrt
Used in:
is_the_concept_of_individual_wrt (arity 3)
Defined by: is_the_concept_of_individual_wrt
Used in:
is_the_concept_of_individual_in_wrt (arity 4)
Defined by: is_the_concept_of_individual_in_wrt
Used in:
situation_wrt (arity 2)
Defined by: situation_wrt
Used in:
true_in_wrt (arity 3)
Defined by: true_in_wrt
Used in:
ex1_wrt (arity 3)
Defined by: (no known definition)
Used in:

Consistency Check

The principles of our theory comprise everything that is not a theorem or lemma, namely axioms, definitions, and sorting rules: There are 92 principles:
This is for the whole schmear/kitchen-sink (all 157 formulas):
This is for the reduced schmear/schmearela/kitchen-sink-minus-theorems/lemmas: