Session Forcing

Theories

• Forcing_Notions
• Pointed_DC
• Rasiowa_Sikorski
• Nat_Miscellanea
• ZF_Miscellanea
• Recursion_Thms
• Utils
  • File ‹Utils.ml›
• Synthetic_Definition
• Internalizations
• Least
• Higher_Order_Constructs
• Relativization
  • File ‹Relativization_Database.ml›
• Discipline_Base
• Arities
• Discipline_Function
• Relative_Univ
• Renaming
• Renaming_Auto
  • File ‹Renaming_ML.ml›
• Interface
• Forcing_Data
• Names
• FrecR
• FrecR_Arities
• Discipline_Cardinal
• Lambda_Replacement
• Cardinal_Relative
• CardinalArith_Relative
• Aleph_Relative
• Cohen_Posets
• FiniteFun_Relative
• Cardinal_AC_Relative
• ZF_Library_Relative
• Replacement_Lepoll
• Separation_Instances
• Replacement_Instances
• Proper_Extension
• Succession_Poset
• Internal_ZFC_Axioms
• Forces_Definition
• Forcing_Theorems
• Separation_Rename
• Separation_Axiom
• Pairing_Axiom
• Union_Axiom
• Powerset_Axiom
• Extensionality_Axiom
• Foundation_Axiom
• Replacement_Axiom
• Infinity_Axiom
• Choice_Axiom
• Ordinals_In_MG
• Forcing_Main
• Cardinal_Library_Relative
• Delta_System_Relative
• Cohen_Posets_Relative
• ZF_Trans_Interpretations
• Cardinal_Preservation
• Not_CH
• Absolute_Versions
• Definitions_Main