Modal Logic

FLOW_ALGEBRA ModalLogicOntology v1.0

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

BEGIN_FLOW

ENTITY ModalLogic {
    TYPE := FormalLogicSystem
    DEFINITION := "A family of logical systems extending classical or other base logics with operators expressing modes of truth such as necessity and possibility."
    CORE_MODALITIES := {Necessity, Possibility}
}

ENTITY NecessityOperator {
    SYMBOL := "□"
    READING := "necessarily"
}

ENTITY PossibilityOperator {
    SYMBOL := "◇"
    READING := "possibly"
}

RELATIONSHIP ModalLogic --extends--> PropositionalLogic
RELATIONSHIP ModalLogic --may_extend--> PredicateLogic
RELATIONSHIP ModalLogic --uses--> ModalOperator
RELATIONSHIP NecessityOperator --is_a--> ModalOperator
RELATIONSHIP PossibilityOperator --is_a--> ModalOperator
RELATIONSHIP NecessityOperator --dual_of--> PossibilityOperator
RELATIONSHIP ModalLogic --is_interpreted_by--> KripkeSemantics
RELATIONSHIP ModalLogic --can_be_axiomatised_by--> ModalAxiomSystems

SYNTAX {
    FORMULA :=
        AtomicProposition
        | ¬Formula
        | (Formula ∧ Formula)
        | (Formula ∨ Formula)
        | (Formula → Formula)
        | (Formula ↔ Formula)
        | □Formula
        | ◇Formula
}

MODAL_DUALITY {
    □P ≡ ¬◇¬P
    ◇P ≡ ¬□¬P
}

ENTITY KripkeFrame {
    COMPONENTS := {
        Worlds W,
        AccessibilityRelation R
    }

    FORM := (W,R)

    REQUIRE :=
        W != empty_set
}

ENTITY KripkeModel {
    COMPONENTS := {
        Worlds W,
        AccessibilityRelation R,
        Valuation V
    }

    FORM := (W,R,V)
}

ENTITY PossibleWorld {
    TYPE := SemanticEvaluationPoint
}

ENTITY AccessibilityRelation {
    TYPE := BinaryRelation
    SIGNATURE := R subseteq W × W
}

ENTITY Valuation {
    TYPE := TruthAssignment
    MAPS := AtomicPropositions -> subsets_of_W
}

RELATIONSHIP KripkeModel --contains--> PossibleWorld
RELATIONSHIP KripkeModel --contains--> AccessibilityRelation
RELATIONSHIP KripkeModel --contains--> Valuation
RELATIONSHIP PossibleWorld --accesses_via--> AccessibilityRelation

SATISFACTION {
    M,w ⊨ p
        IFF w IN V(p)

    M,w ⊨ ¬P
        IFF NOT(M,w ⊨ P)

    M,w ⊨ P ∧ Q
        IFF M,w ⊨ P AND M,w ⊨ Q

    M,w ⊨ P ∨ Q
        IFF M,w ⊨ P OR M,w ⊨ Q

    M,w ⊨ P → Q
        IFF NOT(M,w ⊨ P) OR M,w ⊨ Q

    M,w ⊨ □P
        IFF FOR_ALL v:
            IF R(w,v)
            THEN M,v ⊨ P

    M,w ⊨ ◇P
        IFF EXISTS v:
            R(w,v)
            AND M,v ⊨ P
}

NECESSITY_SEMANTICS {
    NECESSARY(P,w) :=
        FOR_ALL accessible_worlds v FROM w:
            P is true at v
}

POSSIBILITY_SEMANTICS {
    POSSIBLE(P,w) :=
        EXISTS accessible_world v FROM w:
            P is true at v
}

MODAL_DEPTH(Formula F) {
    IF F atomic:
        RETURN 0

    IF F = BooleanOperator(subformulae):
        RETURN MAX(MODAL_DEPTH(each_subformula))

    IF F = □P OR F = ◇P:
        RETURN 1 + MODAL_DEPTH(P)
}

