See a later section. Make sure that that list contains only truly primitive predicates, such as ex1_wrt.
Comment: The property of being a concept is defined to be the property of being abstract
Representation: c = a
Used in the proof of:
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:
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)
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:
Comment: (nothing to say).
Representation: ∀X,F((object(X) ∧ property(F)) ⟶ ∃P((proposition(P) ∧ plug1(P,F,X))))
Used in the proof of:
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:
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:
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:
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:
Comment: (nothing to say).
Representation: ∀D(point(D) ⟶ ¬true_wrt(necfalse,D))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: ∀W,D(world_wrt(W,D) ⟶ (object(W) ∧ point(D)))
Used in the proof of:
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:
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:
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:
Comment: (nothing to say).
Representation: ∀P(proposition(P) ⟶ ∃Q((proposition(Q) ∧ is_a_negation_of(Q,P))))
Used in the proof of:
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:
Comment: (nothing to say).
Representation: ∃D, X((point(D) ∧ (object(X) ∧ ex1_wrt(e,X,D))))
Used in the proof of:
Comment: (nothing to say).
Representation: ∃D((point(D) ∧ ∃X((object(X) ∧ ex1_wrt(e,X,D)))))
Used in the proof of:
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:
Comment: (nothing to say).
Representation: ∀X,F((object(X) ∧ property(F)) ⟶ ∃P((proposition(P) ∧ plug1(P,F,X))))
Used in the proof of:
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:
Comment: (nothing to say).
Representation: ∀X,F((ex1(F,X) ⟷ ex1_wrt(F,X,d)))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: ∀X,F((enc(X,F) ⟷ enc_wrt(X,F,d)))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: proposition(necfalse)
Used in the proof of:
(nothing)
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:
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:
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:
Comment: (nothing to say).
Representation: ∀X,F((ex1(F,X) ⟷ ex1_wrt(F,X,d)))
Used in the proof of:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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)
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:
Comment: (nothing to say).
Representation: ∀F,G((property(F) ∧ property(G)) ⟶ (implies(F,G) ⟷ implies_wrt(F,G,d)))
Used in the proof of:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
Comment: (nothing to say).
Representation: ∀X,D(is_an_actual_world_wrt(X,D) ⟶ (object(X) ∧ point(D)))
Used in the proof of:
Comment: (nothing to say).
Representation: ∀P,F,X(plug1(P,F,X) ⟶ (object(X) ∧ (property(F) ∧ proposition(P))))
Used in the proof of:
(nothing)
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)
Comment: The distinguished point in the underlying modal logic
Representation: point(d)
Used in the proof of:
Comment: (nothing to say).
Representation: ∀X(property(X) ⟶ ¬point(X))
Used in the proof of:
Comment: (nothing to say).
Representation: ∀X(property(X) ⟶ ¬object(X))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: ∀X(proposition(X) ⟶ ¬point(X))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: ∀X(proposition(X) ⟶ ¬object(X))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: ∀X(proposition(X) ⟶ ¬property(X))
Used in the proof of:
(nothing)
Comment: (nothing to say).
Representation: ∀X(point(X) ⟶ ¬object(X))
Used in the proof of:
(nothing)
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:
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:
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:
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:
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)
Comment: (nothing to say).
Representation: ∀X,D(individual_concept_wrt(X,D) ⟶ (object(X) ∧ point(D)))
Used in the proof of:
Comment: The primitive property of concreteness
Representation: property(e)
Used in the proof of:
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:
Comment: (nothing to say).
Representation: ∀F,G,D(implies_wrt(F,G,D) ⟶ (property(F) ∧ (property(G) ∧ point(D))))
Used in the proof of:
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:
Comment: (see TPTP representation below).
Dependencies:
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)))))).
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)))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(u_exemplifies_P_iff_plug1_Pu_is_true_in_the_actual_world,lemma,(! [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)))))).
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))))))))))).
fof(the_actual_world_is_a_world,lemma,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(equivalence_truth_in_the_actual_world_and_truth,conjecture,(! [X] : ((object(X) & is_the_actual_world_wrt(X,d)) => (! [P] : (proposition(P) => (true_in_wrt(P,X,d) <=> true_wrt(P,d))))))).
fof(the_actual_world_exists,lemma,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
fof(actual_wrt,definition,(! [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))))))))).
fof(is_an_actual_world_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (is_an_actual_world_wrt(X,D) <=> (world_wrt(X,D) & actual_wrt(X,D)))))).
fof(is_the_actual_world_wrt,definition,(! [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)))))))).
fof(world_wrt,definition,(! [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))))))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(proposition_negations_exist,axiom,(! [P] : (proposition(P) => (? [Q] : (proposition(Q) & is_a_negation_of(Q,P)))))).
fof(proposition_negation_truth,axiom,(! [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:
Comment: (see TPTP representation below).
Dependencies:
fof(the_actual_world_is_a_world,conjecture,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
fof(is_an_actual_world_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (is_an_actual_world_wrt(X,D) <=> (world_wrt(X,D) & actual_wrt(X,D)))))).
fof(is_the_actual_world_wrt,definition,(! [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)))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
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)))))).
fof(distinguished_point_d,axiom,point(d)).
fof(equivalence_truth_in_the_actual_world_and_truth,lemma,(! [X] : ((object(X) & is_the_actual_world_wrt(X,d)) => (! [P] : (proposition(P) => (true_in_wrt(P,X,d) <=> true_wrt(P,d))))))).
fof(proposition_plug1_truth,axiom,(! [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:
Comment: (see TPTP representation below).
Dependencies:
fof(the_concept_of_individual_wrt_and_the_concept_of_individual_in_wrt_are_counterparts,conjecture,(! [U,X,Y,W] : ((object(U) & (object(X) & (object(Y) & object(W)))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & world_wrt(W,d)))) => ((is_the_concept_of_individual_wrt(X,U,d) & is_the_concept_of_individual_in_wrt(Y,U,W,d)) => counterparts_wrt(Y,X,d)))))).
fof(the_concept_of_an_individual_is_its_concept_in_the_actual_world,lemma,(! [X,U,A] : ((object(X) & (object(U) & object(A))) => ((is_the_actual_world_wrt(A,d) & (ex1_wrt(c,X,d) & ex1_wrt(o,U,d))) => (is_the_concept_of_individual_wrt(X,U,d) <=> is_the_concept_of_individual_in_wrt(X,U,A,d)))))).
fof(counterparts_wrt,definition,(! [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))))))))))))))).
fof(equivalence_truth_in_the_actual_world_and_truth,lemma,(! [X] : ((object(X) & is_the_actual_world_wrt(X,d)) => (! [P] : (proposition(P) => (true_in_wrt(P,X,d) <=> true_wrt(P,d))))))).
fof(the_actual_world_is_a_world,lemma,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(the_actual_world_exists,lemma,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(existence_of_is_the_concept_of_wrt,conjecture,(! [F] : (property(F) => (? [X] : (object(X) & is_the_concept_of_wrt(X,F,d)))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(a_equal_wrt,definition,(! [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)))))))))))).
fof(concept_of_wrt,definition,(! [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))))))))).
fof(is_the_concept_of_wrt,definition,(! [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))))))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(rigidity_of_encoding,axiom,(! [X,F] : ((object(X) & property(F)) => ((? [D] : (point(D) & enc_wrt(X,F,D))) => (! [D] : (point(D) => enc_wrt(X,F,D))))))).
fof(universalized_comprehension_instance_38_1,axiom,(! [G] : (property(G) => (? [Z] : (object(Z) & (ex1_wrt(a,Z,d) & (! [F] : (property(F) => (enc_wrt(Z,F,d) <=> implies_wrt(G,F,d)))))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(sort_enc_wrt,axiom,(! [X,F,D] : (enc_wrt(X,F,D) => (object(X) & (property(F) & point(D)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
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)))))))).
fof(rigidity_of_encoding,axiom,(! [X,F] : ((object(X) & property(F)) => ((? [D] : (point(D) & enc_wrt(X,F,D))) => (! [D] : (point(D) => enc_wrt(X,F,D))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(sort_concept_of_individual_wrt,axiom,(! [X,U,D] : (concept_of_individual_wrt(X,U,D) => (object(X) & (object(U) & point(D)))))).
fof(distinguished_point_d,axiom,point(d)).
fof(comprehension_for_concept_of_individual_wrt,axiom,(! [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)))))))))))).
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)))))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(a_equal_wrt,definition,(! [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:
Comment: (see TPTP representation below).
Dependencies:
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))))))))))))).
fof(sort_is_the_concept_of_wrt,axiom,(! [X,F,D] : (is_the_concept_of_wrt(X,F,D) => (ex1_wrt(c,X,D) & (object(X) & (property(F) & point(D))))))).
fof(included_in_wrt,definition,(! [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)))))))))).
fof(existence_of_is_the_concept_of_wrt,lemma,(! [F] : (property(F) => (? [X] : (object(X) & is_the_concept_of_wrt(X,F,d)))))).
fof(existence_of_the_concept_of_individual_wrt,lemma,(! [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)))))))).
fof(the_concept_of_F_wrt_encodes_G_if_and_only_F_implies_G,lemma,(! [X,F] : ((object(X) & property(F)) => (ex1_wrt(c,X,d) => (is_the_concept_of_wrt(X,F,d) => (! [G] : (property(G) => (enc_wrt(X,G,d) <=> implies_wrt(F,G,d))))))))).
fof(the_concept_of_individual_wrt_encodes_exactly_what_it_exemplifies,lemma,(! [X,U] : ((object(X) & object(U)) => (is_the_concept_of_individual_wrt(X,U,d) => (! [G] : (property(G) => (enc_wrt(X,G,d) <=> ex1_wrt(G,U,d)))))))).
fof(implies_wrt,definition,(! [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)))))))))).
fof(contains_wrt,definition,(! [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:
Comment: (see TPTP representation below).
Dependencies:
fof(existence_and_property_of_the_concept_of_individual_in_wrt,conjecture,(! [U,Y] : ((object(U) & object(Y)) => ((ex1_wrt(o,U,d) & world_wrt(Y,d)) => (? [X] : (object(X) & (ex1_wrt(c,X,d) & (is_the_concept_of_individual_in_wrt(X,U,Y,d) & (! [F,P] : ((property(F) & proposition(P)) => (plug1(P,F,U) => (enc_wrt(X,F,d) <=> true_in_wrt(P,Y,d))))))))))))).
fof(proposition_plug1_truth,axiom,(! [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)))))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(instance_of_comprehension_for_concept_of_individual_in_wrt,axiom,(! [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))))))))))))).
fof(that_ordinary_object_ex1_property_is_true_in_wrt,definition,(! [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)))))))))).
fof(concept_of_individual_in_wrt,definition,(! [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)))))))).
fof(is_the_concept_of_individual_in_wrt,definition,(! [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)))))))).
fof(uniqueness_of_concept_of_individual_in_wrt,lemma,(! [D] : (point(D) => (! [X,Y,U,W] : ((object(X) & (object(Y) & (object(U) & object(W)))) => (world_wrt(W,D) => ((concept_of_individual_in_wrt(X,U,W,D) & concept_of_individual_in_wrt(Y,U,W,D)) => a_equal_wrt(X,Y,D)))))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(sort_concept_of_individual_in_wrt,axiom,(! [X,U,W,D] : (concept_of_individual_in_wrt(X,U,W,D) => (object(X) & (object(U) & (object(W) & point(D))))))).
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))))))))))).
fof(world_wrt,definition,(! [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:
Comment: (see TPTP representation below).
Dependencies:
fof(if_Z_does_not_encode_F_then_Z_does_not_contain_the_concept_of_F,conjecture,(! [F,Y,Z] : ((property(F) & (object(Y) & object(Z))) => ((ex1_wrt(c,Y,d) & ex1_wrt(c,Z,d)) => ((is_the_concept_of_wrt(Y,F,d) & ~ enc_wrt(Z,F,d)) => ~ contains_wrt(Z,Y,d)))))).
fof(concept_of_wrt,definition,(! [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))))))))).
fof(contains_wrt,definition,(! [X,Y,D] : ((object(X) & (object(Y) & point(D))) => (contains_wrt(Y,X,D) <=> included_in_wrt(X,Y,D))))).
fof(implies_wrt,definition,(! [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)))))))))).
fof(included_in_wrt,definition,(! [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)))))))))).
fof(is_the_concept_of_wrt,definition,(! [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))))))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(the_concept_of_individual_in_w_wrt_appears_in_w_wrt,conjecture,(! [U,X,W] : ((object(U) & (object(X) & object(W))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,X,d) & world_wrt(W,d))) => (is_the_concept_of_individual_in_wrt(X,U,W,d) => appears_in_wrt(X,W,d)))))).
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)))))))))).
fof(concept_of_individual_in_wrt,definition,(! [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)))))))).
fof(is_the_concept_of_individual_in_wrt,definition,(! [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)))))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(possibly_not_Fu_implies_a_world_where_not_Fu_is_true,conjecture,(! [U,F] : ((object(U) & property(F)) => ((ex1_wrt(o,U,d) & (? [D] : (point(D) & ~ ex1_wrt(F,U,D)))) => (? [Y,P,Q] : (object(Y) & (proposition(P) & (proposition(Q) & (world_wrt(Y,d) & (plug1(P,F,U) & (is_a_negation_of(Q,P) & true_in_wrt(Q,Y,d)))))))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(facts_about_negated_propositions_and_true_in_wrt,conjecture,(! [P,Q,X] : ((proposition(P) & (proposition(Q) & object(X))) => ((is_a_negation_of(Q,P) & world_wrt(X,d)) => (true_in_wrt(P,X,d) <=> ~ true_in_wrt(Q,X,d)))))).
fof(negated_propositions,definition,(! [P,Q] : ((proposition(P) & proposition(Q)) => (is_a_negation_of(Q,P) <=> (! [D] : (point(D) => (~ true_wrt(Q,D) <=> true_wrt(P,D)))))))).
fof(sort_world,axiom,(! [W,D] : (world_wrt(W,D) => (object(W) & point(D))))).
fof(world_wrt,definition,(! [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:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(not_f_u_implies_not_f_u_is_true_in_the_actual_world,conjecture,(! [U,A,F,P,Q] : ((object(U) & (object(A) & (property(F) & (proposition(P) & proposition(Q))))) => ((ex1_wrt(o,U,d) & (~ ex1_wrt(F,U,d) & (is_a_negation_of(Q,P) & (is_the_actual_world_wrt(A,d) & plug1(P,F,U))))) => true_in_wrt(Q,A,d))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(f_u_implies_f_u_is_true_in_the_actual_world,conjecture,(! [U,A,F,P] : ((object(U) & (object(A) & (property(F) & proposition(P)))) => ((ex1_wrt(o,U,d) & (ex1_wrt(F,U,d) & (is_the_actual_world_wrt(A,d) & plug1(P,F,U)))) => true_in_wrt(P,A,d))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(true_in_A_but_not_true_in_B_then_A_not_B,conjecture,(! [P,X,Y] : ((proposition(P) & (object(X) & object(Y))) => ((world_wrt(X,d) & world_wrt(Y,d)) => ((true_in_wrt(P,X,d) & ~ true_in_wrt(P,Y,d)) => ~ equal_wrt(X,Y,d)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(the_actual_world_exists,conjecture,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
fof(an_actual_world_exists,lemma,(? [A] : (object(A) & is_an_actual_world_wrt(A,d)))).
fof(there_is_at_most_one_actual_world,conjecture,(! [A,B] : ((object(A) & object(B)) => ((is_an_actual_world_wrt(A,d) & is_an_actual_world(B,d)) => object_equal_wrt(A,B,d))))).
fof(is_the_actual_world_wrt,definition,(! [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)))))))).
fof(sort_is_an_actual_world_wrt,axiom,(! [X,D] : (is_an_actual_world_wrt(X,D) => (object(X) & point(D))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(an_actual_world_exists,conjecture,(? [A] : (object(A) & is_an_actual_world_wrt(A,d)))).
fof(actual_wrt,definition,(! [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))))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(encp_wrt,definition,(! [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)))))))).
fof(existence_vac,axiom,(! [P] : (proposition(P) => (? [Q] : (property(Q) & is_being_such_that(Q,P)))))).
fof(instance_of_comprehension_for_an_actual_world,axiom,(! [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))))))))))))).
fof(is_an_actual_world_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (is_an_actual_world_wrt(X,D) <=> (world_wrt(X,D) & actual_wrt(X,D)))))).
fof(situation_wrt,definition,(! [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:
Comment: (see TPTP representation below).
Dependencies:
fof(the_concept_of_F_wrt_encodes_G_if_and_only_F_implies_G,conjecture,(! [X,F] : ((object(X) & property(F)) => (ex1_wrt(c,X,d) => (is_the_concept_of_wrt(X,F,d) => (! [G] : (property(G) => (enc_wrt(X,G,d) <=> implies_wrt(F,G,d))))))))).
fof(is_the_concept_of_wrt,definition,(! [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))))))))).
fof(concept_of_wrt,definition,(! [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))))))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(the_concept_of_individual_wrt_encodes_exactly_what_it_exemplifies,conjecture,(! [X,U] : ((object(X) & object(U)) => (is_the_concept_of_individual_wrt(X,U,d) => (! [G] : (property(G) => (enc_wrt(X,G,d) <=> ex1_wrt(G,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)))))))).
fof(any_concept_of_individual_wrt_encodes_exactly_what_it_exemplifies,lemma,(! [X,U,G] : ((object(X) & object(U)) => (concept_of_individual_wrt(X,U,d) => (! [G] : (property(G) => (enc_wrt(X,G,d) <=> ex1_wrt(G,U,d)))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(uniqueness_of_concept_of_individual_in_wrt,conjecture,(! [D] : (point(D) => (! [X,Y,U,W] : ((object(X) & (object(Y) & (object(U) & object(W)))) => (world_wrt(W,D) => ((concept_of_individual_in_wrt(X,U,W,D) & concept_of_individual_in_wrt(Y,U,W,D)) => a_equal_wrt(X,Y,D)))))))).
fof(rigidity_of_encoding,axiom,(! [X,F] : ((object(X) & property(F)) => ((? [D] : (point(D) & enc_wrt(X,F,D))) => (! [D] : (point(D) => enc_wrt(X,F,D))))))).
fof(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
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))))))))))).
fof(a_equal_wrt,definition,(! [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)))))))))))).
fof(concept_of_individual_in_wrt,definition,(! [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)))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(any_concept_of_individual_wrt_encodes_exactly_what_it_exemplifies,conjecture,(! [X,U,G] : ((object(X) & object(U)) => (concept_of_individual_wrt(X,U,d) => (! [G] : (property(G) => (enc_wrt(X,G,d) <=> ex1_wrt(G,U,d)))))))).
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(distinguished_point_d,axiom,point(d)).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(possibly_Fu_implies_a_world_where_Fu_is_true,conjecture,(! [U,F] : ((object(U) & property(F)) => ((ex1_wrt(o,U,d) & (? [D] : (point(D) & ex1_wrt(F,U,D)))) => (? [Y,P] : (object(Y) & (proposition(P) & (world_wrt(Y,d) & (plug1(P,F,U) & true_in_wrt(P,Y,d)))))))))).
fof(possibly_p_iff_there_is_a_world_where_p_is_true,theorem,(! [P] : (proposition(P) => ((? [D] : (point(D) & true_wrt(P,D))) <=> (? [X] : (object(X) & (world_wrt(X,d) & true_in_wrt(P,X,d)))))))).
fof(existence_of_plug1_propositions,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(proposition_plug1_truth,axiom,(! [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:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(if_the_concept_of_individual_u_in_w_wrt_does_encode_K_then_it_does_contain_the_concept_K,conjecture,(! [U,Z,W,F,Y] : ((object(U) & (object(Z) & (object(W) & (property(F) & object(Y))))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & world_wrt(W,d)))) => ((is_the_concept_of_individual_in_wrt(Z,U,W,d) & (enc_wrt(Z,F,d) & is_the_concept_of_wrt(Y,F,d))) => contains_wrt(Z,Y,d)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(lemma_concept_of_individual_wrt,conjecture,(! [X,U,G] : ((object(X) & (object(U) & property(G))) => ((ex1_wrt(c,X,d) & (ex1_wrt(o,U,d) & is_the_concept_of_individual_wrt(X,U,d))) => (enc_wrt(X,G,d) <=> ex1_wrt(G,U,d)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(sum_lemma,conjecture,(! [X,Y,Z,G] : ((object(X) & (object(Y) & (object(Z) & property(G)))) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & is_the_sum_of_wrt(Z,X,Y,d)))) => (enc_wrt(Z,G,d) <=> (enc_wrt(X,G,d) | enc_wrt(Y,G,d))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(there_are_ordinary_objects,conjecture,(? [X] : (object(X) & ex1_wrt(o,X,d)))).
fof(possibly_there_are_concrete_objects,axiom,(? [D] : (point(D) & (? [X] : (object(X) & ex1_wrt(e,X,D)))))).
fof(o,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
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)))))).
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(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)))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(proposition_plug1_truth,axiom,(! [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)))))))).
fof(the_actual_world_is_a_world,lemma,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
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)))))))))).
fof(equivalence_truth_in_the_actual_world_and_truth,lemma,(! [X] : ((object(X) & is_the_actual_world_wrt(X,d)) => (! [P] : (proposition(P) => (true_in_wrt(P,X,d) <=> true_wrt(P,d))))))).
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))))))))))).
fof(the_actual_world_exists,lemma,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(necessity_of_being_a_concept,conjecture,(! [X] : (object(X) => (ex1_wrt(c,X,d) => (! [D] : (point(D) => ex1_wrt(c,X,D))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(a_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~ (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(an_individual_concept_mirrors_the_world_in_which_it_appears,conjecture,(! [C,W,D] : ((object(C) & object(W)) => (individual_concept_wrt(C,d) => (is_the_world_in_which_appears_wrt(W,C,d) => mirrors_wrt(C,W,d)))))).
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)))))))).
fof(is_the_world_in_which_appears_wrt,definition,(! [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)))))))))).
fof(distinguished_point_d,axiom,point(d)).
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)))))))))).
fof(encp_wrt,definition,(! [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)))))))).
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))))))))))).
fof(true_in_wrt,definition,(! [P,X,D] : ((proposition(P) & (object(X) & point(D))) => (true_in_wrt(P,X,D) <=> (situation_wrt(X,D) & encp_wrt(X,P,D)))))).
fof(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(theorem7_world_theory,axiom,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(co_realizers_are_identical,conjecture,(! [A,B,C,W,D] : ((object(A) & (object(B) & (object(C) & (object(W) & point(D))))) => ((realizes_in_wrt(A,C,W,D) & realizes_in_wrt(B,C,W,D)) => (A = B))))).
fof(co_realizers_are_ordinary_object_equal,lemma,(! [A,B,C,W,D] : ((object(A) & (object(B) & (object(C) & (object(W) & point(D))))) => ((realizes_in_wrt(A,C,W,D) & realizes_in_wrt(B,C,W,D)) => o_equal_wrt(A,B,D))))).
fof(o,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
fof(necessarily_o_equal_wrt_implies_identity,axiom,(! [X,Y] : ((object(X) & object(Y)) => ((! [D] : (point(D) => o_equal_wrt(X,Y,D))) => (X = Y))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(possibly_o_equal_wrt_implies_necessarily_o_equal_wrt,conjecture,(! [X,Y] : ((object(X) & object(Y)) => ((? [D] : (point(D) & o_equal_wrt(X,Y,D))) => (! [D] : (point(D) => o_equal_wrt(X,Y,D))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(existence_of_haecceity_for_ordinary_objects,conjecture,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) => (? [F] : (property(F) & haecceity_of_wrt(F,X,D))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(co_realizers_are_ordinary_object_equal,conjecture,(! [A,B,C,W,D] : ((object(A) & (object(B) & (object(C) & (object(W) & point(D))))) => ((realizes_in_wrt(A,C,W,D) & realizes_in_wrt(B,C,W,D)) => o_equal_wrt(A,B,D))))).
fof(co_realizers_co_exemplify,lemma,(! [A,B,C,W,D] : ((object(A) & (object(B) & (object(C) & (object(W) & point(D))))) => ((realizes_in_wrt(A,C,W,D) & realizes_in_wrt(B,C,W,D)) => (! [F] : (ex1_wrt(F,A,D) <=> ex1_wrt(F,B,D))))))).
fof(existence_of_haecceity_for_ordinary_objects,lemma,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) => (? [F] : (property(F) & haecceity_of_wrt(F,X,D))))))).
fof(haecceity_of_wrt,definition,(! [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))))))))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
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))))))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(co_realizers_co_exemplify,conjecture,(! [A,B,C,W,D] : ((object(A) & (object(B) & (object(C) & (object(W) & point(D))))) => ((realizes_in_wrt(A,C,W,D) & realizes_in_wrt(B,C,W,D)) => (! [F] : (ex1_wrt(F,A,D) <=> ex1_wrt(F,B,D))))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
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))))))))))).
fof(truth_of_plug1_propositions,axiom,(! [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)))))))).
fof(existence_of_plug1_propositions,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(world_wrt,definition,(! [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))))))))))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
fof(possibly_o_equal_wrt_implies_necessarily_o_equal_wrt,lemma,(! [X,Y] : ((object(X) & object(Y)) => ((? [D] : (point(D) & o_equal_wrt(X,Y,D))) => (! [D] : (point(D) => o_equal_wrt(X,Y,D))))))).
fof(haecceity_of_wrt,definition,(! [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))))))))).
fof(existence_of_haecceity_for_ordinary_objects,lemma,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) => (? [F] : (property(F) & haecceity_of_wrt(F,X,D))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(the_concept_of_an_individual_is_its_concept_in_the_actual_world,conjecture,(! [X,U,A] : ((object(X) & (object(U) & object(A))) => ((is_the_actual_world_wrt(A,d) & (ex1_wrt(c,X,d) & ex1_wrt(o,U,d))) => (is_the_concept_of_individual_wrt(X,U,d) <=> is_the_concept_of_individual_in_wrt(X,U,A,d)))))).
fof(concept_of_individual_in_wrt,definition,(! [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)))))))).
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(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(is_the_concept_of_individual_in_wrt,definition,(! [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)))))))).
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)))))))).
fof(kinds_for_truth_in,lemma,(! [X,Y,Z] : (true_in_wrt(X,Y,Z) => (proposition(X) & (situation_wrt(Y,Z) & point(Z)))))).
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))))))))))).
fof(sort_concept_of_individual_in_wrt,axiom,(! [X,U,W,D] : (concept_of_individual_in_wrt(X,U,W,D) => (object(X) & (object(U) & (object(W) & point(D))))))).
fof(sort_concept_of_individual_wrt,axiom,(! [X,U,D] : (concept_of_individual_wrt(X,U,D) => (object(X) & (object(U) & point(D)))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(u_exemplifies_P_iff_plug1_Pu_is_true_in_the_actual_world,lemma,(! [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)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(kinds_for_truth_in,conjecture,(! [X,Y,Z] : (true_in_wrt(X,Y,Z) => (proposition(X) & (situation_wrt(Y,Z) & point(Z)))))).
fof(true_in_wrt,definition,(! [P,X,D] : ((proposition(P) & (object(X) & point(D))) => (true_in_wrt(P,X,D) <=> (situation_wrt(X,D) & encp_wrt(X,P,D)))))).
fof(sort_true_in_wrt,axiom,(! [P,X,D] : (true_in_wrt(P,X,D) => (proposition(P) & (object(X) & point(D)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(being_abstract_and_being_ordinary_are_mutually_exclusive,conjecture,(! [X] : (object(X) => (ex1_wrt(a,X,d) <=> ~ ex1_wrt(o,X,d))))).
fof(o,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(a,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~ (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem01,conjecture,(! [X] : (object(X) => (ex1_wrt(c,X,d) => object_equal_wrt(X,X,d))))).
fof(distinguished_point_d,axiom,point(d)).
fof(distinguished_property_e,axiom,property(e)).
fof(o,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(a,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~ (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(ex1,definition,(! [X,F] : (ex1(F,X) <=> ex1_wrt(F,X,d)))).
fof(enc,definition,(! [X,F] : (enc(X,F) <=> enc_wrt(X,F,d)))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
fof(o_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (o_equal(X,Y) <=> o_equal_wrt(X,Y,d))))).
fof(a_equal_wrt,definition,(! [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)))))))))))).
fof(a_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (a_equal(X,Y) <=> a_equal_wrt(X,Y,d))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(object_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (object_equal(X,Y) <=> object_equal_wrt(X,Y,d))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(sort_enc_wrt,axiom,(! [X,F,D] : (enc_wrt(X,F,D) => (object(X) & (property(F) & point(D)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem02,conjecture,(! [X,Y] : ((object(X) & object(Y)) => ((ex1_wrt(c,X,d) & ex1_wrt(c,Y,d)) => (object_equal_wrt(X,Y,d) => object_equal_wrt(Y,X,d)))))).
fof(distinguished_point_d,axiom,point(d)).
fof(distinguished_property_e,axiom,property(e)).
fof(o,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(a,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~ (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(ex1,definition,(! [X,F] : (ex1(F,X) <=> ex1_wrt(F,X,d)))).
fof(enc,definition,(! [X,F] : (enc(X,F) <=> enc_wrt(X,F,d)))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
fof(o_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (o_equal(X,Y) <=> o_equal_wrt(X,Y,d))))).
fof(a_equal_wrt,definition,(! [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)))))))))))).
fof(a_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (a_equal(X,Y) <=> a_equal_wrt(X,Y,d))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(object_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (object_equal(X,Y) <=> object_equal_wrt(X,Y,d))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(sort_enc_wrt,axiom,(! [X,F,D] : (enc_wrt(X,F,D) => (object(X) & (property(F) & point(D)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem03,conjecture,(! [X,Y,Z] : ((object(X) & (object(Y) & object(Z))) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & ex1_wrt(c,Z,d))) => ((object_equal_wrt(X,Y,d) & object_equal_wrt(Y,Z,d)) => object_equal_wrt(X,Z,d)))))).
fof(distinguished_point_d,axiom,point(d)).
fof(distinguished_property_e,axiom,property(e)).
fof(o,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(a,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~ (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(ex1,definition,(! [X,F] : (ex1(F,X) <=> ex1_wrt(F,X,d)))).
fof(enc,definition,(! [X,F] : (enc(X,F) <=> enc_wrt(X,F,d)))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
fof(o_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (o_equal(X,Y) <=> o_equal_wrt(X,Y,d))))).
fof(a_equal_wrt,definition,(! [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)))))))))))).
fof(a_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (a_equal(X,Y) <=> a_equal_wrt(X,Y,d))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(object_equal,definition,(! [X,Y] : ((object(X) & object(Y)) => (object_equal(X,Y) <=> object_equal_wrt(X,Y,d))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(sort_enc_wrt,axiom,(! [X,F,D] : (enc_wrt(X,F,D) => (object(X) & (property(F) & point(D)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem04,conjecture,(! [G,H,X,Y,Z,W] : ((property(G) & (property(H) & (object(X) & (object(Y) & (object(Z) & (object(W) & (ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & (ex1_wrt(c,W,d) & (is_the_concept_of_wrt(X,G,d) & (is_the_concept_of_wrt(Y,H,d) & (is_the_sum_of_wrt(Z,X,Y,d) & is_the_disj_concept_of_wrt(W,G,H,d)))))))))))))) => object_equal_wrt(Z,W,d)))).
fof(implies_wrt,definition,(! [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)))))))))).
fof(sort_implies_wrt,axiom,(! [F,G,D] : (implies_wrt(F,G,D) => (property(F) & (property(G) & point(D)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem05,conjecture,(! [X,Y] : ((object(X) & object(Y)) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & is_the_sum_of_wrt(Y,X,X,d))) => a_equal_wrt(Y,X,d))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(a_equal_wrt,definition,(! [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)))))))))))).
fof(is_the_sum_of_wrt,definition,(! [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))))))))).
fof(sum_of_wrt,definition,(! [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)))))))))).
fof(rigidity_of_encoding,axiom,(! [X,F] : ((object(X) & property(F)) => ((? [D] : (point(D) & enc_wrt(X,F,D))) => (! [D] : (point(D) => enc_wrt(X,F,D))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(sort_is_the_sum_of_wrt,axiom,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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)))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
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)))))))))).
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)))))))).
fof(u_realizes_in_wrt_the_concept_of_individual_u,lemma,(! [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)))))).
fof(equivalence_truth_in_the_actual_world_and_truth,lemma,(! [X] : ((object(X) & is_the_actual_world_wrt(X,d)) => (! [P] : (proposition(P) => (true_in_wrt(P,X,d) <=> true_wrt(P,d))))))).
fof(the_actual_world_is_a_world,lemma,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
fof(the_actual_world_exists,lemma,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(principia_019,conjecture,(! [X,Y] : ((object(X) & object(Y)) => ((? [D] : (point(D) & object_equal_wrt(X,Y,D))) => (X = Y))))).
fof(necessarily_a_equal_wrt_implies_identity,axiom,(! [X,Y] : ((object(X) & object(Y)) => ((! [D] : (point(D) => a_equal_wrt(X,Y,D))) => (X = Y))))).
fof(necessarily_o_equal_wrt_implies_identity,axiom,(! [X,Y] : ((object(X) & object(Y)) => ((! [D] : (point(D) => o_equal_wrt(X,Y,D))) => (X = Y))))).
fof(object_equal_wrt,definition,(! [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)))))).
fof(o_equal_wrt,definition,(! [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)))))))))))).
fof(a_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(a,X,D) <=> ~ (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(o_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(a_equal_wrt,definition,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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)))))))))))))))))))))))).
fof(theorem38,lemma,(! [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))))))))))))).
fof(existence_and_property_of_the_concept_of_individual_in_wrt,lemma,(! [U,Y] : ((object(U) & object(Y)) => ((ex1_wrt(o,U,d) & world_wrt(Y,d)) => (? [X] : (object(X) & (ex1_wrt(c,X,d) & (is_the_concept_of_individual_in_wrt(X,U,Y,d) & (! [F,P] : ((property(F) & proposition(P)) => (plug1(P,F,U) => (enc_wrt(X,F,d) <=> true_in_wrt(P,Y,d))))))))))))).
fof(the_concept_of_individual_wrt_and_the_concept_of_individual_in_wrt_are_counterparts,lemma,(! [U,X,Y,W] : ((object(U) & (object(X) & (object(Y) & object(W)))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & world_wrt(W,d)))) => ((is_the_concept_of_individual_wrt(X,U,d) & is_the_concept_of_individual_in_wrt(Y,U,W,d)) => counterparts_wrt(Y,X,d)))))).
fof(if_Z_does_not_encode_F_then_Z_does_not_contain_the_concept_of_F,lemma,(! [F,Y,Z] : ((property(F) & (object(Y) & object(Z))) => ((ex1_wrt(c,Y,d) & ex1_wrt(c,Z,d)) => ((is_the_concept_of_wrt(Y,F,d) & ~ enc_wrt(Z,F,d)) => ~ contains_wrt(Z,Y,d)))))).
fof(the_concept_of_individual_in_w_wrt_appears_in_w_wrt,lemma,(! [U,X,W] : ((object(U) & (object(X) & object(W))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,X,d) & world_wrt(W,d))) => (is_the_concept_of_individual_in_wrt(X,U,W,d) => appears_in_wrt(X,W,d)))))).
fof(possibly_not_Fu_implies_a_world_where_not_Fu_is_true,lemma,(! [U,F] : ((object(U) & property(F)) => ((ex1_wrt(o,U,d) & (? [D] : (point(D) & ~ ex1_wrt(F,U,D)))) => (? [Y,P,Q] : (object(Y) & (proposition(P) & (proposition(Q) & (world_wrt(Y,d) & (plug1(P,F,U) & (is_a_negation_of(Q,P) & true_in_wrt(Q,Y,d)))))))))))).
fof(facts_about_negated_propositions_and_true_in_wrt,lemma,(! [P,Q,X] : ((proposition(P) & (proposition(Q) & object(X))) => ((is_a_negation_of(Q,P) & world_wrt(X,d)) => (true_in_wrt(P,X,d) <=> ~ true_in_wrt(Q,X,d)))))).
fof(the_actual_world_exists,lemma,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
fof(the_actual_world_is_a_world,lemma,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
fof(f_u_implies_f_u_is_true_in_the_actual_world,lemma,(! [U,A,F,P] : ((object(U) & (object(A) & (property(F) & proposition(P)))) => ((ex1_wrt(o,U,d) & (ex1_wrt(F,U,d) & (is_the_actual_world_wrt(A,d) & plug1(P,F,U)))) => true_in_wrt(P,A,d))))).
fof(true_in_A_but_not_true_in_B_then_A_not_B,lemma,(! [P,X,Y] : ((proposition(P) & (object(X) & object(Y))) => ((world_wrt(X,d) & world_wrt(Y,d)) => ((true_in_wrt(P,X,d) & ~ true_in_wrt(P,Y,d)) => ~ equal_wrt(X,Y,d)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem_40b,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)))))))))))))))))))))))).
fof(proposition_negations_exist,axiom,(! [P] : (proposition(P) => (? [Q] : (proposition(Q) & is_a_negation_of(Q,P)))))).
fof(theorem38,lemma,(! [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))))))))))))).
fof(possibly_Fu_implies_a_world_where_Fu_is_true,lemma,(! [U,F] : ((object(U) & property(F)) => ((ex1_wrt(o,U,d) & (? [D] : (point(D) & ex1_wrt(F,U,D)))) => (? [Y,P] : (object(Y) & (proposition(P) & (world_wrt(Y,d) & (plug1(P,F,U) & true_in_wrt(P,Y,d)))))))))).
fof(existence_and_property_of_the_concept_of_individual_in_wrt,lemma,(! [U,Y] : ((object(U) & object(Y)) => ((ex1_wrt(o,U,d) & world_wrt(Y,d)) => (? [X] : (object(X) & (ex1_wrt(c,X,d) & (is_the_concept_of_individual_in_wrt(X,U,Y,d) & (! [F,P] : ((property(F) & proposition(P)) => (plug1(P,F,U) => (enc_wrt(X,F,d) <=> true_in_wrt(P,Y,d))))))))))))).
fof(the_concept_of_individual_wrt_and_the_concept_of_individual_in_wrt_are_counterparts,lemma,(! [U,X,Y,W] : ((object(U) & (object(X) & (object(Y) & object(W)))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & world_wrt(W,d)))) => ((is_the_concept_of_individual_wrt(X,U,d) & is_the_concept_of_individual_in_wrt(Y,U,W,d)) => counterparts_wrt(Y,X,d)))))).
fof(facts_about_negated_propositions_and_true_in_wrt,lemma,(! [P,Q,X] : ((proposition(P) & (proposition(Q) & object(X))) => ((is_a_negation_of(Q,P) & world_wrt(X,d)) => (true_in_wrt(P,X,d) <=> ~ true_in_wrt(Q,X,d)))))).
fof(if_the_concept_of_individual_u_in_w_wrt_does_encode_K_then_it_does_contain_the_concept_K,lemma,(! [U,Z,W,F,Y] : ((object(U) & (object(Z) & (object(W) & (property(F) & object(Y))))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & world_wrt(W,d)))) => ((is_the_concept_of_individual_in_wrt(Z,U,W,d) & (enc_wrt(Z,F,d) & is_the_concept_of_wrt(Y,F,d))) => contains_wrt(Z,Y,d)))))).
fof(the_actual_world_exists,lemma,(? [X] : (object(X) & is_the_actual_world_wrt(X,d)))).
fof(the_actual_world_is_a_world,lemma,(! [X] : (object(X) => (is_the_actual_world_wrt(X,d) => world_wrt(X,d))))).
fof(not_f_u_implies_not_f_u_is_true_in_the_actual_world,lemma,(! [U,A,F,P,Q] : ((object(U) & (object(A) & (property(F) & (proposition(P) & proposition(Q))))) => ((ex1_wrt(o,U,d) & (~ ex1_wrt(F,U,d) & (is_a_negation_of(Q,P) & (is_the_actual_world_wrt(A,d) & plug1(P,F,U))))) => true_in_wrt(Q,A,d))))).
fof(true_in_A_but_not_true_in_B_then_A_not_B,lemma,(! [P,X,Y] : ((proposition(P) & (object(X) & object(Y))) => ((world_wrt(X,d) & world_wrt(Y,d)) => ((true_in_wrt(P,X,d) & ~ true_in_wrt(P,Y,d)) => ~ equal_wrt(X,Y,d)))))).
fof(the_concept_of_individual_in_w_wrt_appears_in_w_wrt,lemma,(! [U,X,W] : ((object(U) & (object(X) & object(W))) => ((ex1_wrt(o,U,d) & (ex1_wrt(c,X,d) & world_wrt(W,d))) => (is_the_concept_of_individual_in_wrt(X,U,W,d) => appears_in_wrt(X,W,d)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(possibly_p_iff_there_is_a_world_where_p_is_true,conjecture,(! [P] : (proposition(P) => ((? [D] : (point(D) & true_wrt(P,D))) <=> (? [X] : (object(X) & (world_wrt(X,d) & true_in_wrt(P,X,d)))))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
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)))))))))))).
fof(lemma_concept_of_individual_wrt,lemma,(! [X,U,G] : ((object(X) & (object(U) & property(G))) => ((ex1_wrt(c,X,d) & (ex1_wrt(o,U,d) & is_the_concept_of_individual_wrt(X,U,d))) => (enc_wrt(X,G,d) <=> ex1_wrt(G,U,d)))))).
fof(theorem38,lemma,(! [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))))))))))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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))))))))))).
fof(concept_of_wrt,definition,(! [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))))))))).
fof(contains_wrt,definition,(! [X,Y,D] : ((object(X) & (object(Y) & point(D))) => (contains_wrt(Y,X,D) <=> included_in_wrt(X,Y,D))))).
fof(implies_wrt,definition,(! [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)))))))))).
fof(implies,definition,(! [F,G] : ((property(F) & property(G)) => (implies(F,G) <=> implies_wrt(F,G,d))))).
fof(included_in_wrt,definition,(! [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)))))))))).
fof(is_the_concept_of_wrt,definition,(! [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))))))))).
fof(o_wrt,definition,(! [X,D] : ((object(X) & point(D)) => (ex1_wrt(o,X,D) <=> (? [D2] : (point(D2) & ex1_wrt(e,X,D2))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(possible_existence_of_concrete_object,axiom,(? [D,X] : (point(D) & (object(X) & ex1_wrt(e,X,D))))).
fof(ind_concept_encodes_properties_implied_by_what_it_encodes,theorem,(! [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))))))).
fof(theorem38,lemma,(! [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))))))))))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(ind_concept_encodes_properties_implied_by_what_it_encodes,conjecture,(! [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))))))).
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)))))))).
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)))))))))).
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))))))))))).
fof(implies_wrt,definition,(! [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)))))))))).
fof(implies,definition,(! [F,G] : ((property(F) & property(G)) => (implies(F,G) <=> implies_wrt(F,G,d))))).
fof(world_wrt,definition,(! [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))))))))))).
fof(proposition_plug1_truth,axiom,(! [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)))))))).
fof(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(sort_implies_wrt,axiom,(! [F,G,D] : (implies_wrt(F,G,D) => (property(F) & (property(G) & point(D)))))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
fof(theorem06,conjecture,(! [X,Y,Z,W] : ((object(X) & (object(Y) & (object(Z) & object(W)))) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & (ex1_wrt(c,W,d) & (is_the_sum_of_wrt(Z,X,Y,d) & is_the_sum_of_wrt(W,Y,X,d)))))) => a_equal_wrt(Z,W,d))))).
fof(sum_lemma,lemma,(! [X,Y,Z,G] : ((object(X) & (object(Y) & (object(Z) & property(G)))) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & is_the_sum_of_wrt(Z,X,Y,d)))) => (enc_wrt(Z,G,d) <=> (enc_wrt(X,G,d) | enc_wrt(Y,G,d))))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(theorem07,conjecture,(! [X,Y,Z,SumXY,SumYZ,SumSumXYZ,SumXSumYZ] : ((object(X) & (object(Y) & (object(Z) & (object(SumXY) & (object(SumYZ) & (object(SumSumXYZ) & object(SumXSumYZ))))))) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & (ex1_wrt(c,SumXY,d) & (ex1_wrt(c,SumYZ,d) & (ex1_wrt(c,SumSumXYZ,d) & (ex1_wrt(c,SumXSumYZ,d) & (is_the_sum_of_wrt(SumXY,X,Y,d) & (is_the_sum_of_wrt(SumYZ,Y,Z,d) & (is_the_sum_of_wrt(SumSumXYZ,SumXY,Z,d) & is_the_sum_of_wrt(SumXSumYZ,X,SumYZ,d))))))))))) => a_equal_wrt(SumSumXYZ,SumXSumYZ,d))))).
fof(sum_lemma,lemma,(! [X,Y,Z,G] : ((object(X) & (object(Y) & (object(Z) & property(G)))) => ((ex1_wrt(c,X,d) & (ex1_wrt(c,Y,d) & (ex1_wrt(c,Z,d) & is_the_sum_of_wrt(Z,X,Y,d)))) => (enc_wrt(Z,G,d) <=> (enc_wrt(X,G,d) | enc_wrt(Y,G,d))))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(there_are_individual_concepts,conjecture,(? [X] : (object(X) & individual_concept_wrt(X,d)))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
fof(there_are_ordinary_objects,lemma,(? [X] : (object(X) & ex1_wrt(o,X,d)))).
fof(any_concept_of_individual_is_an_individual_concept,lemma,(! [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)))))).
fof(comprehension_for_concept_of_individual_wrt,axiom,(! [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)))))))))))).
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(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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)))))).
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)))))))))).
fof(distinguished_point_d,axiom,point(d)).
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)))))))).
fof(encp_wrt,definition,(! [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)))))))).
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))))))))))).
fof(true_in_wrt,definition,(! [P,X,D] : ((proposition(P) & (object(X) & point(D))) => (true_in_wrt(P,X,D) <=> (situation_wrt(X,D) & encp_wrt(X,P,D)))))).
fof(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(theorem7_world_theory,axiom,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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))))))))))).
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)))))))))).
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)))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(necessity_of_being_a_concept,lemma,(! [X] : (object(X) => (ex1_wrt(c,X,d) => (! [D] : (point(D) => ex1_wrt(c,X,D))))))).
fof(sort_ex1_wrt,axiom,(! [F,X,D] : (ex1_wrt(F,X,D) => (property(F) & (object(X) & point(D)))))).
fof(sort_properties_not_points,axiom,(! [X] : (property(X) => ~ point(X)))).
Used in the proof of:
Comment: (see TPTP representation below).
Dependencies:
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))))))).
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))))))))))).
fof(is_the_world_in_which_appears_wrt,definition,(! [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)))))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(compossibility_is_reflexive,conjecture,(! [X] : (object(X) => (individual_concept_wrt(X,d) => compossible_wrt(X,X,d))))).
fof(compossibility_wrt,definition,(! [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))))))))))).
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)))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(an_individual_concept_contains_the_world_in_which_it_appears,conjecture,(! [C,W,D] : ((object(C) & object(W)) => (individual_concept_wrt(C,d) => (is_the_world_in_which_appears_wrt(W,C,d) => contains_wrt(C,W,d)))))).
fof(every_individual_concept_appears_at_a_unique_world,theorem,(! [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))))))))))).
fof(being_a_concept_is_being_abstract,axiom,(c = a)).
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)))))))))).
fof(contains_wrt,definition,(! [X,Y,D] : ((object(X) & (object(Y) & point(D))) => (contains_wrt(Y,X,D) <=> included_in_wrt(X,Y,D))))).
fof(encp_wrt,definition,(! [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)))))))).
fof(included_in_wrt,definition,(! [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)))))))))).
fof(is_the_world_in_which_appears_wrt,definition,(! [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)))))))))).
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))))))))))).
fof(situation_wrt,definition,(! [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))))))))))).
fof(true_in_wrt,definition,(! [P,X,D] : ((proposition(P) & (object(X) & point(D))) => (true_in_wrt(P,X,D) <=> (situation_wrt(X,D) & encp_wrt(X,P,D)))))).
fof(world_wrt,definition,(! [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))))))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(existence_proposition_plug1,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(theorem7_world_theory,axiom,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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)))))).
fof(compossibility_wrt,definition,(! [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))))))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
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)))))).
fof(compossibility_wrt,definition,(! [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))))))))))).
fof(every_individual_concept_appears_at_a_unique_world,theorem,(! [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))))))))))).
fof(distinguished_point_d,axiom,point(d)).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(individual_concepts_are_complete,conjecture,(! [X] : (object(X) => (individual_concept_wrt(X,d) => complete_wrt(X,d))))).
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)))))))).
fof(complete_wrt,definition,(! [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)))))))).
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)))))))))).
fof(sort_individual_concept_wrt,axiom,(! [X,D] : (individual_concept_wrt(X,D) => (object(X) & point(D))))).
fof(property_negation,definition,(! [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)))))))).
fof(world_wrt,definition,(! [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))))))))))).
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))))))))))).
fof(existence_of_plug1_propositions,axiom,(! [X,F] : ((object(X) & property(F)) => (? [P] : (proposition(P) & plug1(P,F,X)))))).
fof(truth_of_plug1_propositions,axiom,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
fof(individual_concepts_are_singular,conjecture,(! [X] : (object(X) => (individual_concept_wrt(X,d) => singular_wrt(X,d))))).
fof(co_realizers_are_identical,lemma,(! [A,B,C,W,D] : ((object(A) & (object(B) & (object(C) & (object(W) & point(D))))) => ((realizes_in_wrt(A,C,W,D) & realizes_in_wrt(B,C,W,D)) => (A = B))))).
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)))))))).
fof(distinguished_point_d,axiom,point(d)).
fof(singular_wrt,definition,(! [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:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(distinguished_property_a,conjecture,property(a)).
Used in the proof of:
(nothing)
Comment: (see TPTP representation below).
Dependencies:
(none)
fof(distinguished_property_o,conjecture,property(o)).
Used in the proof of:
(nothing)
(No function symbols with non-zero arity.)
Used in:
is_the_disj_concept_of_wrt
Used in:
is_an_actual_world
Used in:
equal_wrt
Used in:
is_a_negation_of
Used in:
a_property_negation_of
Used in:
plug1
Used in:
true_wrt
Used in:
enc_wrt
Used in:
ex1_wrt
Used in:
The principles of our theory comprise everything that is not a theorem or lemma, namely axioms, definitions, and sorting rules:
There are 92 principles: