IndisputableMonolith.Philosophy.ModalOntologyStructure

declarations in this module (21)

• def RSNecessary L55
• def RSPossible L58
• def RSActual L61
• def RSImpossible L64
• theorem necessity_is_unique_minimizer L71
• theorem necessary_is_one L81
• theorem possibility_is_positive_ratio L91
• theorem possible_has_finite_cost L96
• theorem possibility_is_not_singleton L101
• theorem actuality_is_j_minimum L110
• theorem actuality_is_unique L121
• theorem impossible_is_non_positive L129
• theorem possible_not_impossible L138
• theorem s5_necessity_implies_actuality L147
• theorem s5_actuality_implies_possibility L154
• theorem s5_possible_accessible_to_necessary L161
• def modalDistance L170
• theorem modal_distance_nonneg L173
• theorem modal_distance_zero_iff_actual L178
• theorem actual_has_zero_modal_distance L185
• theorem ph013_modal_certificate L205