Documentation

LeanPool.NFWeakPartition.NFStandard.NotWPP

NF weak partition development: NFStandard.NotWPP.

source
theorem NFChoice.Foundation.NFStandard.hailperin_proves_not_WPP :
HailperinNF.sprovable (Fol.bdNot WPP)

The repository's finite presentation proves the negation of WPP.

source
theorem NFChoice.Foundation.NFStandard.NF_proves_not_WPP :
NF.sprovable (Fol.bdNot WPP)

Standard NF proves the negation of WPP, by full finite-basis equivalence.