A Formal Axiomatization of Computation

Abstract

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}\ne \mathrm{NP}$. In other words, regarding "effective computability" in Brouwer intuitionism viewpoint, we show $\mathrm{P}\ne \mathrm{NP}$.

13 page. arXiv admin note: substantial text overlap with arXiv:1906.09873, arXiv:1205.5994