Predicate Logic

# Predicate Logic — Flow Algebra

URL: https://kirethresearch.org/booksai-core/ontologies/mathematical-ontologies/mathematical-logic-ontologies/predicate-logic.html

FLOW PredicateLogicOntology {

  DOMAIN:
    AI Core
    -> Ontologies
    -> Mathematical Ontologies
    -> Mathematical Logic Ontologies
    -> Predicate Logic

  PURPOSE:
    Represent predicate logic as a machine-interpretable formal system extending propositional logic with individuals, variables, constants, predicates, relations, functions, quantifiers, equality, terms, atomic formulas and structured interpretations. The ontology models first-order syntax and semantics, variable binding, free and bound variables, substitution, quantifier scope, structures, domains, assignments, satisfaction, validity, entailment, derivability, normal forms, Skolemisation, unification, resolution, theorem proving, model finding, natural-language formalisation, ambiguity, versioning and provenance. It enables AI systems to reason about properties and relations of objects rather than treating entire statements as indivisible propositions, while preserving strict distinctions between object language and metalanguage, variables and constants, terms and formulas, predicates and propositions, quantification and aggregation, semantic entailment and syntactic derivability, and classical first-order logic versus non-classical or higher-order extensions.

  ENTITY PredicateLogic {
    TYPE: QuantifiedFormalLogic

    DEFAULT_SCOPE:
      ClassicalFirstOrderLogic

    COMPONENTS:
      signature
      variables
      constants
      function_symbols
      predicate_symbols
      equality
      terms
      formulas
      quantifiers
      interpretations
      variable_assignments
      proof_system
  }

  ENTITY Signature {
    TYPE: NonlogicalVocabulary

    COMPONENTS:
      constant_symbols
      function_symbols_witharities
      predicate_symbols_witharities
  }

  ENTITY Structure {
    TYPE: FirstOrderInterpretation

    COMPONENTS:
      nonempty_domain
      constant_interpretations
      function_interpretations
      predicate_interpretations
  }

  ENTITY VariableAssignment {
    TYPE: Mapping

    MAPPING:
      individual_variables -> domain_elements
  }

  LOGIC_IDENTITY_MODEL {
    canonical:
      classical_first_order_predicate_logic

    RULE:
      logic_variant_andversion MUST be explicit
  }

  SIGNATURE_MODEL {
    signature:
      Sigma

    contains:
      constants
      function_symbols
      relation_symbols

    RULE:
      arity MUST be preserved
  }

  LOGICAL_SYMBOL_MODEL {
    possible:
      NOT
      AND
      OR
      IMPLIES
      IFF
      FORALL
      EXISTS
      EQUALITY
      parentheses

    RULE:
      logical_symbols MUST be distinguished_fromnonlogical_signature
  }

  INDIVIDUAL_VARIABLE_MODEL {
    examples:
      x
      y
      z

    semantic_role:
      range_overdomain_underassignment

    RULE:
      variable != unspecified_constant
  }

  CONSTANT_SYMBOL_MODEL {
    examples:
      a
      b
      c

    interpretation:
      one_domain_element

    RULE:
      constant_symbol != domain_element_byidentity
  }

  FUNCTION_SYMBOL_MODEL {
    symbol:
      f

    arity:
      n

    interpretation:
      domain^n -> domain

    RULE:
      function_symbol != interpreted_function
  }

  PREDICATE_SYMBOL_MODEL {
    symbol:
      P

    arity:
      n

    interpretation:
      subset_ofdomain^n
      orBoolean_relation_underencoding

    RULE:
      predicate_symbol != proposition
  }

  RELATION_SYMBOL_MODEL {
    alias:
      predicate_symbol

    RULE:
      terminology_context SHOULD be preserved
  }

  ZERO_ARITY_PREDICATE_MODEL {
    predicate:
      arity_0

    role:
      proposition_like_symbol

    RULE:
      formalism_mustdeclarewhetherallowed
  }

  TERM_MODEL {
    recursive:
      variable_is_term
      constant_is_term
      function_application_to_terms_is_term

    RULE:
      term != formula
  }

  VARIABLE_TERM_MODEL {
    term:
      individual_variable
  }

  CONSTANT_TERM_MODEL {
    term:
      constant_symbol
  }

  FUNCTION_TERM_MODEL {
    structure:
      f(t1,...,tn)

    RULE:
      argument_count MUST matcharity
  }

  GROUND_TERM_MODEL {
    term:
      contains_no_variables
  }

  ATOMIC_FORMULA_MODEL {
    possible:
      P(t1,...,tn)
      t1 = t2_when_equality_available

    RULE:
      atomic_formula != atomic_term
  }

  COMPOUND_FORMULA_MODEL {
    constructed_from:
      formulas
      logical_connectives
      quantifiers
  }

  WELL_FORMED_FORMULA_MODEL {
    abbreviation:
      WFF

    requirement:
      conforms_tosignature_grammar_andbinding_rules

    RULE:
      well_formedness != truth
  }

  FORMULA_AST_MODEL {
    nodes:
      predicate_application
      equality
      connective
      quantifier

    leaves:
      terms_symbols_variables

    RULE:
      AST MUST preservebinding_structure
  }

  FREE_VARIABLE_MODEL {
    occurrence:
      notwithin_scope_ofmatching_quantifier

    RULE:
      free_status_isoccurrence_specific
  }

  BOUND_VARIABLE_MODEL {
    occurrence:
      within_scope_ofquantifier_binding_samevariable

    RULE:
      variable_entity MAY havebothfree_andbound_occurrences_indifferentlocations
  }

  CLOSED_FORMULA_MODEL {
    sentence:
      formula_withnofree_variables

    RULE:
      sentence_truth_instructure_doesnotdepend_onassignment
  }

  OPEN_FORMULA_MODEL {
    formula:
      hasoneormorefree_variables

    RULE:
      satisfaction_requiresassignment
  }

  VARIABLE_OCCURRENCE_MODEL {
    fields:
      variable_identifier
      formula_position
      free_orbound_status
      binder_identifier
  }

  BINDER_MODEL {
    quantifier:
      bindsvariable_occurrences_withinscope
  }

  SCOPE_MODEL {
    quantifier:
      hasoperand_formula_scope

    RULE:
      scope MUST be structurallyrepresented
  }

  SHADOWING_MODEL {
    nested_quantifier:
      mayreusevariable_symbol

    RULE:
      binder_identity MUST distinguishshadowedoccurrences
  }

  ALPHA_EQUIVALENCE_MODEL {
    formulas:
      differonlyinconsistentrenaming_ofboundvariables

    RULE:
      alpha_equivalent_formulas SHOULD be semanticallyidentified_asbindingvariants
  }

  CAPTURE_AVOIDANCE_MODEL {
    substitution:
      MUST notaccidentally_bindfreevariables

    RULE:
      renameboundvariables_whenrequired
  }

  SUBSTITUTION_MODEL {
    notation:
      phi[x:=t]

    process:
      replacefree_occurrences_ofx_withterm_t

    RULE:
      substitution MUST be capture_avoiding
  }

  FREE_FOR_SUBSTITUTION_MODEL {
    term_t:
      free_forx_inphi_ifsubstitution_causesnovariablecapture

    RULE:
      sidecondition MUST be checked
  }

  UNIVERSAL_QUANTIFIER_MODEL {
    notation:
      forall x phi

    semantics:
      true_instructure_underassignment_ifphi_true_foreverydomain_element_assigned_tox
  }

  EXISTENTIAL_QUANTIFIER_MODEL {
    notation:
      exists x phi

    semantics:
      true_ifphi_true_foratleastone_domain_element_assigned_tox
  }

  QUANTIFIER_DOMAIN_MODEL {
    default_first_order:
      variables_range_overentire_structure_domain

    RULE:
      restricted_quantification_requiresformalencoding_orsemantics
  }

  NONEMPTY_DOMAIN_MODEL {
    classical_standard:
      domain_nonempty

    RULE:
      empty_domain_semantics MUST be separatelydeclared
  }

  UNIVERSAL_INSTANTIATION_MODEL {
    from:
      forall x phi(x)

    infer:
      phi(t)

    RULE:
      term_admissibility_conditions MUST be satisfied
  }

  EXISTENTIAL_GENERALISATION_MODEL {
    from:
      phi(t)

    infer:
      exists x phi(x)

    RULE:
      substitution_relation MUST be valid
  }

  UNIVERSAL_GENERALISATION_MODEL {
    from:
      phi(x)

    infer:
      forall x phi(x)

    RULE:
      x_mustnotdepend_onundischarged_assumptions_inwaysforbiddenbyproofsystem
  }

  EXISTENTIAL_INSTANTIATION_MODEL {
    from:
      exists x phi(x)

    reasoning:
      introducefresh_witness_symbol_undercontrolledscope

    RULE:
      freshness_anddischarge_conditions MUST be preserved
  }

  QUANTIFIER_NEGATION_MODEL {
    NOT forall x phi:
      equivalent_classically_to
      exists x NOT phi

    NOT exists x phi:
      equivalent_classically_to
      forall x NOT phi
  }

  QUANTIFIER_DUALITY_MODEL {
    forall:
      dual_ofexists_undernegation

    exists:
      dual_offorall_undernegation
  }

  NESTED_QUANTIFIER_MODEL {
    example:
      forall x exists y R(x,y)

    RULE:
      quantifier_order_issemantically_material
  }

  QUANTIFIER_ORDER_MODEL {
    compare:
      forall x exists y R(x,y)
      exists y forall x R(x,y)

    RULE:
      formulas_notgenerally_equivalent
  }

  SAME_TYPE_QUANTIFIER_COMMUTATION_MODEL {
    forall x forall y phi:
      equivalent_to forall y forall x phi

    exists x exists y phi:
      equivalent_to exists y exists x phi

    RULE:
      standard_first_order_context
  }

  MIXED_QUANTIFIER_NONCOMMUTATION_MODEL {
    forall_exists:
      generally_noncommutative
  }

  VACUOUS_QUANTIFICATION_MODEL {
    if:
      x_notfree_inphi

    then:
      forall x phi
      and exists x phi
      mayrelate_to phi_under_nonemptydomain_standardsemantics

    RULE:
      exactequivalence depends_ondomain assumptions
  }

  EQUALITY_MODEL {
    symbol:
      =

    semantics:
      identity_ondomain_understandardFOL_withidentity

    RULE:
      equality_may_be logical_oraxiomatised_relation_indifferentformalisms
  }

  REFLEXIVITY_MODEL {
    forall x x=x
  }

  SUBSTITUTIVITY_MODEL {
    equality:
      permitsreplacement_ofidenticals_inappropriatecontexts

    RULE:
      exactschema MUST preserveterm_andformula_structure
  }

  INEQUALITY_MODEL {
    t1 != t2:
      abbreviation_forNOT(t1=t2)
      understandardnotation
  }

  STRUCTURE_MODEL {
    M:
      domain
      interpretation_function

    RULE:
      structure != theory
  }

  DOMAIN_MODEL {
    D:
      set_orcollection_ofindividuals

    RULE:
      domain_elements_neednotbe syntactic_terms
  }

  INTERPRETATION_MODEL {
    constants:
      mapped_toelements

    functions:
      mapped_tooperations

    predicates:
      mapped_torelations
  }

  TERM_EVALUATION_MODEL {
    value:
      [[t]]_M_s

    depends_on:
      structure_M
      assignment_s

    RULE:
      ground_term_value_independent_ofassignment
  }

  SATISFACTION_MODEL {
    notation:
      M,s |= phi

    RULE:
      open_formula_satisfaction depends_onassignment
  }

  SENTENCE_TRUTH_MODEL {
    notation:
      M |= phi

    when:
      phi_closed

    RULE:
      assignment_canbeomitted_forclosedformula
  }

  ATOMIC_SATISFACTION_MODEL {
    P(t1,...,tn):
      true_if tuple_ofterm_values belongs_to interpreted_relation_P
  }

  EQUALITY_SATISFACTION_MODEL {
    t1=t2:
      true_if term_values_areidentical
  }

  CONNECTIVE_SEMANTICS_MODEL {
    NOT_AND_OR_IMPLICATION_IFF:
      evaluated_recursively_fromsubformula_satisfaction

    RULE:
      propositional_semantics_embedded_withinpredicate_logic
  }

  UNIVERSAL_SATISFACTION_MODEL {
    M,s |= forall x phi:
      iff forall d_inD:
        M,s[x:=d] |= phi
  }

  EXISTENTIAL_SATISFACTION_MODEL {
    M,s |= exists x phi:
      iff exists d_inD:
        M,s[x:=d] |= phi
  }

  MODEL_MODEL {
    M:
      model_ofsentence_or theory_ifsatisfiesit
  }

  THEORY_MODEL {
    T:
      set_ofsentences
  }

  MODEL_OF_THEORY_MODEL {
    M |= T:
      iff M_satisfieseverysentence_inT
  }

  SATISFIABILITY_MODEL {
    formula_or theory:
      satisfiable_ifhasatleastone_model
  }

  UNSATISFIABILITY_MODEL {
    formula_or theory:
      no_model_exists
  }

  VALIDITY_MODEL {
    sentence:
      valid_iftrue_inallstructures_ofsignature
  }

  LOGICAL_CONSEQUENCE_MODEL {
    T entails phi:
      everymodel_ofT_isamodel_ofphi
  }

  COUNTERMODEL_MODEL {
    M:
      model_ofpremises
      notmodel_ofconclusion

    RULE:
      countermodel_refutes_entailment
  }

  LOGICAL_EQUIVALENCE_MODEL {
    phi_equivalent_psi:
      same_truth_inallstructures_andassignments_asappropriate

    RULE:
      equivalence_scope MUST be explicit
  }

  ELEMENTARY_EQUIVALENCE_MODEL {
    structures_M_N:
      satisfy_samefirst_order_sentences

    RULE:
      structure_elementary_equivalence != formula_equivalence
  }

  DEFINABILITY_MODEL {
    relation:
      definable_byformula_instructure_orclass

    RULE:
      definability_context MUST be explicit
  }

  DEFINABLE_SET_MODEL {
    formula_phi(x):
      determines_subset_ofdomain_understructure_andparameters
  }

  PARAMETERS_MODEL {
    formula:
      mayuseconstants_orassignedfreevariables_asparameters

    RULE:
      parameter_dependence MUST be preserved
  }

  PROPOSITIONAL_ABSTRACTION_MODEL {
    predicate_formula:
      maybetreated_asatomic_proposition_forpropositional_reasoning

    RULE:
      abstraction_losesinternal_quantifier_andterm_structure
  }

  PREDICATE_VS_PROPOSITION_MODEL {
    predicate:
      requiresarguments_orinterpretation_asrelation

    proposition:
      truth-evaluable_completeclaim

    RULE:
      predicate_symbol != proposition
  }

  TERM_VS_FORMULA_MODEL {
    term:
      denotesobject

    formula:
      expressescondition_withtruth_status

    RULE:
      term != formula
  }

  VARIABLE_VS_CONSTANT_MODEL {
    variable:
      value_fromassignment

    constant:
      fixedinterpretation_withinstructure

    RULE:
      variable != unnamedconstant
  }

  OBJECT_VS_METALANGUAGE_MODEL {
    object_language:
      formulas_terms_symbols

    metalanguage:
      talksaboutformulas_models_proofs

    RULE:
      levels MUST be distinguished
  }

  META_VARIABLE_MODEL {
    examples:
      phi
      psi
      t

    role:
      ranges_overformulas_or terms_inmetalanguage

    RULE:
      metavariable != object_language_variable
  }

  FORMULA_SCHEMA_MODEL {
    pattern:
      metalanguage_template

    RULE:
      schema != individualobject_language_formula
  }

  PRENEX_NORMAL_FORM_MODEL {
    abbreviation:
      PNF

    structure:
      quantifier_prefix
      quantifier_free_matrix

    RULE:
      transformation MUST preserveequivalence_underdeclaredconditions
  }

  QUANTIFIER_PREFIX_MODEL {
    sequence:
      Q1 x1 ... Qn xn
  }

  MATRIX_MODEL {
    prenex:
      quantifier_free_formula_afterprefix

    RULE:
      matrix_term_here != algebraicmatrix
  }

  NEGATION_NORMAL_FORM_MODEL {
    negation:
      pushed_toatomic_formulas

    RULE:
      quantifier_duality_used
  }

  SKOLEMISATION_MODEL {
    purpose:
      eliminate_existential_quantifiers_usingSkolem_symbols

    property:
      satisfiability_preserving_understandardFOL_transformation

    RULE:
      Skolemised_formula != generallylogically_equivalent_tooriginal
  }

  SKOLEM_CONSTANT_MODEL {
    introduced_when:
      existential_hasnouniversal_dependencies
  }

  SKOLEM_FUNCTION_MODEL {
    arguments:
      preceding_universal_variables_onwhichwitnessdepends

    RULE:
      dependency_set MUST be preserved
  }

  SKOLEM_DEPENDENCY_MODEL {
    existential_variable:
      depends_onuniversals_inscope

    RULE:
      incorrectdependency_changessemantics
  }

  CLAUSAL_FORM_MODEL {
    formula:
      transformed_toset_ofclauses

    common_pipeline:
      eliminate_IFF
      eliminate_implication
      NNF
      standardise_variables_apart
      prenex_orcontrolledprocessing
      Skolemise
      drop_universal_quantifiers
      CNF
  }

  STANDARDISE_APART_MODEL {
    variables:
      renameboundvariables_tofreshdistinctnames

    RULE:
      preservesalpha_equivalence
  }

  LITERAL_MODEL {
    positive:
      atomic_formula

    negative:
      NOT atomic_formula
  }

  CLAUSE_MODEL {
    disjunction:
      literals

    variables:
      oftenimplicitly_universallyquantified_inresolution setting

    RULE:
      convention MUST be explicit
  }

  GROUND_ATOM_MODEL {
    atomic_formula:
      containsnogvariables
  }

  GROUND_FORMULA_MODEL {
    formula:
      containsnofree_orboundvariables
      dependingusage

    RULE:
      ground_typicallymeansnovariables_atall
  }

  HERBRAND_UNIVERSE_MODEL {
    elements:
      ground_terms_constructed_fromconstants_andfunctionsymbols

    RULE:
      requiresatleastonegroundterm_oraddedconstant
  }

  HERBRAND_BASE_MODEL {
    atoms:
      allground_atoms_overHerbrand_universe
  }

  HERBRAND_INTERPRETATION_MODEL {
    domain:
      Herbrand_universe

    functions:
      syntactic_term_constructors

    RULE:
      predicate_truth_assignment_definesinterpretation
  }

  HERBRAND_THEOREM_MODEL {
    role:
      connectsfirst_order_satisfiability/unsatisfiability_togroundinstances_underconditions

    RULE:
      exacttheorem_scope MUST be preserved
  }

  UNIFICATION_MODEL {
    input:
      terms_oratoms

    goal:
      substitution_makingexpressions_identical
  }

  UNIFIER_MODEL {
    substitution:
      sigma

    condition:
      sigma(s)=sigma(t)
  }

  MOST_GENERAL_UNIFIER_MODEL {
    abbreviation:
      MGU

    property:
      everyotherunifier_factors_throughMGU

    RULE:
      uniqueness_uptovariablerenaming
  }

  OCCURS_CHECK_MODEL {
    constraint:
      variable_cannotbeunified_withterm_containingitself
      inordinaryfinite_first_orderterms

    RULE:
      omission_changestermtheory
  }

  UN
IFICATION_FAILURE_MODEL {
    possible:
      symbol_mismatch
      arity_mismatch
      occurs_check_failure
      incompatible_constants
  }

  RESOLUTION_MODEL {
    first_order:
      resolvecomplementary_literals_afterunification

    RULE:
      MGU_andparentclauses MUST be preserved
  }

  FACTORING_MODEL {
    clause:
      unifyandmergesimilar_literals

    RULE:
      first_order_resolution_completeness_maydepend_onfactoring
  }

  RESOLUTION_REFUTATION_MODEL {
    premises_plusnegated_goal:
      clausify
      resolve
      deriveempty_clause

    RULE:
      transformation_andunification_provenance MUST be preserved
  }

  EMPTY_CLAUSE_MODEL {
    meaning:
      contradiction
  }

  SUBSUMPTION_MODEL {
    clause_C:
      subsumesD_underappropriate_substitution

    RULE:
      first_order_subsumption_requiresmatching
  }

  THEOREM_PROVING_MODEL {
    input:
      axioms_orpremises
      conjecture

    output:
      proof
      countermodel_whenavailable
      unknown
      timeout

    RULE:
      failedproofsearch != falsehood
  }

  MODEL_FINDING_MODEL {
    goal:
      constructstructure_satisfyingformula_or theory

    RULE:
      finite_model_search_failure != unsatisfiability_withoutcompletenessbasis
  }

  PROOF_SYSTEM_MODEL {
    possible:
      natural_deduction
      sequent_calculus
      Hilbert_system
      resolution

    RULE:
      derivability_status MUST identifyproofsystem
  }

  DERIVABILITY_MODEL {
    T proves phi:
      formalderivation_exists
  }

  SOUNDNESS_MODEL {
    T proves phi:
      implies T entails phi
      forsoundproofsystem
  }

  COMPLETENESS_MODEL {
    classical_first_order_logic:
      semantic_consequence_impliesformalderivability
      forcompleteproofsystem

    RULE:
      completeness != decidability
  }

  COMPACTNESS_MODEL {
    theory:
      satisfiable_ifeveryfinite_subset_satisfiable
      underclassicalFOL

    RULE:
      theorem_scope MUST be explicit
  }

  LOWENHEIM_SKolem_MODEL {
    role:
      relatesexistence_ofmodels_ofdifferentcardinalities

    RULE:
      exactupward_downward_form MUST be distinguished
  }

  UNDECIDABILITY_MODEL {
    first_order_validity:
      notdecidable_ingeneral

    RULE:
      semidecidability_anddecidability MUST be distinguished
  }

  SEMIDECIDABILITY_MODEL {
    valid_formula:
      proofsearch_mayeventuallyfindproof_undercompleteeffectivecalculus

    RULE:
      nontermination_oninvalidcases_possible
  }

  MONADIC_FRAGMENT_MODEL {
    restriction:
      unary_predicates_underdeclaredconditions

    RULE:
      fragment_properties differ_fromgeneralFOL
  }

  GUARDED_FRAGMENT_MODEL {
    restriction:
      quantification_guarded_byatomic_formulas

    RULE:
      syntax MUST be validated_beforefragmentclassification
  }

  TWO_VARIABLE_FRAGMENT_MODEL {
    abbreviation:
      FO2

    restriction:
      onlytwovariable_symbols_reused

    RULE:
      fragment_hasdistinct_decidabilityproperties
  }

  FUNCTION_FREE_MODEL {
    signature:
      nofunctionsymbols_ofpositivearity

    RULE:
      constants_maystilloccur
  }

  RELATIONAL_LOGIC_MODEL {
    signature:
      predicates_andconstants_withoutfunctions_whenrestricted

    RULE:
      relation_arity MUST be preserved
  }

  DATALOG_LINK_MODEL {
    fragment:
      function_free_Horn_rules_underrestrictions

    RULE:
      Datalog_semantics_anddatabase_assumptions MUST be separatelyidentified
  }

  HORN_LOGIC_MODEL {
    clauses:
      atmostonepositive_literal

    RULE:
      first_orderHorn_reasoning_supportslogic_programming_links
  }

  FORWARD_CHAINING_MODEL {
    rules:
      deriveground_orvariable_instantiatedconsequences

    RULE:
      fairness_andtermination_depend_onfragment
  }

  BACKWARD_CHAINING_MODEL {
    goal:
      unifywithruleheads
      generatesubgoals

    RULE:
      searchstrategy != semantic_entailment
  }

  LOGIC_PROGRAMMING_MODEL {
    rules:
      oftenHorn_clause_based

    RULE:
      Prolog_operational_semantics_includingNAF != pureclassicalFOL
  }

  NEGATION_AS_FAILURE_DISTINCTION_MODEL {
    failure_toproveP:
      operational_notP

    RULE:
      NAF != classical_negation
  }

  CLOSED_WORLD_DISTINCTION_MODEL {
    missing_fact:
      maybetreatedfalse_indatabasepolicy

    RULE:
      classicalFOL_doesnotassumeclosedworld
  }

  OPEN_WORLD_MODEL {
    absent_information:
      neitherP_norNOTP_necessarily

    RULE:
      absence != falsity
  }

  UNIQUE_NAMES_DISTINCTION_MODEL {
    constants_a_b:
      maydenotesameelement_instandardFOL

    RULE:
      unique_names_assumption MUST be explicit
  }

  DOMAIN_CLOSURE_DISTINCTION_MODEL {
    domain:
      maycontainunnamed_elements

    RULE:
      domain_closure_assumption_notstandardFOL
  }

  DATABASE_MODEL {
    relation:
      finite_table_likeinterpretation

    RULE:
      database_null_andclosedworld_semantics differ_fromclassicalFOL
  }

  KNOWLEDGE_GRAPH_MODEL {
    entities:
      domain_elements
      predicates
      relations

    RULE:
      graph_edge_semantics MAY be represented_bypredicate_atoms
  }

  RDF_MAPPING_MODEL {
    triple:
      subject_predicate_object

    possible:
      binary_relation_atom

    RULE:
      RDF_open_world_andidentity_semantics MUST be preserved
  }

  ONTOLOGY_MAPPING_MODEL {
    classes:
      unary_predicates

    properties:
      binary_predicates

    RULE:
      description_logic_semantics differs_fromunrestrictedFOL
  }

  DESCRIPTION_LOGIC_DISTINCTION_MODEL {
    DL:
      decidable_fragments_withspecialconstructors

    RULE:
      DL_concepts_roles_andrestrictions MUST notbe treated_asarbitraryFOL_withouttranslation
  }

  NATURAL_LANGUAGE_FORMALISATION_MODEL {
    source:
      natural_language_statement

    process:
      identifyentities
      predicates
      relations
      quantifiers
      negation
      scope
      variables
      constants

    RULE:
      formalisation_isinterpretive
  }

  UNIVERSAL_LANGUAGE_MODEL {
    cues:
      every
      all
      each
      any_undercontext

    candidate:
      forall
  }

  EXISTENTIAL_LANGUAGE_MODEL {
    cues:
      some
      at_least_one
      there_exists
      a_undercontext

    candidate:
      exists
  }

  NO_LANGUAGE_MODEL {
    phrase:
      no_A_is_B

    candidate:
      forall x(A(x) -> NOT B(x))
      or NOT exists x(A(x) AND B(x))

    RULE:
      equivalent_underclassical semantics
  }

  EVERY_MODEL {
    "Every A is B":
      forall x(A(x) -> B(x))
  }

  SOME_MODEL {
    "Some A is B":
      exists x(A(x) AND B(x))
  }

  SOME_NOT_MODEL {
    "Some A is not B":
      exists x(A(x) AND NOT B(x))
  }

  NO_MODEL {
    "No A is B":
      forall x(A(x) -> NOT B(x))
  }

  ONLY_MODEL {
    "Only A are B":
      forall x(B(x) -> A(x))

    RULE:
      direction MUST be carefullypreserved
  }

  RELATIVE_CLAUSE_MODEL {
    source:
      noun_withproperty_orrelation

    RULE:
      mayintroducepredicate_conjunction_orquantifier_scope
  }

  PRONOUN_BINDING_MODEL {
    source:
      pronouns_oranaphora

    RULE:
      coreference MUST be resolved_beforeformalisation
  }

  QUANTIFIER_SCOPE_AMBIGUITY_MODEL {
    example:
      every_student_read_a_book

    candidates:
      forall x(Student(x)->exists y(Book(y) AND Read(x,y)))
      exists y(Book(y) AND forall x(Student(x)->Read(x,y)))

    RULE:
      preservecandidate_readings
  }

  NEGATION_SCOPE_AMBIGUITY_MODEL {
    source:
      not_every
      every_not
      no

    RULE:
      scopechangeslogicalform
  }

  VARIABLE_BINDING_AMBIGUITY_MODEL {
    source:
      repeatedpronouns_orvariables

    RULE:
      bindingstructure MUST be explicit
  }

  IDENTITY_LANGUAGE_MODEL {
    cues:
      is_same_as
      identical_to

    RULE:
      copular_is_doesnotalwaysmeanlogical_equality
  }

  EXISTENTIAL_IMPORT_MODEL {
    categorical_statement:
      universal_doesnotimplyexistence_inmodernFOL

    RULE:
      do_notinferexistence_fromforallx(A->B)
  }

  PRESUPPOSITION_DISTINCTION_MODEL {
    natural_language:
      maypresupposeexistence_oruniqueness

    RULE:
      presupposition != assertedFOL_content_withoutformalisation
  }

  DEFINITE_DESCRIPTION_MODEL {
    phrase:
      the_F

    RULE:
      mayrequireexistence_uniqueness_orRussellian_analysis
  }

  FUNCTIONAL_RELATION_MODEL {
    relation:
      uniqueoutputforeachinput

    RULE:
      predicate_relation != function_untilfunctionalityestablished
  }

  EXISTENCE_UNIQUENESS_MODEL {
    exists_exactly_one_x_phi:
      exists x(phi(x) AND forall y(phi(y)->y=x))

    RULE:
      exactencoding MAY vary
  }

  COUNTING_QUANTIFIER_DISTINCTION_MODEL {
    examples:
      exactly_two
      atleast_three

    RULE:
      notprimitive_inbasicFOL_butdefinable_withidentity_forfixedfinitecounts
  }

  SECOND_ORDER_DISTINCTION_MODEL {
    second_order:
      quantifiesoverpredicates_relations_orfunctions

    RULE:
      first_order_variables_rangeonlyoverindividuals
  }

  HIGHER_ORDER_DISTINCTION_MODEL {
    higher_order:
      variables_mayrange_overfunctions_predicates_orhigher_types

    RULE:
      notbasicFOL
  }

  MANY_SORTED_MODEL {
    variables:
      assignedsorts

    quantifiers:
      range_overcorrespondingdomains

    RULE:
      sort_system MUST be explicit
  }

  SINGLE_SORTED_MODEL {
    standard:
      oneindividualdomain
  }

  TYPED_FIRST_ORDER_MODEL {
    predicates_andfunctions:
      haveinput_outputtypes

    RULE:
      typechecking precedessemanticreasoning
  }

  SORT_ERASURE_MODEL {
    many_sorted_toone_sorted:
      encode sorts_asunarypredicates

    RULE:
      translation_constraints MUST be included
  }

  FREE_LOGIC_MODEL {
    terms:
      mayfailtodenote

    RULE:
      standardFOL_assumesconstantsdenote_andfunctions_total
  }

  PARTIAL_FUNCTION_DISTINCTION_MODEL {
    standardFOL_function:
      total

    RULE:
      partialfunctions requireencoding_oralternative semantics
  }

  INTUITIONISTIC_PREDICATE_LOGIC_MODEL {
    semantics:
      constructive_Kripke_orproof_theoretic

    RULE:
      classicalquantifier_negation_andexcludedmiddle MAY fail
  }

  MODAL_PREDICATE_LOGIC_MODEL {
    dimensions:
      worlds
      domains
      quantifiers

    RULE:
      constant_varying_domain_semantics MUST be identified
  }

  TEMPORAL_PREDICATE_LOGIC_MODEL {
    dimensions:
      time
      individuals
      predicates

    RULE:
      temporalindex MUST be preserved
  }

  PARACONSISTENT_PREDICATE_LOGIC_MODEL {
    contradictions:
      maynotexplode

    RULE:
      logic_specific semantics required
  }

  FUZZY_PREDICATE_LOGIC_MODEL {
    predicate_membership:
      graded

    RULE:
      truthfunctions_andquantifieraggregations MUST be defined
  }

  PROBABILISTIC_LOGIC_DISTINCTION_MODEL {
    probability:
      assignedtoformulas_models_orinterpretations

    RULE:
      probability != first_ordertruth
  }

  MODEL_THEORY_MODEL {
    studies:
      structures
      theories
      definability
      elementary_embeddings
      types

    RULE:
      advancedmodeltheory_entities SHOULD linkto dedicatedontologies
  }

  HOMOMORPHISM_MODEL {
    structures:
      mapping_preservingselectedoperations_relations

    RULE:
      exactpreservationcriterion depends_onlanguage
  }

  ISOMORPHISM_MODEL {
    structures:
      bijective_structure_preserving_mapping

    RULE:
      isomorphicstructures_satisfysamefirst_order_sentences
  }

  EMBEDDING_MODEL {
    mapping:
      injective_structure_preserving

    RULE:
      elementary_embedding_isstronger
  }

  ELEMENTARY_EMBEDDING_MODEL {
    mapping:
      preservestruth_ofallformulas_withparameters

    RULE:
      modeltheoretic_context MUST be explicit
  }

  AUTOMORPHISM_MODEL {
    isomorphism:
      structure_toitself
  }

  THEORY_CONSISTENCY_MODEL {
    syntactic:
      noformalcontradiction_derivable

    semantic:
      satisfiable_hasmodel

    RULE:
      equivalence_requires_soundness_completeness context
  }

  CATEGORICITY_MODEL {
    theory:
      models_ofspecifiedcardinality_uniqueuptoisomorphism

    RULE:
      cardinality_scope MUST be explicit
  }

  COMPLETE_THEORY_MODEL {
    theory:
      forevery_sentence_phi
      T_entails_phi_orT_entails_NOT_phi

    RULE:
      theory_completeness != proofsystem_completeness
  }

  AXIOMATISABILITY_MODEL {
    class_ofstructures:
      definablebysetofsentences

    RULE:
      finite_recursive_orotheraxiomatisability SHOULD be typed
  }

  FINITE_MODEL_MODEL {
    structure:
      finite_domain
  }

  INFINITE_MODEL_MODEL {
    structure:
      infinite_domain
  }

  FINITE_MODEL_PROPERTY_MODEL {
    theory_orformula:
      ifsatisfiable_thenhasfinitemodel

    RULE:
      property_notuniversal_forFOL
  }

  COMPACTNESS_APPLICATION_MODEL {
    use:
      inferexistence_ofmodel_fromfinite_subset satisfiability

    RULE:
      classicalFOL_context
  }

  PROOF_SEARCH_MODEL {
    operations:
      instantiate
      unify
      resolve
      rewrite
      branch

    RULE:
      searchtrace != proof_untilvalidated
  }

  HEURISTIC_MODEL {
    possible:
      term_ordering
      literal_selection
      clause_weight
      depth_limit

    RULE:
      heuristic_choice != inference_rule
  }

  UNKNOWN_STATUS_MODEL {
    possible:
      timeout
      resource_limit
      incomplete_model_search
      unsupported_fragment

    RULE:
      unknown != false
      unknown != invalid
  }

  PROOF_CERTIFICATE_MODEL {
    artifact:
      derivation_orresolution_refutation

    RULE:
      checker_version SHOULD be preserved
  }

  MODEL_CERTIFICATE_MODEL {
    artifact:
      explicitstructure_andinterpretation

    RULE:
      validateallsentences_againstmodel
  }

  EXPLAINABILITY_MODEL {
    output:
      signature
      formula
      variable_bindings
      quantifier_scope
      structure_orproof
      substitutions
      result

    RULE:
      explanation MUST exposebinding_andquantifier_scope
  }

  AMBIGUITY_MODEL {
    possible:
      quantifier_scope
      variable_binding
      predicate_arity
      constant_vsvariable
      equality_vspredication
      natural_language_formalisation

    RULE:
      ambiguity MUST be resolved_orpreserved
  }

  SEMANTIC_CONFIDENCE_MODEL {
    confidence:
      support_forformalisation_structure_orinterpretation

    RULE:
      confidence != truth_orvalidity
  }

  VERSION_MODEL {
    versioned:
      signature
      formula
      theory
      proofsystem
      semantics
      ontology

    RULE:
      results MUST preserveversions
  }

  PROVENANCE_MODEL {
    fields:
      source
      formalisation
      signature
      parser
      structure
      proof
      solver
      version
      agent

    RULE:
      predicate_logic_record MUST remainprovenance_linked
  }

  INTEROPERABILITY_MODEL {
    exchange:
      signature
      typed_symbols
      term_ASTs
      formula_AST
      binder_graph
      theory
      structure
      assignment
      proof_or model

    RULE:
      surfaceformula_withoutbinding_andarity_metadata_isnotlossless
  }

  KNOWLEDGE_GRAPH_MODEL {
    nodes:
      variable
      constant
      function
      predicate
      term
      formula
      quantifier
      structure
      domain_element
      proof

    edges:
      OCCURS_IN
      BINDS
      APPLIES_TO
      INTERPRETED_AS
      SATISFIES
      ENTAILS
      DERIVES
      SUBSTITUTES

    RULE:
      syntax_semantics_andproof_edges MUST be typed
  }

  RELATIONSHIPS {
    PredicateLogic -> HAS -> Signature
    Signature -> DECLARES -> PredicateSymbol
    Signature -> DECLARES -> FunctionSymbol
    Signature -> DECLARES -> ConstantSymbol
    Formula -> CONTAINS -> Term
    Quantifier -> BINDS -> IndividualVariable
    Structure -> HAS_DOMAIN -> Domain
    Structure -> INTERPRETS -> SignatureSymbol
    VariableAssignment -> MAPS -> DomainElement
    Structure -> SATISFIES -> Formula
    Proof -> DERIVES -> Formula
  }

  SEMANTIC_EQUIVALENCE {
    "predicate logic" ~= quantified_logic_withterms_predicates_relations_andindividual_variables
    "first-order logic" ~= predicate_logic_wherequantifiedvariables_range_overindividuals
    "structure" ~= domain_plusinterpretations_ofnonlogical_symbols

    variable != constant
    constant_symbol != domain_element
    function_symbol != interpreted_function
    predicate_symbol != proposition
    term != formula
    free_occurrence != bound_occurrence
    object_variable != metavariable
    satisfaction != derivability
    entailment != implication_formula
    satisfiable != valid
    Skolemisation != logical_equivalence
    NAF != classical_negation
    absent_fact != false_fact
    first_order != second_order
    semantic_confidence != truth
  }

  CONSTRAINTS {
    logic_signature_andversion_must_be preserved = true
    symbol_arities_must_be explicit = true
    terms_andformulas_must_be distinguished = true
    variables_constants_functions_andpredicates_must_be distinguished = true
    free_andbound_occurrences_must_be tracked = true
    quantifier_scope
_andbinder_identity_must_be preserved = true
    substitution_must_be capture_avoiding = true
    classical_first_order_domain_must_be nonempty_unlessalternative_declared = true
    structure_assignment_andformula_context_must_be preserved_foropen_formula_satisfaction = true
    semantic_entailment_and syntactic_derivability_must_be distinguished = true
    Skolemisation_must_be labelled_satisfiability_preserving_notgeneral_equivalence = true
    unification_must_checkarity_symbols_andoccurs_condition_understandardterms = true
    open_world_absence_must_not_be interpreted_asfalse = true
    natural_language_quantifier_scope_ambiguity_must_be preserved = true
    nonclassical_andhigher_order_extensions_must_be separatelyidentified = true
    provenance_must_be preserved = true
  }

  PREDICATE_LOGIC_RECORD_MODEL {
    RECORD:
      logic_identifier
      logic_version
      signature_identifier
      variable_symbols
      constant_symbols
      function_symbols_andarities
      predicate_symbols_andarities
      equality_status
      source_formula
      formula_AST
      term_ASTs
      free_variables
      bound_variables
      binder_graph
      quantifier_prefix
      quantifier_scope
      substitutions
      structure_identifier
      domain
      symbol_interpretations
      variable_assignment
      satisfaction_status
      satisfiability_status
      validity_status
      entailment_status
      countermodel
      theory_identifier
      proofsystem_identifier
      derivability_status
      normal_form
      Skolem_symbols
      clauses
      unifiers
      proof_identifier
      model_certificate
      ambiguity_status
      semantic_confidence
      version
      provenance

    RULE:
      predicate_logic_record MUST support_reconstruction_ofsyntax_binding_semantics_models_proofs_andprovenance
  }

  REASONING_RULES {
    IF predicate_formula_received
      THEN identifylogic_signature_andversion
      parse_terms_predicates_connectives_andquantifiers
      constructAST_andbinder_graph
      validatearities_andwellformedness

    IF substitution_requested
      THEN identifyfree_occurrences
      checkfree_forcondition
      renameboundvariables_ifneeded
      performcapture_avoiding_substitution

    IF structure_andassignment_supplied
      THEN evaluateterms
      recursivelyevaluatesatisfaction

    IF universal_quantifier
      THEN evaluatebody_foreverydomain_element_underupdatedassignment

    IF existential_quantifier
      THEN searchforatleastonewitness_domain_element

    IF entailment_requested
      THEN searchforcountermodel_orconstructformalproof
      preservemethod_andstatus

    IF clausification_requested
      THEN preserveoriginalformula
      standardiseapart
      performvalidatedtransformations
      recordSkolem_dependencies
      distinguishsatisfiability_preservation_fromequivalence

    IF resolution_requested
      THEN identifycomplementary_predicate_literals
      computeMGU
      checkoccurs_condition
      constructresolvent
      preserveparentclauses_andunifier

    IF natural_language_received
      THEN identifyquantifiers_predicates_relations_entities_andnegation
      preservequantifier_scope_coreference_andbindingambiguity

    IF proof_or_model_search_returnsunknown
      THEN preserveunknown_timeout_orresource_status
      anddo_notinferfalsehood

    IF signature_formula_theory_orlogic_revision_occurs
      THEN preservehistorical_record
      recursively_revalidate_currentmodels_proofs_andsemanticrelations
  }

  VALIDATION {
    CHECK logic_identifier
    CHECK logic_version
    CHECK signature
    CHECK constant_symbols
    CHECK function_arities
    CHECK predicate_arities
    CHECK variables
    CHECK term_wellformedness
    CHECK formula_wellformedness
    CHECK AST
    CHECK free_bound_occurrences
    CHECK binder_graph
    CHECK quantifier_scope
    CHECK alpha_renaming
    CHECK substitution
    CHECK capture_avoidance
    CHECK equality
    CHECK structure
    CHECK nonempty_domain
    CHECK interpretations
    CHECK assignment
    CHECK term_evaluation
    CHECK satisfaction
    CHECK satisfiability
    CHECK validity
    CHECK entailment
    CHECK countermodel
    CHECK theory
    CHECK derivability
    CHECK proofsystem
    CHECK prenex_NNF
    CHECK Skolemisation
    CHECK clauses
    CHECK unification
    CHECK occurs_check
    CHECK resolution
    CHECK proof_or_model_certificate
    CHECK natural_language_formalisation
    CHECK ambiguity
    CHECK semantic_confidence
    CHECK version
    CHECK provenance
  }

  CONFIDENCE {
    signature_resolution_confidence: 1.00
    term_parsing_confidence: 1.00
    formula_binding_confidence: 1.00
    quantifier_scope_confidence: 0.99
    substitution_confidence: 1.00
    model_semantics_confidence: 1.00
    unification_resolution_confidence: 1.00
    natural_language_formalisation_confidence: 0.94
    provenance_confidence: 1.00

    RULE:
      confidence decreases when signature, arity, binder scope,
      structure, assignment, proof system, natural-language scope,
      version orprovenance is missing or ambiguous
  }

  UPDATE_MODEL {
    ON new_formula:
      assign_formula_identifier
      attachlogic_signature_andversion
      parseAST_andbinder_graph
      validatewellformedness
      preserveprovenance
      compute_FLOW_HASH

    ON new_structure:
      registerdomain_andinterpretations
      validatearity_andtotality_requirements
      attachmodelprovenance

    ON new_proof_or_model:
      attachproof_certificate_orstructure
      validateagainstformula_andtheory
      preserveverification_status

    ON signature_revision:
      preserveprevious_signature
      create_newversion
      identifyaffectedformulas_models_andproofs
      recursivelyrevalidate

    ON semantic_revision:
      preserve_previous_definition
      record_revision
      recompute_FLOW_HASH
  }

  AI_CONSUMPTION {
    canonical_entity: PredicateLogic
    canonical_role: QuantifiedFormalLogic

    interpretation_order:
      identify_logic_variant_andversion
      resolve_signature
      classify_variables_constants_functions_andpredicates
      parse_terms_andatomic_formulas
      constructformula_AST
      resolvequantifier_binders_andscopes
      classifyfree_andbound_occurrences
      validatearity_andwellformedness
      performcapture_avoiding_substitution_whenrequired
      resolveequality_semantics
      resolve_structure_domain_andinterpretations
      resolvevariable_assignment
      evaluate_term_denotations_andformula_satisfaction
      determine_satisfiability_validity_orentailment
      preservecountermodel_whenavailable
      distinguishsemantic_entailment_fromderivability
      transformtoNNF_prenex_orclausalform_whenrequested
      preserveSkolem_dependencies_andtransformation_status
      performunification_andresolution_whenrequested
      preserveproof_model_orunknownstatus
      resolve_natural_language_quantification_andbinding
      detectambiguity
      assignsemantic_confidence
      preserveversions_andprovenance
      emit_machine_resolvable_predicate_logic_structure

    ambiguity_controls:
      distinguish_variable_fromconstant
      distinguish_constant_symbol_fromdomain_element
      distinguish_function_symbol_frominterpreted_function
      distinguish_predicate_symbol_fromproposition
      distinguish_term_fromformula
      distinguish_free_occurrence_frombound_occurrence
      distinguish_object_variable_frommetavariable
      distinguish_satisfaction_fromderivability
      distinguish_entailment_fromimplication_formula
      distinguish_satisfiable_fromvalid
      distinguish_Skolemisation_fromlogical_equivalence
      distinguish_NAF_fromclassical_negation
      distinguish_absent_fact_fromfalse_fact
      distinguish_first_order_fromsecond_order
      distinguish_semantic_confidence_fromtruth
      preserve_signature_arity_AST_binding_structure_model_assignment_proof_version_andprovenance
  }

  PROVENANCE {
    ontology_scope:
      predicate_logic_first_order_terms_quantifiers_structures_semantics_unification_resolution_andAI_reasoning

    parent_path:
      AI Core
      -> Ontologies
      -> Mathematical Ontologies
      -> Mathematical Logic Ontologies
      -> Predicate Logic

    authorship:
      Mark Higgins
      Sky (Recursive AI)

    site:
      https://kirethresearch.org
  }

  FLOW_HASH {
    INPUTS:
      canonical_entity
      ontology_path
      logic_identity_model
      signature_model
      logical_symbol_model
      individual_variable_model
      constant_symbol_model
      function_symbol_model
      predicate_symbol_model
      relation_symbol_model
      zero_arity_predicate_model
      term_model
      variable_term_model
      constant_term_model
      function_term_model
      ground_term_model
      atomic_formula_model
      compound_formula_model
      well_formed_formula_model
      formula_AST_model
      free_variable_model
      bound_variable_model
      closed_formula_model
      open_formula_model
      variable_occurrence_model
      binder_model
      scope_model
      shadowing_model
      alpha_equivalence_model
      capture_avoidance_model
      substitution_model
      free_for_substitution_model
      universal_quantifier_model
      existential_quantifier_model
      quantifier_domain_model
      nonempty_domain_model
      universal_instantiation_model
      existential_generalisation_model
      universal_generalisation_model
      existential_instantiation_model
      quantifier_negation_model
      quantifier_duality_model
      nested_quantifier_model
      quantifier_order_model
      same_type_quantifier_commutation_model
      mixed_quantifier_noncommutation_model
      vacuous_quantification_model
      equality_model
      reflexivity_model
      substitutivity_model
      inequality_model
      structure_model
      domain_model
      interpretation_model
      term_evaluation_model
      satisfaction_model
      sentence_truth_model
      atomic_satisfaction_model
      equality_satisfaction_model
      connective_semantics_model
      universal_satisfaction_model
      existential_satisfaction_model
      model_model
      theory_model
      model_of_theory_model
      satisfiability_model
      unsatisfiability_model
      validity_model
      logical_consequence_model
      countermodel_model
      logical_equivalence_model
      elementary_equivalence_model
      definability_model
      definable_set_model
      parameters_model
      propositional_abstraction_model
      predicate_vs_proposition_model
      term_vs_formula_model
      variable_vs_constant_model
      object_vs_metalanguage_model
      meta_variable_model
      formula_schema_model
      prenex_normal_form_model
      quantifier_prefix_model
      matrix_model
      negation_normal_form_model
      Skolemisation_model
      Skolem_constant_model
      Skolem_function_model
      Skolem_dependency_model
      clausal_form_model
      standardise_apart_model
      literal_model
      clause_model
      ground_atom_model
      ground_formula_model
      Herbrand_universe_model
      Herbrand_base_model
      Herbrand_interpretation_model
      Herbrand_theorem_model
      unification_model
      unifier_model
      most_general_unifier_model
      occurs_check_model
      unification_failure_model
      resolution_model
      factoring_model
      resolution_refutation_model
      empty_clause_model
      subsumption_model
      theorem_proving_model
      model_finding_model
      proof_system_model
      derivability_model
      soundness_model
      completeness_model
      compactness_model
      Lowenheim_Skolem_model
      undecidability_model
      semidecidability_model
      monadic_fragment_model
      guarded_fragment_model
      two_variable_fragment_model
      function_free_model
      relational_logic_model
      Datalog_link_model
      Horn_logic_model
      forward_chaining_model
      backward_chaining_model
      logic_programming_model
      negation_as_failure_distinction_model
      closed_world_distinction_model
      open_world_model
      unique_names_distinction_model
      domain_closure_distinction_model
      database_model
      knowledge_graph_model
      RDF_mapping_model
      ontology_mapping_model
      description_logic_distinction_model
      natural_language_formalisation_model
      universal_language_model
      existential_language_model
      no_language_model
      every_model
      some_model
      some_not_model
      no_model
      only_model
      relative_clause_model
      pronoun_binding_model
      quantifier_scope_ambiguity_model
      negation_scope_ambiguity_model
      variable_binding_ambiguity_model
      identity_language_model
      existential_import_model
      presupposition_distinction_model
      definite_description_model
      functional_relation_model
      existence_uniqueness_model
      counting_quantifier_distinction_model
      second_order_distinction_model
      higher_order_distinction_model
      many_sorted_model
      single_sorted_model
      typed_first_order_model
      sort_erasure_model
      free_logic_model
      partial_function_distinction_model
      intuitionistic_predicate_logic_model
      modal_predicate_logic_model
      temporal_predicate_logic_model
      paraconsistent_predicate_logic_model
      fuzzy_predicate_logic_model
      probabilistic_logic_distinction_model
      model_theory_model
      homomorphism_model
      isomorphism_model
      embedding_model
      elementary_embedding_model
      automorphism_model
      theory_consistency_model
      categoricity_model
      complete_theory_model
      axiomatisability_model
      finite_model_model
      infinite_model_model
      finite_model_property_model
      compactness_application_model
      proof_search_model
      heuristic_model
      unknown_status_model
      proof_certificate_model
      model_certificate_model
      explainability_model
      ambiguity_model
      semantic_confidence_model
      version_model
      provenance_model
      interoperability_model
      knowledge_graph_model
      relationships
      semantic_equivalence
      constraints
      predicate_logic_record_model
      reasoning_rules
      validation
      confidence_model
      update_model
      AI_consumption_model

    PURPOSE:
      deterministic_semantic_integrity_identifier

    RECOMPUTE_WHEN:
      ontology_definition_changes
      logic_identity_signature_symbol_orarity_changes
      term_formula_AST_binding_orquantifier_scope_changes
      substitution_alpha_equivalence_orcapture_avoidance_changes
      structure_domain_interpretation_orassignment_semantics_change
      satisfaction_validity_entailment_orlogical_equivalence changes
      prenex_Skolemisation_clausal_form_orHerbrand_semantics_change
      unification_resolution_factoring_orproofsystem_changes
      fragment_decidability_compactness_orcompleteness_context changes
      natural_language_quantifier_binding_orformalisation changes
      first_order_higher_order_nonclassical_orontology_mapping distinctions change
      predicate_logic_record_changes
      constraint_model_changes
      reasoning_rule_changes
      version_orprovenance_changes
  }

}

END FLOW