Subset Ontology

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

1. PURPOSE
Represent subset and proper-subset relationships, validate set inclusion, and support sound set-theoretic inference across finite and infinite sets.

2. TYPED ENTITIES
  Set(id: URI, elements: optional Set[Object], cardinality: optional Cardinal)
  Element(id: URI, type: optional Class)
  SubsetAssertion(left: Set, right: Set, proper: Boolean, provenance: Evidence)
  MembershipAssertion(element: Element, set: Set, truth: TruthValue)
  Cardinal(value: NaturalNumber | InfiniteCardinal)
  Evidence(source: URI, method: String, timestamp: optional DateTime)
  TruthValue = TRUE | FALSE | UNKNOWN

3. RELATIONSHIPS
  MEMBER_OF(x, A) : Element x Set -> TruthValue
  SUBSET_OF(A, B) : Set x Set -> TruthValue
  PROPER_SUBSET_OF(A, B) : Set x Set -> TruthValue
  EQUAL_SET(A, B) : Set x Set -> TruthValue
  DISJOINT(A, B) : Set x Set -> TruthValue
  INTERSECTION(A, B) : Set x Set -> Set
  UNION(A, B) : Set x Set -> Set

4. FORMAL SEMANTICS
  SUBSET_OF(A, B) <=> forall x (MEMBER_OF(x,A) => MEMBER_OF(x,B))
  PROPER_SUBSET_OF(A, B) <=> SUBSET_OF(A,B) and not EQUAL_SET(A,B)
  EQUAL_SET(A, B) <=> SUBSET_OF(A,B) and SUBSET_OF(B,A)
  EMPTY_SET subset_of A for every set A.
  SUBSET_OF(A,A) is TRUE for every set A.
  Proper subset is irreflexive; subset is reflexive.

5. FLOW OPERATORS
  flow ASSERT_SUBSET(A:Set, B:Set) -> SubsetAssertion
    require WELL_FORMED(A) and WELL_FORMED(B)
    evaluate forall x in A: MEMBER_OF(x,B)
    emit SUBSET_OF(A,B) when all memberships are proven
    otherwise emit FALSE on counterexample, UNKNOWN on incomplete evidence

  flow INFER_PROPER_SUBSET(A:Set, B:Set) -> TruthValue
    require SUBSET_OF(A,B) == TRUE
    if exists x: MEMBER_OF(x,B) == TRUE and MEMBER_OF(x,A) == FALSE
      return TRUE
    if EQUAL_SET(A,B) == TRUE: return FALSE
    return UNKNOWN

  flow TRANSITIVE_SUBSET(A:Set, B:Set, C:Set) -> TruthValue
    if SUBSET_OF(A,B) == TRUE and SUBSET_OF(B,C) == TRUE
      return TRUE  # establishes SUBSET_OF(A,C)
    return UNKNOWN

6. INFERENCE RULES
  R1 Reflexivity: Set(A) => SUBSET_OF(A,A).
  R2 Transitivity: A subset_of B and B subset_of C => A subset_of C.
  R3 Antisymmetry: A subset_of B and B subset_of A => A = B.
  R4 Membership propagation: x in A and A subset_of B => x in B.
  R5 Proper subset: A subset_of B and exists x in B\A => A proper_subset_of B.
  R6 Intersection: (A intersection B) subset_of A; (A intersection B) subset_of B.
  R7 Union: A subset_of (A union B); B subset_of (A union B).
  R8 Cardinality (finite): A subset_of B and finite(B) => |A| <= |B|.
  R9 Proper finite subset: A proper_subset_of B and finite(B) => |A| < |B|.
  R10 Empty set: empty_set subset_of A.

7. VALIDATION AND GUARDS
  - Never infer proper inclusion merely from unequal cardinalities without proven inclusion.
  - For infinite sets, a proper subset may have the same cardinality as its superset.
  - Under incomplete or open-world membership data, absence of an element is not proof of non-membership.
  - Distinguish object membership (x in A) from set inclusion (A subset_of B).
  - Check universe, equality semantics, and type compatibility before comparison.

8. CONFIDENCE
  CONFIDENCE:
    formal_proof: 1.0
    verified_finite_enumeration: 1.0
    partial_evidence: UNKNOWN
    heuristic_estimate: NON_DEDUCTIVE
  Confidence describes evidence strength, not the truth value of an unproven proposition.

9. SEMANTIC_EQUIVALENCE
  aliases:
    subset_of: ["is subset of", "is contained in", "set inclusion", "⊆"]
    proper_subset_of: ["strict subset", "proper inclusion", "⊊"]
  constraint: "⊂" is convention-dependent; resolve meaning before mapping.

10. PROVENANCE
  Record source, proof method, assumptions, set definitions, and validation timestamp for each asserted relation.

11. FLOW_HASH
  FLOW_HASH := SHA256(canonical_serialisation(version, typed_entities, relations, rules, constraints))
  Canonicalisation must preserve mathematical distinctions and normalise deterministic field ordering.

12. UPDATE_MODEL
  On changes to membership, set definition, universe, or proof evidence:
    invalidate affected derived subset assertions;
    recompute dependent relations by rule dependency order;
    preserve prior versions and provenance;
    regenerate FLOW_HASH.

13. AI_CONSUMPTION
  output:
    ontology: SubsetOntology
    assertions: typed triples with TRUE/FALSE/UNKNOWN
    proof_trace: ordered inference steps
    confidence: evidence-grounded value
    provenance: source and method
    semantic_equivalence: normalised relation identifiers
    flow_hash: deterministic digest
  safety: Never present unverified subset assertions as mathematical theorems.

END FLOW ALGEBRA