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: