Inner product space with no ortho-normal basis without choice

TL;DR

This paper demonstrates within ZF set theory that there exists a well-defined inner product space lacking any orthonormal basis, challenging assumptions about the necessity of the Axiom of Choice.

Contribution

It provides a construction of an inner product space without an orthonormal basis without relying on the Axiom of Choice.

Findings

Existence of such inner product space in ZF

No orthonormal basis can be constructed for this space

The space is explicitly definable within ZF

Abstract

We prove in ZF that there is an inner product space, in fact, nicely definable with no orthonormal basis.