Diffusion afp-devel d1cdfc97ad72

Refining three sessions.
d1cdfc97ad72
Actions

Tags

None

Subscribers

None

Description

Refining three sessions.

Delta_System_Lemma: Moving results out of the scope of AC.
Transitive_Models: General locale re-engineering.
Independence_CH: specifying finite set of axioms required for forcing CH and ¬CH.

Details

Provenance

Authored on

Parents

rAFP206c4f90ab7c: Tuned.

Branches

Unknown

Tags

Unknown

Event Timeline

sterraf committed rAFPd1cdfc97ad72: Refining three sessions..Jul 26 2022, 1:09 AM

Changes (64)

Path

Size

thys/

Delta_System_Lemma/

Cardinal_Library.thy

Cohen_Posets.thy

Delta_System.thy

document/

Independence_CH/

Absolute_Versions.thy

Cardinal_Preservation.thy

Choice_Axiom.thy

Cohen_Posets_Relative.thy

Definitions_Main.thy

Demonstrations.thy

Fm_Definitions.thy

Forces_Definition.thy

Forcing_Data.thy

Forcing_Main.thy

Forcing_Notions.thy

Forcing_Theorems.thy

Infinity_Axiom.thy

Internal_ZFC_Axioms.thy

Kappa_Closed_Notions.thy

Ordinals_In_MG.thy

Pairing_Axiom.thy

Powerset_Axiom.thy

Proper_Extension.thy

Replacement_Axiom.thy

Replacement_Instances.thy

Separation_Axiom.thy

Separation_Instances.thy

Separation_Rename.thy

Succession_Poset.thy

Union_Axiom.thy

ZF_Trans_Interpretations.thy

Transitive_Models/

Aleph_Relative.thy

CardinalArith_Relative.thy

Cardinal_AC_Relative.thy

Cardinal_Library_Relative.thy

Cardinal_Relative.thy

Delta_System_Relative.thy

Discipline_Base.thy

Discipline_Cardinal.thy

Discipline_Function.thy

FiniteFun_Relative.thy

Internalizations.thy

Lambda_Replacement.thy

Nat_Miscellanea.thy

Partial_Functions_Relative.thy

Pointed_DC_Relative.thy

Recursion_Thms.thy

Renaming_Auto.thy

Replacement_Lepoll.thy

Univ_Relative.thy

ZF_Library_Relative.thy

ZF_Miscellanea.thy

document/

rAFPd1cdfc97ad72

thys/Delta_System_Lemma/Cardinal_Library.thy

Loading...

thys/Delta_System_Lemma/Cofinality.thy

Loading...

thys/Delta_System_Lemma/Cohen_Posets.thy

Loading...

thys/Delta_System_Lemma/Delta_System.thy

Loading...

thys/Delta_System_Lemma/Konig.thy

Loading...

thys/Delta_System_Lemma/ZF_Library.thy

Loading...

thys/Delta_System_Lemma/document/root.bib

Loading...

thys/Delta_System_Lemma/document/root.tex

Loading...

thys/Independence_CH/Absolute_Versions.thy

Loading...

thys/Independence_CH/CH.thy

Loading...

thys/Independence_CH/Cardinal_Preservation.thy

Loading...

thys/Independence_CH/Choice_Axiom.thy

Loading...

thys/Independence_CH/Cohen_Posets_Relative.thy

Loading...

thys/Independence_CH/Definitions_Main.thy

Loading...

thys/Independence_CH/Demonstrations.thy

Loading...

thys/Independence_CH/Edrel.thy

Loading...

thys/Independence_CH/Fm_Definitions.thy

Loading...

thys/Independence_CH/Forces_Definition.thy

Loading...

thys/Independence_CH/Forcing_Data.thy

Loading...

thys/Independence_CH/Forcing_Main.thy

Loading...

thys/Independence_CH/Forcing_Notions.thy

Loading...

thys/Independence_CH/Forcing_Theorems.thy

Loading...

thys/Independence_CH/Infinity_Axiom.thy

Loading...

thys/Independence_CH/Interface.thy

Loading...

thys/Independence_CH/Internal_ZFC_Axioms.thy

Loading...

thys/Independence_CH/Kappa_Closed_Notions.thy

Loading...

thys/Independence_CH/Names.thy

Loading...

thys/Independence_CH/Not_CH.thy

Loading...

thys/Independence_CH/Ordinals_In_MG.thy

Loading...

thys/Independence_CH/Pairing_Axiom.thy

Loading...

thys/Independence_CH/Powerset_Axiom.thy

Loading...

thys/Independence_CH/Proper_Extension.thy

Loading...

thys/Independence_CH/Replacement_Axiom.thy

Loading...

thys/Independence_CH/Replacement_Instances.thy

Loading...

thys/Independence_CH/Separation_Axiom.thy

Loading...

thys/Independence_CH/Separation_Instances.thy

Loading...

thys/Independence_CH/Separation_Rename.thy

Loading...

thys/Independence_CH/Succession_Poset.thy

Loading...

thys/Independence_CH/Union_Axiom.thy

Loading...

thys/Independence_CH/ZF_Trans_Interpretations.thy

Loading...

thys/Transitive_Models/Aleph_Relative.thy

Loading...

thys/Transitive_Models/Arities.thy

Loading...

thys/Transitive_Models/CardinalArith_Relative.thy

Loading...

thys/Transitive_Models/Cardinal_AC_Relative.thy

Loading...

thys/Transitive_Models/Cardinal_Library_Relative.thy

Loading...

thys/Transitive_Models/Cardinal_Relative.thy

Loading...

thys/Transitive_Models/Delta_System_Relative.thy

Loading...

thys/Transitive_Models/Discipline_Base.thy

Loading...

thys/Transitive_Models/Discipline_Cardinal.thy

Loading...

thys/Transitive_Models/Discipline_Function.thy

Loading...

thys/Transitive_Models/FiniteFun_Relative.thy

Loading...

thys/Transitive_Models/Internalizations.thy

Loading...

thys/Transitive_Models/Lambda_Replacement.thy

Loading...

thys/Transitive_Models/Nat_Miscellanea.thy

Loading...

thys/Transitive_Models/Partial_Functions_Relative.thy

Loading...

thys/Transitive_Models/Pointed_DC_Relative.thy

Loading...

thys/Transitive_Models/Recursion_Thms.thy

Loading...

thys/Transitive_Models/Renaming.thy

Loading...

thys/Transitive_Models/Renaming_Auto.thy

Loading...

thys/Transitive_Models/Replacement_Lepoll.thy

Loading...

thys/Transitive_Models/Univ_Relative.thy

Loading...

thys/Transitive_Models/ZF_Library_Relative.thy

Loading...

thys/Transitive_Models/ZF_Miscellanea.thy

Loading...

thys/Transitive_Models/document/root.tex

Loading...