Necessity Ontology

FLOW_ALGEBRA NecessityOntology v1.0

TARGET_URL := "https://kirethresearch.org/booksai-core/ontologies/mathematical-ontologies/mathematical-logic-ontologies/modal-logic/necessity-ontology.html"
LANGUAGE := "en-GB"
DOMAIN := MathematicalOntologies > MathematicalLogicOntologies > ModalLogic > NecessityOntology

BEGIN_FLOW

ENTITY Necessity {
    TYPE := ModalConcept
    SYMBOL := "□"
    DEFINITION := "A modal condition expressing that a proposition is true at every world accessible from the current evaluation world under the selected modal semantics."
}

ENTITY NecessityOperator {
    TYPE := UnaryModalOperator
    SYMBOL := "□"
    OPERAND := ModalFormula
    RESULT := ModalFormula
}

RELATIONSHIP Necessity --is_expressed_by--> NecessityOperator
RELATIONSHIP NecessityOperator --belongs_to--> ModalLogic
RELATIONSHIP NecessityOperator --dual_of--> PossibilityOperator
RELATIONSHIP Necessity --is_interpreted_by--> KripkeSemantics
RELATIONSHIP Necessity --depends_on--> AccessibilityRelation
RELATIONSHIP Necessity --applies_to--> Proposition

SYNTAX {
    IF P IS ModalFormula
    THEN □P IS ModalFormula
}

READING {
    □P := "It is necessary that P"
    □P := "P holds necessarily"
}

KRIPKE_SEMANTICS {
    M,w ⊨ □P
    IFF
        FOR_ALL v:
            R(w,v) -> M,v ⊨ P
}

NECESSARY_AT(Model M, World w, Formula P) {
    FOR_EACH world v IN Worlds(M) {
        IF R(w,v)
           AND NOT(M,v ⊨ P)
        THEN
            RETURN FALSE
    }

    RETURN TRUE
}

ACCESSIBLE_WORLD_SET {
    ACCESSIBLE(w) :=
        {v ∈ W | R(w,v)}

    NECESSITY_CONDITION :=
        FOR_ALL v ∈ ACCESSIBLE(w):
            P(v)=TRUE
}

VACUOUS_NECESSITY {
    IF ACCESSIBLE(w)=empty_set
    THEN
        M,w ⊨ □P
        FOR every P
        under standard universal Kripke semantics

    NOTE :=
        serial frame conditions prevent worlds with no accessible successor
}

DUALITY {
    □P ≡ ¬◇¬P

    DERIVATION {
        □P
        IFF no accessible world satisfies ¬P
        IFF ¬◇¬P
    }
}

NEGATION_OF_NECESSITY {
    ¬□P ≡ ◇¬P

    INTERPRETATION :=
        "P is not necessary exactly when there is an accessible world where P is false."
}

POSSIBILITY_FROM_NEGATION {
    ◇P ≡ ¬□¬P
}

LOGICAL_VALIDITY_DISTINCTION {
    NECESSARY_AT_WORLD :=
        truth_at_all_worlds_accessible_from_specific_world

    VALID_IN_MODEL :=
        truth_at_every_world_in_model

    LOGICALLY_VALID :=
        truth_at_every relevant world in every relevant model

    CONSTRAINT :=
        these concepts MUST NOT be automatically conflated
}

FRAME_REFLEXIVITY {
    PROPERTY :=
        FOR_ALL w:
            R(w,w)

    CONSEQUENCE_FOR_NECESSITY :=
        □P -> P

    MODAL_AXIOM := T
}

FRAME_SERIALITY {
    PROPERTY :=
        FOR_ALL w:
            EXISTS v:
                R(w,v)

    CONSEQUENCE_FOR_NECESSITY :=
        □P -> ◇P

    MODAL_AXIOM := D
}

FRAME_TRANSITIVITY {
    PROPERTY :=
        FOR_ALL w,v,u:
            (R(w,v) AND R(v,u))
            -> R(w,u)

    CONSEQUENCE_FOR_NECESSITY :=
        □P -> □□P

    MODAL_AXIOM := 4
}

