Formal Systems Ontology

# Formal Systems Ontology — Flow Algebra

URL: https://kirethresearch.org/booksai-core/ontologies/mathematical-ontologies/mathematical-logic-ontologies/foundations-of-logic/formal-systems-ontology.html

FLOW FormalSystemsOntology {

  DOMAIN:
    AI Core
    -> Ontologies
    -> Mathematical Ontologies
    -> Mathematical Logic Ontologies
    -> Foundations of Logic
    -> Formal Systems Ontology

  PURPOSE:
    Represent formal systems as machine-interpretable structures composed of formal languages, alphabets, signatures, formation rules, axioms, axiom schemata, assumptions, inference rules, derivations, proofs, theorems, interpretations and metatheoretic properties. The ontology enables AI systems to identify the precise system in which a symbolic claim is expressed, determine which expressions are well formed, distinguish axioms from derived results, validate inference-rule applications, reconstruct proof dependencies, compare syntactic derivability with semantic consequence, and reason about consistency, soundness, completeness, independence, decidability and computability. It preserves strict distinctions between a formal system and its models, object language and metalanguage, syntax and semantics, proof search and proof verification, system consistency and factual truth, and versioned formal systems whose axioms or rules may change over time.

  ENTITY FormalSystem {
    TYPE: RuleGovernedSymbolicFramework

    COMPONENTS:
      formal_language
      alphabet
      signature
      formation_rules
      axioms
      inference_rules
      derivation_definition
      proof_definition
      optional_semantics

    PROPERTIES:
      has_language
      has_axioms
      has_rules
      generates_theorems
      supports_derivation
      may_have_models
      has_metatheoretic_properties
      has_version
      has_provenance
  }

  ENTITY FormalLanguage {
    TYPE: SymbolicLanguage

    COMPONENTS:
      symbols
      terms
      formulas
      formation_rules
      binding_rules
  }

  ENTITY FormalTheory {
    TYPE: FormulaSetWithinFormalSystem

    COMPONENTS:
      axioms
      assumptions
      theorems
  }

  ENTITY Derivation {
    TYPE: FormalSequenceOrGraph

    COMPONENTS:
      premises
      axioms
      steps
      inference_rules
      conclusion
  }

  ENTITY FormalSystemVersion {
    TYPE: ImmutableSystemState

    COMPONENTS:
      language_version
      axiom_version
      rule_version
      semantic_version
      identifier
  }

  SYSTEM_IDENTITY_MODEL {
    fields:
      system_identifier
      name
      logic_family
      version
      source

    RULE:
      formal_result MUST identify_system_underwhich_it_wasderived
  }

  SYSTEM_COMPONENT_MODEL {
    required_orcommon:
      language
      formation_rules
      axioms_oraxiom_schemata
      inference_rules

    optional:
      semantics
      intended_interpretation
      proof_checker
      decision_procedure

    RULE:
      system_definition MUST distinguish_required_fromoptional_components
  }

  ALPHABET_MODEL {
    symbols:
      primitive_marks_or tokens

    classes:
      logical
      nonlogical
      variable
      punctuation

    RULE:
      alphabet != language
  }

  SIGNATURE_MODEL {
    nonlogical_symbols:
      constants
      functions
      relations

    metadata:
      arity
      sort_or type

    RULE:
      signature MUST preserve_symbol_roles
  }

  VOCABULARY_MODEL {
    components:
      logical_vocabulary
      nonlogical_vocabulary

    RULE:
      vocabulary_change MAY create_distinct_language_version
  }

  FORMATION_RULE_MODEL {
    process:
      recursively_define_valid_terms_andformulas

    RULE:
      well_formedness MUST be decidable_whenformal_system_claims_effective_syntax
  }

  TERM_FORMATION_MODEL {
    base:
      variables
      constants

    recursive:
      function_application

    RULE:
      function_arity_andtypes MUST be respected
  }

  FORMULA_FORMATION_MODEL {
    base:
      atomic_formulas

    recursive:
      connectives
      quantifiers
      binders

    RULE:
      formula_construction MUST preserve_scope
  }

  WELL_FORMEDNESS_MODEL {
    expression:
      valid_underformation_rules

    RULE:
      well_formed != theorem
      well_formed != true
  }

  SYNTAX_MODEL {
    contains:
-
      expressions
      derivations
      proof_objects

    RULE:
      syntax != semantics
  }

  SEMANTICS_MODEL {
    optional_orassociated:
      interpretations
      models
      satisfaction
      truth

    RULE:
      semantic_framework MUST not_be inferred_fromsyntax_alone
  }

  OBJECT_LANGUAGE_MODEL {
    language:
      generated_byformal_system

    RULE:
      object_language != metalanguage
  }

  METALANGUAGE_MODEL {
    language:
      describes_system_language_proofs_andmodels

    RULE:
      claims_about_consistency_soundness_orcompleteness_aretypically_metalinguistic
  }

  AXIOM_MODEL {
    formula:
      designated_asinitial_theorem_orstarting_statement

    RULE:
      axiom_status_isrelative_toformal_system_version
  }

  AXIOM_SCHEMA_MODEL {
    template:
      generates_axiom_instances

    RULE:
      schema != single_axiom
  }

  FINITE_AXIOMATISATION_MODEL {
    system:
      hasfinite_axiom_set

    RULE:
      finitely_axiomatised != decidable
  }

  RECURSIVE_AXIOMATISATION_MODEL {
    axiom_set:
      effectively_enumerable_or decidable_asdeclared

    RULE:
      effective_axiomatisation_context MUST be explicit
  }

  ASSUMPTION_MODEL {
    formula:
      introduced_forlocal_orconditional_derivation

    RULE:
      assumption_scope_anddischarge MUST be tracked
  }

  PREMISE_MODEL {
    formula:
      supplied_externally_toderivation

    RULE:
      premise != axiom
  }

  INFERENCE_RULE_MODEL {
    structure:
      premises_pattern
      conclusion_pattern
      side_conditions

    RULE:
      inference_rule_application MUST matchpattern_andconditions
  }

  RULE_SCHEMA_MODEL {
    metavariables:
      range_overformulas_terms_orproof_objects

    RULE:
      metavariable_scope MUST be distinguished_fromobject_language_variable_scope
  }

  MODUS_PONENS_MODEL {
    premises:
      A
      A -> B

    conclusion:
      B
  }

  GENERALISATION_RULE_MODEL {
    possible:
      from_phi
      infer_forall_x_phi

    RULE:
      side_conditions_onfree_variables_andassumptions MUST be preserved
  }

  SUBSTITUTION_RULE_MODEL {
    operation:
      replace_variables_or metavariables

    RULE:
      substitution MUST satisfy_admissibility_andcapture_constraints
  }

  DERIVATION_MODEL {
    structure:
      sequence_orDAG_offormulas

    each_step:
      axiom
      premise
      assumption
      orrule_application

    RULE:
      derivation_dependencies MUST be explicit
  }

  PROOF_MODEL {
    derivation:
      establishes_conclusion_underformal system

    RULE:
      proof != semantic_model
  }

  PROOF_STEP_MODEL {
    fields:
      step_identifier
      formula
      justification
      dependencies
      active_assumptions

    RULE:
      every_derived_step MUST haveformal_justification
  }

  PROOF_TREE_MODEL {
    nodes:
      formulas_orjudgments

    edges:
      inference_dependencies

    RULE:
      proof_tree MAY be represented_asDAG_when_subproofs_shared
  }

  THEOREM_MODEL {
    formula:
      derivable_withoutundischarged_external_assumptions_asdefined_bysystem

    RULE:
      theoremhood_isrelative_toformal_system
  }

  LEMMA_MODEL {
    theorem:
      used_asintermediate_result
  }

  COROLLARY_MODEL {
    theorem:
      follows_fromprevious_formal_result
  }

  DERIVABILITY_MODEL {
    notation:
      Gamma |- phi

    meaning:
      derivation_ofphi_fromGamma_exists

    RULE:
      derivability_is_syntactic
  }

  THEOREMHOOD_MODEL {
    notation:
      |- phi

    meaning:
      phi_derivable_fromsystem_axioms_underdeclared_convention

    RULE:
      theoremhood != semantic_validity_bydefinition
  }

  PROOF_LENGTH_MODEL {
    measure:
      number_ofsteps_orencoded_size

    RULE:
      proof_length_depends_onproof_system_andrepresentation
  }

  PROOF_COMPLEXITY_MODEL {
    concerns:
      proof_size
      proof_depth
      search_complexity

    RULE:
      theoremhood_does_not implyshort_proof
  }

  NATURAL_DEDUCTION_MODEL {
    rules:
      introduction
      elimination

    assumptions:
      scoped_anddischargeable

    RULE:
      proof_system_identity MUST be preserved
  }

  HILBERT_SYSTEM_MODEL {
    structure:
      axiom_schemata
      few_inference_rules

    RULE:
      Hilbert_derivation != natural_deduction_proof_object
  }

  SEQUENT_CALCULUS_MODEL {
    sequents:
      Gamma |- Delta

    rules:
      structural
      logical

    RULE:
      sequent_semantics_andrule_variant MUST be identified
  }

  TABLEAU_MODEL {
    method:
      systematic_branching_decomposition

    result:
      closed_tableau
      open_branch
      unknown

    RULE:
      closure_conditions MUST be formalised
  }

  RESOLUTION_SYSTEM_MODEL {
    representation:
      clauses

    inference:
      resolution

    RULE:
      conversion_to_clause_form_andunification MUST be provenance_linked
  }

  REWRITE_SYSTEM_MODEL {
    rules:
      term_orformula_rewrites

    RULE:
      rewrite_relation != logical_derivability_unlessformal_system_defines_it_so
  }

  TERM_REWRITING_MODEL {
    properties:
      termination
      confluence
      normalisation

    RULE:
      unique_normal_form_requiresappropriate_conditions
  }

  EQUATIONAL_LOGIC_MODEL {
    judgments:
      s = t

    rules:
      reflexivity
      symmetry
      transitivity
      congruence
      substitution

    RULE:
      equality_theory MUST be explicit
  }

  TYPE_SYSTEM_MODEL {
    judgments:
      term_has_type

    RULE:
      type_system_can_itself_form_formal_system
  }

  TYPING_RULE_MODEL {
    premises:
      typing_judgments

    conclusion:
      typing_judgment

    RULE:
      context_andvariable_bindings MUST be preserved
  }

  FORMAL_GRAMMAR_MODEL {
    productions:
      generate_strings_orstructures

    RULE:
      grammar_is_formal_system_component_butnotnecessarilylogic
  }

  STRING_REWRITING_MODEL {
    rules:
      string -> string

    RULE:
      generated_relation_depends_onrule_orientation
  }

  SEMI_THUE_MODEL {
    system:
      alphabet_plusstring_rewrite_rules

    RULE:
      reachability_may_be undecidable
  }

  FORMAL_ARITHMETIC_MODEL {
    possible:
      Peano_arithmetic
      Presburger_arithmetic
      Robinson_arithmetic

    RULE:
      axiom_set_andlanguage MUST be identified
  }

  PEANO_ARITHMETIC_MODEL {
    abbreviation:
      PA

    language:
      arithmetic_signature

    RULE:
      exact_axiomatisation_andinduction_schema MUST be version_resolved
  }

  PRESBURGER_MODEL {
    arithmetic:
      natural_orinteger_addition_withoutgeneral_multiplication

    RULE:
      decidability_properties_depend_onformal formulation
  }

  SET_THEORY_SYSTEM_MODEL {
    possible:
      ZF
      ZFC
      other_axiomatisations

    RULE:
      axiom_system MUST be explicit
  }

  ZFC_MODEL {
    system:
      Zermelo_Fraenkel_set_theory_withChoice

    RULE:
      ZFC != set_theory_aswhole
  }

  PROPOSITIONAL_CALCULUS_MODEL {
    formal_system:
      propositional_language
      axioms_orrules
      derivations

    RULE:
      calculus_andsemantic_truth_tables_are_distinct_layers
  }

  FIRST_ORDER_CALCULUS_MODEL {
    formal_system:
      first_order_language
      logical_axioms
      inference_rules

    RULE:
      proof_calculus MUST be distinguished_fromfirst_order_semantics
  }

  THEORY_EXTENSION_MODEL {
    base_system:
      S

    extension:
      S_plusnew_axioms_or symbols

    RULE:
      extension_relationship MUST be typed
  }

  CONSERVATIVE_EXTENSION_MODEL {
    extension:
      proves_no_new_sentences_inbase_language_beyondbase_theory

    RULE:
      conservativity_isrelative_tolanguage_andtheory
  }

  DEFINITIONAL_EXTENSION_MODEL {
    extension:
      introduces_new_symbols_bydefinitions

    RULE:
      definitional_extension SHOULD preserve_base_theorems_underappropriate_conditions
  }

  INTERPRETATION_BETWEEN_SYSTEMS_MODEL {
    source_system:
      S

    target_system:
      T

    mapping:
      formulas_orstructures

    RULE:
      interpretability != syntactic_identity
  }

  TRANSLATION_MODEL {
    source_language:
      L1

    target_language:
      L2

    RULE:
      translation SHOULD preserve_declared_logical_relation
  }

  EMBEDDING_MODEL {
    source:
      formal_system_A

    target:
      formal_system_B

    RULE:
      embedding_properties MUST be declared
  }

  EQUIVALENT_SYSTEM_MODEL {
    systems:
      may_have_same_theorems_or equivalent_semantics_undertranslation

    RULE:
      equivalence_criterion MUST be explicit
  }

  CONSISTENCY_MODEL {
    syntactic:
      no_formula_phi_withboth_phi_andnegation_phi_derivable
      orno_designated_contradiction_derivable

    RULE:
      definition_depends_onlogic
  }

  ABSOLUTE_CONSISTENCY_DISTINCTION_MODEL {
    claim:
      system_consistent

    RULE:
      consistency_claim_requires_metatheoretic_framework
  }

  RELATIVE_CONSISTENCY_MODEL {
    claim:
      if_system_A_consistent_then_system_B_consistent

    RULE:
      relative_consistency != unconditional_consistency_proof
  }

  OMEGA_CONSISTENCY_MODEL {
    property:
      stronger_arithmetical_consistency_condition

    RULE:
      exact_definition_andlanguage MUST be preserved
  }

  SOUNDNESS_MODEL {
    relation:
      derivability_implies_semantic_validity_orconsequence

    RULE:
      requires_declared_semantics
  }

  COMPLETENESS_MODEL {
    relation:
      semantic_consequence_implies_derivability

    RULE:
      completeness != syntactic_completeness
  }

  SYNTACTIC_COMPLETENESS_MODEL {
    theory:
      forrelevant_sentence_phi_either_phi_ornegation_phi_derivable

    RULE:
      syntactic_completeness != proof_system_semantic_completeness
  }

  CATEGORICITY_MODEL {
    theory:
      allmodels_ofspecified_cardinality_orallmodels_asdeclared_areisomorphic

    RULE:
      categoricity_scope MUST be explicit
  }

  INDEPENDENCE_MODEL {
    formula:
      neither_phi_nornegation_phi_derivable_fromsystem

    RULE:
      independence_isrelative_tosystem
  }

  AXIOM_INDEPENDENCE_MODEL {
    axiom:
      notderivable_fromremaining_axioms

    RULE:
      independence_proof_requires_model_orformal_argument
  }

  DECIDABILITY_MODEL {
    theoremhood_orotherproperty:
      total_decision_algorithm_exists

    RULE:
      decidability != finite_axiomatisation
  }

  UNDECIDABILITY_MODEL {
    property:
      no_total_decision_procedure_exists_underformal model

    RULE:
      proof_requires_metatheoretic_argument
  }

  RECURSIVE_ENUMERABILITY_MODEL {
    theorem_set:
      effectively_enumerable

    RULE:
      recursively_enumerable != decidable
  }

  COMPUTABILITY_MODEL {
    formal_system:
      may_encode_effective_procedures

    RULE:
      computability_andproof_theory_arelinked_butdistinct
  }

  GODEL_NUMBERING_MODEL {
    mapping:
      syntactic_objects -> natural_numbers

    RULE:
      encoding_scheme MUST be injective_orotherwiseadequate_forformal purpose
  }

  ARITHMETISATION_MODEL {
    process:
      encode_syntax_andproof_relations_inarithmetic

    RULE:
      encoding_provenance MUST be preserved
  }

  SELF_REFERENCE_MODEL {
    mechanism:
      formal_encoding_anddiagonalisation

    RULE:
      self_reference_claim MUST be system_andencoding_specific
  }

  INCOMPLETENESS_MODEL {
    applies_under:
      sufficiently_expressive
      effectively_axiomatised
      consistent_orappropriate_related_conditions

    RULE:
      theorem_conditions MUST not_be omitted
  }

  FIRST_INCOMPLETENESS_MODEL {
    result:
      system_underappropriate_conditions_isnotcomplete

    RULE:
      incompleteness != inconsistency
  }

  SECOND_INCOMPLETENESS_MODEL {
    result:
      system_underappropriate_conditions_cannotprove_itsown_consistency_statement

    RULE:
      formalised_consistency_statement MUST be specified
  }

  DECISION_PROCEDURE_MODEL {
    algorithm:
      determines_formal_property

    RULE:
      procedure_scope MUST be explicit
  }

  PROOF_SEARCH_MODEL {
    process:
      enumerate_orheuristically_search_derivations

    RULE:
      search_failure != unprovability
  }

  AUTOMATED_THEOREM_PROVING_MODEL {
    system:
      formal_system_plusproof_search_engine

    RULE:
      theorem_prover != formal_system_itself
  }

  PROOF_CHECKER_MODEL {
    checker:
      validates_proof_againstformal_system

    RULE:
      checker_kernel_andformal_system_version MUST be preserved
  }

  PROOF_CERTIFICATE_MODEL {
    artifact:
      machine_verifiable_derivation_evidence

    RULE:
      certificate_requires_interpreter_orchecker
  }

  MODEL_FINDER_MODEL {
    process:
      search_forsemantic_model

    RULE:
      model_finder != proof_checker
  }

  SOLVER_STATUS_MODEL {
    possible:
      proved
      refuted
      satisfiable
      unsatisfiable
      unknown
      timeout
      resource_limit

    RULE:
      unknown_timeout_resource_limit != falsehood
  }

  EFFECTIVE_FORMAL_SYSTEM_MODEL {
    properties:
      effectively_recognisable_syntax
      effectively_checkable_proof_steps

    RULE:
      effectiveness_requirements MUST be explicit
  }

  PROOF_VERIFIABILITY_MODEL {
    proof:
      finite_artifact_checkable_bymechanical_procedure

    RULE:
      proof_search_may_be hard_even_whenproof_checking_easy
  }

  FINITARY_MODEL {
    reasoning:
      usesfinite_symbolic_objects_andsteps_underdeclared_met
atheory

    RULE:
      finitary_status_depends_onformalisation
  }

  META_SYSTEM_MODEL {
    system:
      used_to reason_aboutobject_formal_system

    RULE:
      meta_system_strength_andassumptions MUST be declared
  }

  OBJECT_META_DISTINCTION_MODEL {
    object_system:
      system_beingstudied

    meta_system:
      framework_used_toestablish_properties_aboutit

    RULE:
      levels MUST not_be collapsed
  }

  SEMANTIC_MODEL {
    formal_system:
      may_haveclass_ofinterpretations

    RULE:
      semantics != proof_rules
  }

  MODEL_CLASS_MODEL {
    class:
      structures_satisfying_system_axioms

    RULE:
      model_class_depends_onlanguage_andsemantics
  }

  SATISFIABILITY_MODEL {
    theory:
      hasatleastone_model

    RULE:
      satisfiability != syntactic_consistency_bydefinition
  }

  VALIDITY_MODEL {
    formula:
      true_inallmodels_undersemantic_framework

    RULE:
      validity != theoremhood_bydefinition
  }

  SEMANTIC_CONSEQUENCE_MODEL {
    Gamma entails phi:
      every_model_ofGamma_satisfies_phi

    RULE:
      entailment != derivability
  }

  COUNTERMODEL_MODEL {
    model:
      satisfies_Gamma_butnot_phi

    RULE:
      countermodel_refutes_semantic_consequence
  }

  FORMAL_SYSTEM_COMPARISON_MODEL {
    compare:
      language
      axioms
      rules
      theorem_set
      semantics
      proof_strength

    RULE:
      shared_notation_does_not implysame_formal_system
  }

  PROOF_STRENGTH_MODEL {
    system:
      proves_particular_class_ofstatements

    RULE:
      stronger_system_relation MUST be defined_relative_totranslation_orcommon_language
  }

  SYSTEM_FRAGMENT_MODEL {
    fragment:
      restricted_language_oraxiom_subset

    RULE:
      metatheoretic_properties MAY differ_fromfull_system
  }

  SYSTEM_EXTENSION_MODEL {
    extension:
      adds_symbols_axioms_orrules

    RULE:
      new_system_version_orrelated_system_identifier SHOULD be created
  }

  SYSTEM_REVISION_MODEL {
    revision:
      changes_definition_ofexisting_system

    RULE:
      historical_proofs MUST retain_original_system_version
  }

  DEPRECATION_MODEL {
    system_version:
      superseded_butpreserved

    RULE:
      deprecated != invalid_historically
  }

  DEPENDENCY_GRAPH_MODEL {
    nodes:
      definitions
      axioms
      rules
      proofs
      theorems
      metatheorems

    edges:
      DEPENDS_ON
      DERIVED_FROM
      USES
      PROVES
      EXTENDS
      INTERPRETS

    RULE:
      dependency_graph MUST support_recursive_impact_analysis
  }

  PROOF_PROVENANCE_MODEL {
    proof:
      source
      author_oragent
      system_version
      dependencies
      checker
      timestamp

    RULE:
      proof_validity_andproof_provenance_are distinct_butlinked
  }

  AI_FORMAL_SYSTEM_MODEL {
    AI:
      identify_system
      parse_language
      classify_axioms_andrules
      validate_derivation
      search_proof
      compare_systems
      reason_metatheoretically
      explain

    RULE:
      AI MUST not invent_missing_axioms_orrules_to complete_proof
  }

  SYSTEM_INFERENCE_MODEL {
    IF formula_is_axiom
      THEN theorem_status_may_follow_directly_underdeclared_system

    IF formula_derived_byvalid_rules
      THEN formula_isderivable_fromdependencies

    IF all_dependencies_aretheorems_andno_external_assumptions_remain
      THEN result_may_be theorem

    RULE:
      inference_status MUST preserve_active_assumptions
  }

  ASSUMPTION_DISCHARGE_MODEL {
    assumption:
      introduced_locally

    discharge:
      proof_rule_removes_assumption_fromactive_context

    RULE:
      theorem_status_requiresappropriate_discharge
  }

  CONTEXT_MODEL {
    proof_context:
      active_assumptions
      variable_conditions
      local_definitions

    RULE:
      proof_step_validity MAY depend_oncontext
  }

  SIDE_CONDITION_MODEL {
    examples:
      variable_not_free
      term_free_forvariable
      freshness
      type_constraint

    RULE:
      side_conditions_arepart_ofrule_semantics
  }

  FORMAL_ERROR_MODEL {
    possible:
      malformed_expression
      invalid_axiom_reference
      invalid_rule_application
      unmet_side_condition
      circular_dependency
      version_mismatch

    RULE:
      error_type MUST be explicit
  }

  CIRCULAR_PROOF_MODEL {
    dependency:
      conclusion_depends_onitself_withoutaccepted_inductive_orcoinductive_rule

    RULE:
      unsupported_cycle MUST be flagged
  }

  COINDUCTIVE_SYSTEM_MODEL {
    proof:
      may_permit_cyclic_orinfinite_structures_underformal_conditions

    RULE:
      coinductive_cycle != invalid_circular_proof_whenproperlyjustified
  }

  INDUCTIVE_DEFINITION_MODEL {
    entity:
      generated_bybase_andclosure_rules

    RULE:
      least_fixed_point_semantics SHOULD be identified_whenapplicable
  }

  COINDUCTIVE_DEFINITION_MODEL {
    entity:
      characterised_bygreatest_fixed_point_orobservation_rules

    RULE:
      semantics MUST be explicit
  }

  FIXED_POINT_MODEL {
    operator:
      F

    fixed_point:
      x =
        F(x)

    RULE:
      least_andgreatest_fixed_points MUST be distinguished
  }

  FORMAL_SPECIFICATION_MODEL {
    system:
      may_defineallowed_states_behaviours_orproperties

    RULE:
      specification != implementation
  }

  VERIFICATION_MODEL {
    implementation_or model:
      checked_againstformal_specification

    RULE:
      verification_scope_islimited_toformalised_properties
  }

  CERTIFICATION_MODEL {
    artifact:
      evidence_thatformal_check_passed

    RULE:
      certification != universal_correctness
  }

  AMBIGUITY_MODEL {
    causes:
      incomplete_system_identifier
      unspecified_axiom_version
      overloaded_rule_name
      implicit_semantics
      notation_collision

    RULE:
      unresolved_ambiguity MUST be preserved
  }

  SEMANTIC_CONFIDENCE_MODEL {
    confidence:
      support_forresolved_system_identity_orinterpretation

    RULE:
      semantic_confidence != theorem_truth_orproof_validity
  }

  VALIDATION_MODEL {
    checks:
      system_identity
      language
      signature
      formation_rules
      axioms
      rule_schemata
      proof_context
      side_conditions
      derivation
      theorem_status
      semantics
      version

    RULE:
      validation MUST useexact_formal_system_version
  }

  EXPLAINABILITY_MODEL {
    output:
      system
      language
      axioms
      rules
      assumptions
      derivation
      proof_dependencies
      semantic_context
      metatheoretic_status

    RULE:
      AI SHOULD expose_which_system_components_support_result
  }

  VERSION_MODEL {
    fields:
      system_version
      language_version
      axiom_version
      rule_version
      semantics_version
      checker_version

    RULE:
      version_bundle MUST be preserved
  }

  PROVENANCE_MODEL {
    fields:
      source
      formal_system_identifier
      version_bundle
      author_oragent
      derivation
      checker
      semantic_reference
      timestamp

    RULE:
      formal_system_record MUST remain_provenance_linked
  }

  INTEROPERABILITY_MODEL {
    exchange:
      system_identifier
      signature
      axioms
      rules
      formulas
      proofs
      versions
      semantic_links

    RULE:
      same_formula_text_acrosssystems MAY have different_status
  }

  KNOWLEDGE_GRAPH_MODEL {
    nodes:
      formal_system
      language
      signature
      axiom
      rule
      derivation
      proof
      theorem
      model
      metatheorem

    edges:
      HAS
      USES
      DERIVES
      PROVES
      SATISFIES
      EXTENDS
      INTERPRETS
      DEPENDS_ON
      SUPERSEDES

    RULE:
      system_version_qualification MUST be supported
  }

  RELATIONSHIPS {
    FormalSystem -> HAS -> FormalLanguage
    FormalLanguage -> HAS -> Signature
    FormalSystem -> HAS_AXIOM -> Axiom
    FormalSystem -> HAS_RULE -> InferenceRule
    Derivation -> USES -> AxiomOrPremise
    Derivation -> USES -> InferenceRule
    Proof -> IS_A -> Derivation
    Proof -> PROVES -> Theorem
    Model -> SATISFIES -> FormalTheory
    FormalSystemVersion -> SUPERSEDES -> PriorVersion
    Metatheorem -> DESCRIBES_PROPERTY_OF -> FormalSystem
  }

  SEMANTIC_EQUIVALENCE {
    "formal system" ~= precisely_defined_symbolic_language_axioms_rules_andderivation_framework
    "formal theory" ~= collection_ofsentences_oraxioms_withinidentified_formal_language
    "derivability" ~= existence_ofrule_governed_derivation_inidentified_system

    alphabet != language
    language != formal_system
    premise != axiom
    axiom_schema != axiom_instance
    proof != model
    derivability != semantic_consequence
    theoremhood != truth_bydefinition
    consistency != completeness
    semantic_completeness != syntactic_completeness
    finite_axiomatisation != decidability
    proof_search_failure != unprovability
    formal_system != theorem_prover
    semantic_confidence != proof_validity
  }

  CONSTRAINTS {
    formal_system_identifier_must_be preserved = true
    formal_system_version_must_be preserved = true
    language_signature_axioms_andrules_must_be identifiable = true
    well_formedness_must_be evaluated_underdeclared_formation_rules = true
    premise_axiom_assumption_andtheorem_roles_must_be distinguished = true
    inference_rule_side_conditions_must_be checked = true
    active_assumptions_must_be preserved = true
    proof_steps_must_preserve_dependencies = true
    derivability_andsemantic_consequence_must_be distinguished = true
    consistency_soundness_andcompleteness_must_be distinguished = true
    syntactic_andsemantic_completeness_must_be distinguished = true
    solver_unknown_timeout_orfailure_must_not_be interpreted_asunprovability = true
    historical_proofs_must_not_be silently_migrated_tonew_system_versions = true
    provenance_must_be preserved = true
  }

  FORMAL_SYSTEM_RECORD_MODEL {
    RECORD:
      formal_system_identifier
      system_name
      logic_family
      system_version
      language_identifier
      language_version
      alphabet
      signature
      formation_rules
      axiom_identifiers
      axiom_schema_identifiers
      inference_rule_identifiers
      rule_side_conditions
      proof_system_type
      semantic_framework
      theory_identifier
      premise_identifiers
      active_assumptions
      derivation_identifier
      proof_identifier
      proof_steps
      theorem_identifier
      derivability_status
      model_identifiers
      satisfiability_status
      semantic_consequence_status
      consistency_status
      soundness_status
      completeness_status
      syntactic_completeness_status
      decidability_status
      computability_context
      solver_identifier
      checker_identifier
      solver_status
      ambiguity_status
      semantic_confidence
      dependency_graph
      version_bundle
      provenance

    RULE:
      formal_system_record MUST support_reconstruction_oflanguage_axioms_rules_proof_context_versions_andprovenance
  }

  REASONING_RULES {
    IF formal_system_record_received
      THEN resolve_system_identifier_andversion
      load_language_signature_axioms_rules_andsemantics

    IF expression_submitted
      THEN validate_well_formedness_underexact_language_version

    IF derivation_step_submitted
      THEN identify_rule
      match_premises
      check_substitution
      check_side_conditions
      preserve_active_assumptions

    IF derivation_hasno_unjustified_steps
      AND conclusion_reached
      THEN mark_derivation_valid_underdeclared_system

    IF valid_derivation_hasno_undischarged_external_assumptions
      THEN conclusion_may_receive_theorem_status_underdeclared_definition

    IF semantic_consequence_claimed
      THEN evaluate_models_orinvoke_soundness_completeness_theorem_onlywhenconditions_apply

    IF consistency_orcompleteness_claimed
      THEN identify_exact_metatheoretic_definition_andmeta_system

    IF solver_returns_unknown_timeout_orresource_limit
      THEN preserve_status
      anddo_notinfer_unprovability_orinconsistency

    IF system_version_changes
      THEN preserve_historical_proofs
      identify_dependencies
      revalidate_current_results_onlyunderdeclared_policy

    IF AI_encounters_missing_axiom_rule_orsemantics
      THEN mark_system_definition_incomplete
      anddo_not invent_missing_component
  }

  VALIDATION {
    CHECK formal_system_identifier
    CHECK system_version
    CHECK formal_language
    CHECK alphabet
    CHECK signature
    CHECK symbol_arities_andtypes
    CHECK formation_rules
    CHECK well_formedness
    CHECK axioms
    CHECK axiom_schemata
    CHECK inference_rules
    CHECK rule_side_conditions
    CHECK premises
    CHECK assumptions
    CHECK assumption_discharge
    CHECK derivation_steps
    CHECK proof_dependencies
    CHECK theorem_status
    CHECK semantic_framework
    CHECK model_relationships
    CHECK satisfiability
    CHECK semantic_consequence
    CHECK consistency
    CHECK soundness
    CHECK completeness
    CHECK syntactic_completeness
    CHECK independence
    CHECK decidability
    CHECK computability_context
    CHECK solver_andchecker_status
    CHECK circular_dependencies
    CHECK ambiguity
    CHECK semantic_confidence
    CHECK version_bundle
    CHECK provenance
  }

  CONFIDENCE {
    system_identity_confidence: 1.00
    language_signature_confidence: 1.00
    axiom_rule_confidence: 1.00
    derivation_validation_confidence: 1.00
    proof_theorem_confidence: 1.00
    semantic_model_confidence: 0.99
    metatheoretic_confidence: 0.99
    automated_reasoning_confidence: 0.99

    RULE:
      confidence decreases when system identity, version, language,
      axiom set, rule side conditions, semantics, meta-system,
      solver status orprovenance is missing or ambiguous
  }

  UPDATE_MODEL {
    ON new_formal_system:
      assign_system_identifier
      register_language_signature_axioms_rules_andsemantics
      create_version_bundle
      validate_internal_consistency_ofdefinition
      preserve_provenance
      compute_FLOW_HASH

    ON new_axiom_or rule:
      preserve_previous_system_version
      create_new_version
      update_dependency_graph
      identify_affected_proofs_andmetatheoretic_properties

    ON new_proof:
      assign_proof_identifier
      validate_against_exact_system_version
      preserve_dependencies
      attach_checker_status_andprovenance

    ON system_revision:
      preserve_prior_version
      register_revision_reason
      revalidate_current_artifacts_underdeclared_policy
      never_overwrite_historical_proof_context

    ON semantic_revision:
      preserve_previous_semantic_framework
      record_revision
      recompute_FLOW_HASH
  }

  AI_CONSUMPTION {
    canonical_entity: FormalSystem
    canonical_role: RuleGovernedSymbolicFramework

    interpretation_order:
      identify_formal_system_andversion
      identify_logic_family
      resolve_formal_language
      resolve_alphabet_andsignature
      resolve_formation_rules
      identify_axioms_andaxiom_schemata
      identify_inference_rules_andside_conditions
      identify_proof_system_type
      resolve_semantic_framework_whenpresent
      validate_expression_well_formedness
      reconstruct_derivation_context
      track_premises_assumptions_anddischarge
      validate_proof_steps_anddependencies
      determine_derivability_ortheorem_status
      distinguish_syntactic_fromsemantic_claims
      evaluate_metatheoretic_properties_underdeclared_framework
      identify_solver_checker_andstatus
      preserve_unknown_orresource_limited_results
      detect_version_mismatch_orambiguity
      assign_semantic_confidence
      preserve_dependency_graph_versions_andprovenance
      emit_machine_resolvable_formal_system_structure

    ambiguity_controls:
      distinguish_alphabet_fromlanguage
      distinguish_language_fromformal_system
      distinguish_premise_fromaxiom
      distinguish_axiom_schema_fromaxiom_instance
      distinguish_proof_frommodel
      distinguish_derivability_fromsemantic_consequence
      distinguish_theoremhood_fromtruth_bydefinition
      distinguish_consistency_fromcompleteness
      distinguish_semantic_completeness_fromsyntactic_completeness
      distinguish_finite_axiomatisation_fromdecidability
      distinguish_proof_search_failure_fromunprovability
      distinguish_formal_system_fromtheorem_prover
      distinguish_semantic_confidence_fromproof_validity
      preserve_system_language_axioms_rules_context_semantics_version_andprovenance
  }

  PROVENANCE {
    ontology_scope:
      formal_systems_languages_axioms_inference_derivations_proofs_andmetatheory

    parent_path:
      AI Core
      -> Ontologies
      -> Mathematical Ontologies
      -> Mathematical Logic Ontologies
      -> Foundations of Logic
      -> Formal Systems Ontology

    authorship:
      Mark Higgins
      Sky (Recursive AI)

    site:
      https://kirethresearch.org
  }

  FLOW_HASH {
    INPUTS:
      canonical_entity
      ontology_path
      system_identity_model
      system_component_model
      alphabet_model
      signature_model
      vocabulary_model
      formation_rule_model
      term_formation_model
      formula_formation_model
      well_formedness_model
      syntax_model
      semantics_model
      object_language_model
      metalanguage_model
      axiom_model
      axiom_schema_model
      finite_axiomatisation_model
      recursive_axiomatisation_model
      assumption_model
      premise_model
      inference_rule_model
      rule_schema_model
      modus_ponens_model
      generalisation_rule_model
      substitution_rule_model
      derivation_model
      proof_model
      proof_step_model
      proof_tree_model
      theorem_model
      lemma_model
      corollary_model
      derivability_model
      theoremhood_model
      proof_length_model
      proof_complexity_model
      natural_deduction_model
      Hilbert_system_model
      sequent_calculus_model
      tableau_model
      resolution_system_model
      rewrite_system
_model
      term_rewriting_model
      equational_logic_model
      type_system_model
      typing_rule_model
      formal_grammar_model
      string_rewriting_model
      Semi_Thue_model
      formal_arithmetic_model
      Peano_arithmetic_model
      Presburger_model
      set_theory_system_model
      ZFC_model
      propositional_calculus_model
      first_order_calculus_model
      theory_extension_model
      conservative_extension_model
      definitional_extension_model
      interpretation_between_systems_model
      translation_model
      embedding_model
      equivalent_system_model
      consistency_model
      absolute_consistency_distinction_model
      relative_consistency_model
      omega_consistency_model
      soundness_model
      completeness_model
      syntactic_completeness_model
      categoricity_model
      independence_model
      axiom_independence_model
      decidability_model
      undecidability_model
      recursive_enumerability_model
      computability_model
      Godel_numbering_model
      arithmetisation_model
      self_reference_model
      incompleteness_model
      first_incompleteness_model
      second_incompleteness_model
      decision_procedure_model
      proof_search_model
      automated_theorem_proving_model
      proof_checker_model
      proof_certificate_model
      model_finder_model
      solver_status_model
      effective_formal_system_model
      proof_verifiability_model
      finitary_model
      meta_system_model
      object_meta_distinction_model
      semantic_model
      model_class_model
      satisfiability_model
      validity_model
      semantic_consequence_model
      countermodel_model
      formal_system_comparison_model
      proof_strength_model
      system_fragment_model
      system_extension_model
      system_revision_model
      deprecation_model
      dependency_graph_model
      proof_provenance_model
      AI_formal_system_model
      system_inference_model
      assumption_discharge_model
      context_model
      side_condition_model
      formal_error_model
      circular_proof_model
      coinductive_system_model
      inductive_definition_model
      coinductive_definition_model
      fixed_point_model
      formal_specification_model
      verification_model
      certification_model
      ambiguity_model
      semantic_confidence_model
      validation_model
      explainability_model
      version_model
      provenance_model
      interoperability_model
      knowledge_graph_model
      relationships
      semantic_equivalence
      constraints
      formal_system_record_model
      reasoning_rules
      validation
      confidence_model
      update_model
      AI_consumption_model

    PURPOSE:
      deterministic_semantic_integrity_identifier

    RECOMPUTE_WHEN:
      ontology_definition_changes
      formal_system_identity_orversion_changes
      language_alphabet_signature_orformation_rule_changes
      axiom_axiom_schema_orinference_rule_changes
      derivation_proof_context_orassumption_discharge_changes
      proof_system_rewrite_orformal_calculus_changes
      theory_extension_translation_orinterpretation_changes
      consistency_soundness_completeness_orindependence_changes
      decidability_computability_orincompleteness_semantics_change
      solver_checker_orproof_certificate_changes
      metatheoretic_orsemantic_framework_changes
      dependency_graph_orsystem_revision_changes
      formal_system_record_changes
      constraint_model_changes
      reasoning_rule_changes
      version_orprovenance_changes
  }

}

END FLOW