  We introduce an axiomatization for the notion of computation. Based on the
idea of Brouwer choice sequences, we construct a model, denoted by $E$, which
satisfies our axioms and $E \models \mathrm{ P \neq NP}$. In other words,
regarding "effective computability" in Brouwer intuitionism viewpoint, we show
$\mathrm{ P \neq NP}$.