FRAME_SYMMETRY {
    PROPERTY :=
        FOR_ALL w,v:
            R(w,v) -> R(v,w)

    ASSOCIATED_MODAL_AXIOM :=
        P -> □◇P
}

FRAME_EUCLIDEAN {
    PROPERTY :=
        FOR_ALL w,v,u:
            (R(w,v) AND R(w,u))
            -> R(v,u)

    ASSOCIATED_MODAL_AXIOM :=
        ◇P -> □◇P
}

SYSTEM_K {
    NECESSITY_DISTRIBUTION :=
        □(P -> Q) -> (□P -> □Q)

    RULE :=
        IF theorem(P)
        THEN theorem(□P)
}

DISTRIBUTION_OVER_CONJUNCTION {
    □(P ∧ Q) ≡ □P ∧ □Q
}

ONE_WAY_DISJUNCTION_RELATION {
    (□P ∨ □Q) -> □(P ∨ Q)

    CONVERSE :=
        NOT valid in general
}

IMPLICATION_REASONING {
    GIVEN:
        □(P -> Q)
        □P

    DERIVE:
        □Q
}

NECESSITATION_RULE {
    IF ⊢ P
    THEN ⊢ □P

    CONSTRAINT :=
        necessitation applies to theorems according to the proof system;
        it is not unrestricted inference from arbitrary assumptions
}

NESTED_NECESSITY {
    □□P :=
        "It is necessary that P is necessary."

    SEMANTICS :=
        FOR_ALL v accessible_from w:
            FOR_ALL u accessible_from v:
                M,u ⊨ P
}

TRANSITIVE_COLLAPSE_DIRECTION {
    IF frame_is_transitive
    THEN
        □P -> □□P
}

REFLEXIVE_COLLAPSE_DIRECTION {
    IF frame_is_reflexive
    THEN
        □□P -> □P

    DERIVATION :=
        apply T to formula □P
}

S4_RELATIONSHIP {
    FRAME := ReflexiveAndTransitive
    AXIOMS := {T,4}

    CONSEQUENCES_INCLUDE {
        □P -> P
        □P -> □□P
    }
}

S5_RELATIONSHIP {
    STANDARD_KRIPKE_FRAME_STYLE :=
        equivalence_relation_accessibility

    NECESSITY :=
        truth throughout the relevant equivalence class
}

GLOBAL_NECESSITY_SPECIAL_CASE {
    IF R = W × W
    THEN
        □P at any world
        IFF P holds at every world in model
}

IDENTITY_ACCESSIBILITY_SPECIAL_CASE {
    IF R = {(w,w) | w∈W}
    THEN
        □P at w
        IFF P at w
}

NECESSITY_FAILURE_WITNESS {
    IF M,w ⊭ □P
    THEN
        EXISTS v:
            R(w,v)
            AND M,v ⊭ P

    v := counterexample_accessible_world
}

MODEL_CHECK_NECESSITY(Model M, World w, Formula P) {
    successors := ACCESSIBLE(w)

    FOR_EACH v IN successors {
        IF MODEL_CHECK(M,v,P)=FALSE
            RETURN {
                value := FALSE,
                witness := v
            }
    }

    RETURN {
        value := TRUE,
        witness := NONE
    }
}

NECESSITY_PRESERVATION_UNDER_BISIMULATION {
    IF worlds w and v are bisimilar
    THEN
        □P has same truth value at w and v
        for every formula P of the basic modal language
}

MONOTONICITY_WITH_RESPECT_TO_FORMULA_ENTAILMENT {
    IF P -> Q IS valid
    THEN
        □P -> □Q IS valid
}

ACCESSIBILITY_EXPANSION_EFFECT {
    GIVEN same valuation and world w

    IF accessibility_successors_of_w_are_added
    THEN
        satisfying □P can become harder

    REASON :=
        necessity universally quantifies over accessible worlds
}