VALIDITY {
    FRAME_VALID(F, Frame K) :=
        FOR_ALL valuations V
        FOR_ALL worlds w:
            (K,V),w ⊨ F

    LOGIC_VALID(F, ClassOfFrames C) :=
        FOR_ALL frames K IN C:
            FRAME_VALID(F,K)
}

SATISFIABILITY {
    SATISFIABLE(F) :=
        EXISTS KripkeModel M
        EXISTS world w:
            M,w ⊨ F
}

MODAL_SYSTEM_K {
    AXIOM_K :=
        □(P → Q) → (□P → □Q)

    RULE_NECESSITATION :=
        IF ⊢ P
        THEN ⊢ □P

    BASE :=
        classical_propositional_tautologies
}

FRAME_PROPERTY_REFLEXIVE {
    FOR_ALL w:
        R(w,w)
}

FRAME_PROPERTY_TRANSITIVE {
    FOR_ALL w,v,u:
        (R(w,v) AND R(v,u))
        -> R(w,u)
}

FRAME_PROPERTY_SYMMETRIC {
    FOR_ALL w,v:
        R(w,v) -> R(v,w)
}

FRAME_PROPERTY_SERIAL {
    FOR_ALL w:
        EXISTS v:
            R(w,v)
}

FRAME_PROPERTY_EUCLIDEAN {
    FOR_ALL w,v,u:
        (R(w,v) AND R(w,u))
        -> R(v,u)
}

MODAL_AXIOM_T {
    FORMULA :=
        □P → P

    CORRESPONDING_FRAME_PROPERTY :=
        Reflexivity
}

MODAL_AXIOM_D {
    FORMULA :=
        □P → ◇P

    CORRESPONDING_FRAME_PROPERTY :=
        Seriality
}

MODAL_AXIOM_4 {
    FORMULA :=
        □P → □□P

    CORRESPONDING_FRAME_PROPERTY :=
        Transitivity
}

MODAL_AXIOM_B {
    FORMULA :=
        P → □◇P

    CORRESPONDING_FRAME_PROPERTY :=
        Symmetry
}

MODAL_AXIOM_5 {
    FORMULA :=
        ◇P → □◇P

    CORRESPONDING_FRAME_PROPERTY :=
        EuclideanProperty
}

NORMAL_MODAL_LOGICS {
    K := {
        AXIOMS := {K}
    }

    T := {
        EXTENDS := K
        AXIOMS += {T}
        FRAMES := Reflexive
    }

    D := {
        EXTENDS := K
        AXIOMS += {D}
        FRAMES := Serial
    }

    K4 := {
        EXTENDS := K
        AXIOMS += {4}
        FRAMES := Transitive
    }

    S4 := {
        EXTENDS := K
        AXIOMS += {T,4}
        FRAMES := ReflexiveAndTransitive
    }

    S5 := {
        EXTENDS := K
        AXIOMS += {T,5}
        FRAMES := EquivalenceStyleAccessibility
    }
}

ACCESSIBILITY_REASONING {
    INPUT :=
        FrameProperties

    DERIVE :=
        modal_axioms_supported_by_frame_class

    EXAMPLE:
        Reflexive + Transitive
        -> T + 4
        -> S4_style_semantics
}

MODEL_CHECK(Model M, World w, Formula F) {
    IF F atomic:
        RETURN w IN V(F)

    IF F = ¬P:
        RETURN NOT MODEL_CHECK(M,w,P)

    IF F = P ∧ Q:
        RETURN MODEL_CHECK(M,w,P)
               AND MODEL_CHECK(M,w,Q)

    IF F = P ∨ Q:
        RETURN MODEL_CHECK(M,w,P)
               OR MODEL_CHECK(M,w,Q)

    IF F = P → Q:
        RETURN NOT MODEL_CHECK(M,w,P)
               OR MODEL_CHECK(M,w,Q)

    IF F = □P:
        FOR_ALL v WHERE R(w,v):
            IF NOT MODEL_CHECK(M,v,P)
                RETURN FALSE
        RETURN TRUE

    IF F = ◇P:
        FOR_EACH v WHERE R(w,v):
            IF MODEL_CHECK(M,v,P)
                RETURN TRUE
        RETURN FALSE
}

