Some intuitionist principles in the free topos

Trevor Wares
Brouwer's principle/theorem states that all total functions R→R are continuous. Obviously not classically true this result was a theorem of Brouwer in his intuitionistic setting. The formalization(s) of intuitionistic logic provides us with systems of logic in which to ask is this principle provable? In a higher order setting (e.g. higher order type theory) one has two ways of expressing this principle. First is simply the statement ⊢∀f&parl0;f:R&rarrr; R⇒'' fiscontinuous'' &parr0; Second is as a...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.