Set Ontology

FLOW ALGEBRA
TITLE: Set Theory Ontology
VERSION: 1.0
DOMAIN: Discrete Mathematics / Set Theory
SOURCE_URL: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/set-theory/set-theory-ontology-2.html
STATUS: Domain-based formalisation; source page content not independently verified.
AUTHORS: Mark Higgins — Sky (Recursive AI)
PROJECT: Kireth Semantic Library

FLOW "SetTheoryOntology" v1.0 {
  DOMAIN: "Discrete Mathematics / Set Theory"
  PURPOSE: "Represent sets, membership, set operations and their formal consequences with explicit assumptions and provenance."

  TYPES {
    Entity: abstract
    Set <: Entity
    Element <: Entity
    FiniteSet <: Set
    InfiniteSet <: Set
    EmptySet <: Set
    UniversalSet <: Set  # always relative to a specified universe
    OrderedPair <: Entity
    Relation <: Set
    Function <: Relation
    CardinalNumber <: Entity
    Proposition <: Entity
    Proof <: Entity
    Source <: Entity
  }

  RELATIONSHIPS {
    MEMBER_OF(Element, Set): Boolean
    SUBSET_OF(Set, Set): Boolean
    PROPER_SUBSET_OF(Set, Set): Boolean
    DISJOINT_WITH(Set, Set): Boolean
    EQUIVALENT_CARDINALITY(Set, Set): Boolean
    BIJECTION_BETWEEN(Set, Set): Boolean
    DERIVED_FROM(Proposition, Source): Boolean
    PROVED_BY(Proposition, Proof): Boolean
  }

  OPERATIONS {
    UNION(A:Set, B:Set) -> Set
    INTERSECTION(A:Set, B:Set) -> Set
    DIFFERENCE(A:Set, B:Set) -> Set
    SYMMETRIC_DIFFERENCE(A:Set, B:Set) -> Set
    COMPLEMENT(A:Set, U:UniversalSet) -> Set  # require A subset of U
    CARTESIAN_PRODUCT(A:Set, B:Set) -> Set
    POWER_SET(A:Set) -> Set
    CARDINALITY(A:Set) -> CardinalNumber
  }

  AXIOMS_AND_SEMANTICS {
    EXTENSIONALITY: A = B iff forall x (x in A iff x in B)
    EMPTY_SET: forall x (x not_in EMPTY)
    SUBSET: A subseteq B iff forall x (x in A implies x in B)
    PROPER_SUBSET: A subset B iff A subseteq B and A != B
    UNION: x in UNION(A,B) iff (x in A or x in B)
    INTERSECTION: x in INTERSECTION(A,B) iff (x in A and x in B)
    DIFFERENCE: x in DIFFERENCE(A,B) iff (x in A and x not_in B)
    POWER_SET: X in POWER_SET(A) iff X subseteq A
    CARTESIAN_PRODUCT: (a,b) in CARTESIAN_PRODUCT(A,B) iff a in A and b in B
    COMPLEMENT: x in COMPLEMENT(A,U) iff x in U and x not_in A
    NOTE: "Unrestricted comprehension is not permitted; use a consistent axiomatic foundation such as ZF/ZFC when required."
  }

  INFERENCE_RULES {
    R1: MEMBER_OF(x,A) and SUBSET_OF(A,B) => MEMBER_OF(x,B)
    R2: SUBSET_OF(A,B) and SUBSET_OF(B,C) => SUBSET_OF(A,C)
    R3: SUBSET_OF(A,B) and SUBSET_OF(B,A) => A = B
    R4: MEMBER_OF(x,INTERSECTION(A,B)) => MEMBER_OF(x,A) and MEMBER_OF(x,B)
    R5: MEMBER_OF(x,A) => MEMBER_OF(x,UNION(A,B))
    R6: DISJOINT_WITH(A,B) iff INTERSECTION(A,B) = EMPTY
    R7: A = B => POWER_SET(A) = POWER_SET(B)
    R8: finite(A) => CARDINALITY(POWER_SET(A)) = 2 ^ CARDINALITY(A)
    R9: finite(A) and finite(B) => CARDINALITY(CARTESIAN_PRODUCT(A,B)) = CARDINALITY(A) * CARDINALITY(B)
    R10: BIJECTION_BETWEEN(A,B) => EQUIVALENT_CARDINALITY(A,B)
  }

  CONSTRAINTS {
    TYPE_CHECK: "Membership arguments must have appropriate element/set roles."
    UNIVERSE_CHECK: "Complement requires an explicit universe U and A subseteq U."
    FINITENESS_CHECK: "Finite cardinality formulae require finite operands."
    CONSISTENCY_CHECK: "Reject contradictions and unsupported unrestricted set formation."
    EVIDENCE_CHECK: "Distinguish proved statements from conjectures and heuristics."
  }

  CONFIDENCE {
    PROVED_THEOREM: 1.0
    VERIFIED_DERIVATION: 1.0
    UNVERIFIED_ASSERTION: null
    POLICY: "Do not convert uncertainty scores into mathematical truth values."
  }

  SEMANTIC_EQUIVALENCE {
    "subseteq" <=> "is_subset_of"
    "element_of" <=> "member_of"
    "intersection" <=> "set_meet"  # contextual synonym only
    POLICY: "Preserve strict vs non-strict subset and membership vs inclusion distinctions."
  }

  PROVENANCE {
    SOURCE_URL: "https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/set-theory/set-theory-ontology-2.html"
    SOURCE_VERIFICATION: "not verified"
    DERIVATION_RECORD: [source_id, axiom_ids, rule_ids, timestamp, reviewer]
  }

  FLOW_HASH {
    METHOD: "SHA-256"
    INPUT: "Canonical UTF-8 serialization of versioned ontology content excluding the FLOW_HASH value itself"
    VALUE: "COMPUTE_ON_PUBLICATION"
  }

  UPDATE_MODEL {
    TRIGGER: [axiom_revision, relation_revision, new_proof, corrected_definition]
    PROCEDURE: [validate_types, check_consistency, rerun_inferences, update_provenance, increment_version, recompute_hash]
    INVALIDATION: "Recheck dependent theorems when definitions or axioms change."
  }

  AI_CONSUMPTION {
    FORMAT: "typed semantic flow"
    CAPABILITIES: [entity_resolution, set_operation_reasoning, theorem_dependency_tracing, proof_validation, cross_ontology_alignment]
    GUARDRAILS: [no_unjustified_axioms, no_false_equivalence, no_unproven_claim_as_fact, retain_provenance]
    OUTPUT: [typed_entities, validated_relations, inferred_propositions, proof_traces, uncertainty_flags]
  }
}

END FLOW ALGEBRA