Skip to main content
MathOverflow

Return to Question

Post Timeline

Clarified my comment about Dedekind-finiteness
Source Link
Timothy Chow
Timothy Chow
  • 91.7k
  • 30
  • 408
  • 652

Some years ago, Kevin Buzzard wrote a blog post asking whether the trace of a linear map $\phi \colon V \to V$ on a vector space $V$ can be defined "without picking a basis." He had some very interesting insights, but stopped short of trying to formally define what it means for a proof to pick a basis (or not pick a basis).

Is it possible to formalize what it means for a proof to pick a basis?

My first thought was that "every vector space has a basis" is equivalent to the axiom of choice, so maybe one wants to work in ZF. If $V$ has no basis then a proof of a fact about $V$ certainly can't involve picking a basis for $V$. "Finite-dimensional" could maybe mean that $V$ has a Dedekind-finite spanning set but nonot necessarily a finite spanning set? But I don't think this works because I don't think the trace makes sense with this notion of "finite-dimensional."

So probably a more promising tack is Kevin's comment toward the end of his blog post, "This has something to do with constructivism." But I would like to see it spelled out more formally exactly what it would mean for a proof to pick (or not pick) a basis.

Some years ago, Kevin Buzzard wrote a blog post asking whether the trace of a linear map $\phi \colon V \to V$ on a vector space $V$ can be defined "without picking a basis." He had some very interesting insights, but stopped short of trying to formally define what it means for a proof to pick a basis (or not pick a basis).

Is it possible to formalize what it means for a proof to pick a basis?

My first thought was that "every vector space has a basis" is equivalent to the axiom of choice, so maybe one wants to work in ZF. If $V$ has no basis then a proof of a fact about $V$ certainly can't involve picking a basis for $V$. "Finite-dimensional" could maybe mean that $V$ has a Dedekind-finite spanning set but no finite spanning set? But I don't think this works because I don't think the trace makes sense.

So probably a more promising tack is Kevin's comment toward the end of his blog post, "This has something to do with constructivism." But I would like to see it spelled out more formally exactly what it would mean for a proof to pick (or not pick) a basis.

Some years ago, Kevin Buzzard wrote a blog post asking whether the trace of a linear map $\phi \colon V \to V$ on a vector space $V$ can be defined "without picking a basis." He had some very interesting insights, but stopped short of trying to formally define what it means for a proof to pick a basis (or not pick a basis).

Is it possible to formalize what it means for a proof to pick a basis?

My first thought was that "every vector space has a basis" is equivalent to the axiom of choice, so maybe one wants to work in ZF. If $V$ has no basis then a proof of a fact about $V$ certainly can't involve picking a basis for $V$. "Finite-dimensional" could maybe mean that $V$ has a Dedekind-finite spanning set but not necessarily a finite spanning set? But I don't think this works because I don't think the trace makes sense with this notion of "finite-dimensional."

So probably a more promising tack is Kevin's comment toward the end of his blog post, "This has something to do with constructivism." But I would like to see it spelled out more formally exactly what it would mean for a proof to pick (or not pick) a basis.

Became Hot Network Question
Source Link
Timothy Chow
Timothy Chow
  • 91.7k
  • 30
  • 408
  • 652

Precise meaning of "picking a basis"?

Some years ago, Kevin Buzzard wrote a blog post asking whether the trace of a linear map $\phi \colon V \to V$ on a vector space $V$ can be defined "without picking a basis." He had some very interesting insights, but stopped short of trying to formally define what it means for a proof to pick a basis (or not pick a basis).

Is it possible to formalize what it means for a proof to pick a basis?

My first thought was that "every vector space has a basis" is equivalent to the axiom of choice, so maybe one wants to work in ZF. If $V$ has no basis then a proof of a fact about $V$ certainly can't involve picking a basis for $V$. "Finite-dimensional" could maybe mean that $V$ has a Dedekind-finite spanning set but no finite spanning set? But I don't think this works because I don't think the trace makes sense.

So probably a more promising tack is Kevin's comment toward the end of his blog post, "This has something to do with constructivism." But I would like to see it spelled out more formally exactly what it would mean for a proof to pick (or not pick) a basis.