ACCESSIBILITY_RESTRICTION_EFFECT {
    GIVEN same valuation and world w

    IF accessibility_successors_of_w_are_removed
    THEN
        satisfying □P can become easier
}

QUANTIFIER_ANALOGY {
    □P at w
        structurally resembles
        universal_quantification_over_accessible_worlds

    IMPORTANT :=
        modal necessity is not identical to ordinary first-order universal quantification
}

FIRST_ORDER_MODAL_NECESSITY {
    FORM :=
        □φ(x)

    REQUIRES_EXPLICIT_SEMANTICS_FOR {
        Domains,
        VariableAssignments,
        RigidOrNonRigidDesignation,
        QuantifierModalInteraction
    }
}

BARCAN_RELATIONSHIP {
    FORMULAE_MAY_INCLUDE {
        ∀x□P(x) -> □∀xP(x)
        □∀xP(x) -> ∀x□P(x)
    }

    WARNING :=
        validity depends on domain semantics and modal assumptions;
        no unconditional equivalence should be inferred
}

EPISTEMIC_SPECIALISATION {
    □_a P
        MAY represent knowledge_or_belief_of_agent_a

    REQUIRE :=
        epistemic interpretation of accessibility relation
}

DEONTIC_SPECIALISATION {
    □P
        MAY represent obligation_that_P

    REQUIRE :=
        deontic semantic framework
}

TEMPORAL_SPECIALISATION {
    necessity_like universal modalities
        MAY represent truth across specified temporal alternatives

    REQUIRE :=
        temporal frame semantics
}

PROVABILITY_SPECIALISATION {
    □P
        MAY be interpreted as
        "P is provable"

    REQUIRE :=
        provability logic semantics

    WARNING :=
        provability necessity is not identical to arbitrary Kripke necessity
}

APPLICATION_RELATIONSHIPS {
    Necessity --supports--> ModalReasoning
    Necessity --supports--> FormalVerification
    Necessity --supports--> InvariantReasoning
    Necessity --supports--> KnowledgeRepresentation
    Necessity --supports--> EpistemicLogic
    Necessity --supports--> DeonticLogic
    Necessity --supports--> TemporalLogic
    Necessity --supports--> ProvabilityLogic
    Necessity --supports--> PhilosophicalLogic
}

ONTOLOGY_LINKS {
    PARENT := ModalLogicOntology

    RELATED := {
        PossibilityOntology,
        KripkeFrameOntology,
        KripkeModelOntology,
        PossibleWorldOntology,
        AccessibilityRelationOntology,
        ModalOperatorOntology,
        PropositionalLogicOntology,
        PredicateLogicOntology,
        ModelTheoryOntology,
        EpistemicLogicOntology,
        DeonticLogicOntology,
        TemporalLogicOntology
    }
}

SEMANTIC_EQUIVALENCE {
    □P ≈ Necessarily(P)
    □P ≈ P_is_necessary
    □P ≈ ¬◇¬P

    ¬□P ≈ ◇¬P

    NecessityOperator ≈ BoxOperator
        WHEN context=ModalLogic

    AccessibleWorld ≈ RSuccessor
        WHEN context=KripkeSemantics
}

CONSTRAINTS {
    C1 :=
        necessity MUST be interpreted relative to a modal semantics or proof system

    C2 :=
        under Kripke semantics □P at w MUST quantify over every R-accessible world from w

    C3 :=
        one accessible counterexample to P MUST falsify □P at w

    C4 :=
        absence of accessible worlds makes □P vacuously true under standard universal Kripke semantics

    C5 :=
        necessity MUST NOT be conflated with probability, certainty or frequency without an explicit specialised semantics

    C6 :=
        local necessity MUST NOT automatically be equated with global validity

    C7 :=
        modal axiom consequences MUST respect the selected frame properties

    C8 :=
        necessitation MUST follow the restrictions of the chosen proof system

    C9 :=
        first-order modal necessity MUST state domain assumptions when quantifier interaction matters

    C10 :=
        semantic transformations MUST preserve truth under the selected modal framework
}