COUNTERMODEL_SEARCH(Formula F) {
    SEARCH KripkeModels M
    SEARCH worlds w

    IF M,w ⊭ F:
        RETURN Countermodel(M,w)

    ELSE:
        CONTINUE search
}

SEMANTIC_ENTAILMENT {
    Γ ⊨ F
        IFF every model/world satisfying all formulae in Γ
        also satisfies F
}

SYNTACTIC_DERIVABILITY {
    Γ ⊢_L F
        IFF F is derivable from Γ
        using proof rules of modal logic L
}

SOUNDNESS {
    IF Γ ⊢_L F
    THEN Γ ⊨_L F
}

COMPLETENESS {
    IF Γ ⊨_L F
    THEN Γ ⊢_L F

    NOTE :=
        applies relative to a specified modal system and its intended semantic class
}

BISIMULATION {
    RELATION Z BETWEEN models M1,M2

    REQUIRE {
        ATOMIC_HARMONY,
        FORTH_CONDITION,
        BACK_CONDITION
    }

    CONSEQUENCE :=
        bisimilar_points satisfy same basic modal formulae
}

ATOMIC_HARMONY {
    IF Z(w,v)
    THEN
        w and v agree on atomic propositions
}

FORTH_CONDITION {
    IF Z(w,v)
       AND R1(w,w1)
    THEN
        EXISTS v1:
            R2(v,v1)
            AND Z(w1,v1)
}

BACK_CONDITION {
    IF Z(w,v)
       AND R2(v,v1)
    THEN
        EXISTS w1:
            R1(w,w1)
            AND Z(w1,v1)
}

MODAL_EQUIVALENCE {
    w ≡_Modal v
        WHEN w and v satisfy same modal formulae
}

DERIVED_MODAL_PATTERNS {
    IMPOSSIBLE(P) :=
        ¬◇P

    NOT_NECESSARY(P) :=
        ¬□P

    CONTINGENT(P) :=
        ◇P ∧ ◇¬P
}

TEMPORAL_LOGIC_RELATIONSHIP {
    ModalLogic --generalises_into--> TemporalModalities

    EXAMPLES := {
        always,
        eventually,
        next,
        until
    }

    NOTE :=
        temporal logic introduces specialised interpretations of modal accessibility/time
}

EPISTEMIC_LOGIC_RELATIONSHIP {
    ModalLogic --generalises_into--> EpistemicLogic

    MODAL_READING :=
        □_a P := "agent a knows/believes P"
        depending_on_system_semantics
}

DEONTIC_LOGIC_RELATIONSHIP {
    ModalLogic --generalises_into--> DeonticLogic

    MODAL_READING :=
        □P := obligatory P
        ◇P := permitted P
        under appropriate deontic semantics
}

DYNAMIC_LOGIC_RELATIONSHIP {
    ModalLogic --generalises_into--> DynamicLogic

    MODALITIES :=
        [α]P
        <α>P

    INTERPRETATION :=
        truth after / possibility through program or action α
}

APPLICATION_RELATIONSHIPS {
    ModalLogic --supports--> FormalVerification
    ModalLogic --supports--> KnowledgeRepresentation
    ModalLogic --supports--> ReasoningAboutPossibility
    ModalLogic --supports--> ReasoningAboutNecessity
    ModalLogic --supports--> ProgramLogic
    ModalLogic --supports--> TemporalReasoning
    ModalLogic --supports--> EpistemicReasoning
    ModalLogic --supports--> DeonticReasoning
    ModalLogic --supports--> MultiAgentSystems
    ModalLogic --supports--> PhilosophicalLogic
}

