OAI/ModelTheory/Categoricity/Model.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Set-sized relational structures and categoricity thresholds

Carriers are arbitrary ZFSets, rather than subsets of one fixed set. Strong substructures are induced relational substructures. The abstract elementary class axioms include isomorphism invariance, coherence, nonzero ordinal unions and smoothness over a common upper bound. The Löwenheim–Skolem bound includes the cardinality of the language, and categoricity includes existence.

The Hanf index is the initial ordinal of a cardinal successor. The lower endpoint of the categoricity tail is included.

  1. structure OAI.CHObstruction.RelModel line 26

    Also declared: ComparatorChallenges/CHObstruction.lean:13 (same declaration text).

  2. structure OAI.CHObstruction.RelModel.IsSubstructure line 34

    Also declared: ComparatorChallenges/CHObstruction.lean:21 (same declaration text).

  3. structure OAI.CHObstruction.RelModel.Iso line 39

    Also declared: ComparatorChallenges/CHObstruction.lean:26 (same declaration text).

  4. def OAI.CHObstruction.RelModel.IsUnion line 44

    Also declared: ComparatorChallenges/CHObstruction.lean:31 (same declaration text).

  5. structure OAI.CHObstruction.ClassData line 50

    Also declared: ComparatorChallenges/CHObstruction.lean:37 (same declaration text).

  6. def OAI.CHObstruction.ClassData.LSBound line 58

    Also declared: ComparatorChallenges/CHObstruction.lean:45 (same declaration text).

  7. def OAI.CHObstruction.ClassData.HasLSNumber line 63

    Also declared: ComparatorChallenges/CHObstruction.lean:50 (same declaration text).

  8. structure OAI.CHObstruction.ClassData.IsAEC line 66

    Also declared: ComparatorChallenges/CHObstruction.lean:53 (same declaration text).

  9. def OAI.CHObstruction.ClassData.Categorical line 90

    Also declared: ComparatorChallenges/CHObstruction.lean:77 (same declaration text).

  10. def OAI.CHObstruction.ClassData.TwoModels line 95

    Also declared: ComparatorChallenges/CHObstruction.lean:82 (same declaration text).

  11. def OAI.CHObstruction.CH line 101

    Also declared: ComparatorChallenges/CHObstruction.lean:88 (same declaration text).

  12. def OAI.CHObstruction.hanf line 103

    Also declared: ComparatorChallenges/CHObstruction.lean:90 (same declaration text).

  13. def OAI.CHObstruction.endpoint line 105

    Also declared: ComparatorChallenges/CHObstruction.lean:92 (same declaration text).

  14. def OAI.CHObstruction.tailThreshold line 107

    Also declared: ComparatorChallenges/CHObstruction.lean:94 (same declaration text).