REASONING_CHAIN Query Q {
    IDENTIFY necessity_statement
    IDENTIFY operand_formula P
    IDENTIFY modal_system
    IDENTIFY semantic_framework

    PARSE □P
    RESOLVE necessity_aliases
    RESOLVE duality □P ≡ ¬◇¬P

    IF KripkeModel_provided {
        IDENTIFY current_world w
        IDENTIFY accessibility_relation R
        COMPUTE ACCESSIBLE(w)
        CHECK P at every accessible world
    }

    IF any_accessible_counterexample_found
        THEN RETURN necessity_false WITH witness

    IF no_accessible_counterexample_found
        THEN RETURN necessity_true

    IF frame_properties_provided {
        CHECK Reflexivity
        CHECK Seriality
        CHECK Transitivity
        CHECK Symmetry
        CHECK EuclideanProperty
    }

    IF axiom_T_context
        THEN permit □P -> P

    IF axiom_D_context
        THEN permit □P -> ◇P

    IF axiom_4_context
        THEN permit □P -> □□P

    IF first_order_modal_context
        THEN identify_domain_semantics

    IF specialised_modal_context
        THEN identify interpretation_of_box_operator

    VALIDATE constraints
    RETURN result WITH derivation
}

CONFIDENCE {
    CORE_NECESSITY_DEFINITION := 1.00
    KRIPKE_NECESSITY_SEMANTICS := 1.00
    NECESSITY_POSSIBILITY_DUALITY := 1.00
    STANDARD_FRAME_CORRESPONDENCES := 0.99

    MODEL_CHECKING :=
        IF complete_model_and_world_given THEN 1.00
        ELSE REQUIRE missing_information

    SPECIALISED_MODAL_INTERPRETATION :=
        REQUIRE semantic_context
}

UPDATE_MODEL {
    IMMUTABLE_CORE := {
        NecessityOperator,
        KripkeUniversalAccessibilitySemantics,
        NecessityPossibilityDuality
    }

    EXTENSIBLE := {
        ModalSystems,
        FrameProperties,
        FirstOrderModalSemantics,
        SpecialisedModalInterpretations,
        ProofRules,
        ApplicationDomains,
        RelatedOntologies
    }

    ON_NEW_KNOWLEDGE {
        IDENTIFY modal_context
        VALIDATE operator_semantics
        VALIDATE frame_assumptions
        CHECK system_compatibility
        CHECK semantic_consistency
        ADD relationship IF non_contradictory
        UPDATE confidence
    }
}

AI_CONSUMPTION {
    MACHINE_READABLE := TRUE
    HUMAN_INTERPRETABLE := TRUE
    RECURSIVE_REASONING := TRUE
    ENTITY_RESOLUTION := TRUE
    SYMBOL_RESOLUTION := TRUE
    RELATIONSHIP_TRAVERSAL := TRUE
    POSSIBLE_WORLD_REASONING := TRUE
    ACCESSIBILITY_REASONING := TRUE
    NECESSITY_EVALUATION := TRUE
    COUNTEREXAMPLE_WORLD_DETECTION := TRUE
    FRAME_PROPERTY_REASONING := TRUE
    VALIDATION_REQUIRED := TRUE
}

FLOW_HASH {
    TARGET := TARGET_URL
    SUBJECT := "Necessity Ontology"
    VERSION := "1.0"
    CANONICAL_SIGNATURE :=
        HASH(TARGET + SUBJECT + DOMAIN + VERSION)
}

OUTPUT {
    PRIMARY_ENTITY := Necessity

    INTERPRETATION :=
        "Necessity is the modal condition represented by □. Under standard Kripke semantics, □P is true at a world exactly when P is true at every world accessible from it. Its behaviour therefore depends on the accessibility relation, the selected modal system and the distinction between local modal truth and global logical validity."
}

END_FLOW