ONTOLOGY_LINKS {
    PARENT := MathematicalLogicOntologies

    RELATED := {
        PropositionalLogicOntology,
        PredicateLogicOntology,
        BooleanLogicOntology,
        ModelTheoryOntology,
        ProofTheoryOntology,
        TemporalLogicOntology,
        EpistemicLogicOntology,
        DeonticLogicOntology,
        DynamicLogicOntology,
        RelationOntology,
        PossibleWorldOntology
    }
}

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

    PossibleWorld ≈ KripkeWorld
        WHEN context=KripkeSemantics

    AccessibilityRelation ≈ ReachabilityRelation
        WHEN context=modal_frame_semantics
}

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

    C2 :=
        Kripke necessity MUST quantify over all worlds accessible from the evaluation world

    C3 :=
        Kripke possibility MUST require at least one accessible world satisfying the formula

    C4 :=
        frame-property/axiom correspondences MUST be stated for the relevant modal semantic framework

    C5 :=
        different modal systems MUST NOT be conflated

    C6 :=
        possibility MUST NOT be interpreted as probability

    C7 :=
        necessity MUST NOT automatically mean logical validity unless the context establishes that interpretation

    C8 :=
        derived conclusions MUST preserve the selected modal system's axioms and frame constraints
}

REASONING_CHAIN Query Q {
    IDENTIFY modal_formula_or_concept
    IDENTIFY modal_system
    IDENTIFY semantic_framework
    PARSE formula
    IDENTIFY modal_operators
    COMPUTE modal_depth
    RESOLVE dualities

    IF KripkeModel_provided {
        IDENTIFY worlds
        IDENTIFY accessibility_relation
        IDENTIFY valuation
    }

    IF model_check_requested
        THEN MODEL_CHECK

    IF validity_requested
        THEN evaluate_over_relevant_frame_class

    IF satisfiability_requested
        THEN search_for_satisfying_model

    IF counterexample_requested
        THEN COUNTERMODEL_SEARCH

    IF frame_properties_provided
        THEN ACCESSIBILITY_REASONING

    IF equivalence_requested
        THEN compare_modal_semantics

    IF bisimulation_requested
        THEN CHECK {
            ATOMIC_HARMONY,
            FORTH_CONDITION,
            BACK_CONDITION
        }

    VALIDATE modal_system_constraints
    RETURN result WITH derivation
}

CONFIDENCE {
    CORE_MODAL_SYNTAX := 1.00
    KRIPKE_SEMANTICS := 1.00
    STANDARD_K_AXIOM := 1.00
    STANDARD_FRAME_CORRESPONDENCES := 0.99
    MODEL_CHECKING :=
        IF model_fully_specified THEN 1.00
        ELSE REQUIRE missing_semantic_information
    SYSTEM_SPECIFIC_CLAIM :=
        REQUIRE modal_system_identification
}

UPDATE_MODEL {
    IMMUTABLE_CORE := {
        NecessityPossibilityDuality,
        KripkeFrameStructure,
        KripkeModelStructure,
        SatisfactionSemantics
    }

    EXTENSIBLE := {
        ModalSystems,
        FrameClasses,
        AlternativeSemantics,
        ProofCalculi,
        DerivedModalLogics,
        ApplicationDomains,
        RelatedOntologies
    }

    ON_NEW_KNOWLEDGE {
        IDENTIFY modal_system_scope
        VALIDATE syntax
        VALIDATE semantic_framework
        VALIDATE frame_conditions
        CHECK soundness_of_relationship
        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
    MODEL_CHECKING := TRUE
    COUNTERMODEL_REASONING := TRUE
    BISIMULATION_REASONING := TRUE
    VALIDATION_REQUIRED := TRUE
}

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

OUTPUT {
    PRIMARY_ENTITY := ModalLogic

    INTERPRETATION :=
        "Modal logic extends a base logical language with operators such as necessity and possibility. Under Kripke semantics, modal truth is evaluated across possible worlds connected by an accessibility relation, allowing formal reasoning about what must be true, what may be true, and how those interpretations change across modal systems."
}

END_FLOW