...
 
Commits (2)
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg/nat ❚
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import sets http://mathhub.info/MitM/Foundation/sets ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory Intersection : fnd:?Logic =
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_zfc ❚
import sets http://mathhub.info/MitM/Foundation/sets ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory NaturalNumbers : fnd:?Logic =
include sets:?ZFC ❙
nat : set ❙
\ No newline at end of file
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_zfc ❚
import sets http://mathhub.info/MitM/Foundation/sets ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory russelsParadox : fnd:?Logic =
include sets:?ZFC ❙
russelsParadox : ⊦ ¬ ∃ [S] ⟪ S | [x] ⟫ ❙