Let me try to situate your definition in context.

A **closure operator** on a set $X$ is a function $\text{cl}\colon \mathcal{P}(X)\to \mathcal{P}(X)$ such that for all $A,B\subseteq X$, we have:

- $A\subseteq \text{cl}(A)$.
- If $A\subseteq B$, then $\text{cl}(A) \subseteq \text{cl}(B)$
- $\text{cl}(\text{cl}(A)) = \text{cl}(A)$.

We say the closure operator satisfies **exchange** if additionally for all $A\subseteq X$ and $a,b\in X$:

- If $b\in \text{cl}(A\cup \{a\})$ but $b\notin \text{cl}(A)$, then $a\in \text{cl}(A\cup \{b\})$.

When $X$ is finite, a pair $(X,\text{cl})$ such that $\text{cl}$ is a closure operator on $X$ satisfying exchange is called a (finite) **matroid** [this is one of many equivalent definitions of this concept].

Now we can clearly make the same definition when $X$ is infinite, but it turns out not to have some of the nice properties of matroids. For example, we can no longer prove that every closed set has a basis (a maximal independent subset). So usually people *strengthen* this definition by adding extra axioms: it's common to look at **finitary matroids** (also called a **pregeometries**, especially by model theorists) or **B-matroids**. See Wikipedia.

Your definition is a slight *weakening* of the notion of a closure operator satisfying exchange, which becomes equivalent to this notion if we add an assumption about existence of bases for closed sets.

First let's observe that what you call a structure is equivalent to a closure operator.

In one direction, given a structure $S = (X,\mathcal{T})$, we can define $\text{cl}(A) = \langle A\rangle_S$ as in your question, and this clearly satisfies axioms 1, 2, and 3.

Conversely, given a closure operator $\text{cl}$ on $X$, we can take $\mathcal{T}$ to be the set of closed subsets of $X$, i.e. $\mathcal{T} = \{A\subseteq X\mid \text{cl}(A) = A\}$. Then $\mathcal{T}$ is stable under arbitrary intersections, since if $A_i\in \mathcal{T}$ for all $i\in I$, then $\bigcap_{i\in I} A_i \subseteq A_i$ for all $i\in I$, so $$\text{cl}(\bigcap_{i\in I} A_i)\subseteq \text{cl}(A_i) = A_i$$ for all $i\in I$, and hence $$\text{cl}(\bigcap_{i\in I} A_i) \subseteq \bigcap_{i\in I} A_i.$$ In the other direction, we have $$\bigcap_{i\in I} A_i \subseteq \text{cl}(\bigcap_{i\in I} A_i),$$ so these sets are equal, and $\bigcap_{i\in I} A_i\in \mathcal{T}$.

Now if $\text{cl}$ satisfies exchange, then the structure $(X,\mathcal{T})$ has a dimension in your sense.

Assume $U\subseteq X$ is free and $v\notin \text{cl}(U)$. Assume for contradiction that $U\cup \{v\}$ is not free. Then since $v\notin \text{cl}(U)$, we must have some $u\in U$ such that $u\in \text{cl}(U'\cup \{v\})$, where $U' = U\setminus \{u\}$. But since $U$ is free, $u\notin \text{cl}(U')$. So by exchange, $v\in \text{cl}(U'\cup \{u\}) = \text{cl}(U)$, contradiction.

We can prove the converse, if we additionally assume existence of bases. Let's say that a structure $S = (X,\mathcal{T})$ **has bases** if for every set $A\subseteq X$, there is a free set $A'\subseteq X$ such that $\text{cl}(A') = \text{cl}(A)$.

Now suppose $S = (X,\mathcal{T})$ is a structure with a dimension and bases. To prove exchange, suppose $b\in \text{cl}(A\cup \{a\})$ but $b\notin \text{cl}(A)$.

Let $A'$ be a free set such that $\text{cl}(A') = \text{cl}(A)$. Then $b\notin \text{cl}(A')$, so since $S$ has a dimension, $A'\cup \{b\}$ is free. Now $(A'\cup \{b\})\cup \{a\}$ is not free (since $b\in \text{cl}(A'\cup \{a\}) = \text{cl}(A\cup \{a\})$), so since $S$ has a dimension, $a\in \text{cl}(A'\cup \{b\}) = \text{cl}(A\cup \{b\})$.

Here is a counterexample showing that not every structure with a dimension has basis, and the associated closure operator does not satisfy exchange in general.

Let $X = A \cup \{a,b\}$, where $A$ is infinite and $a,b\notin A$. Define a structure by letting $\mathcal{T} = \mathcal{P}_{\text{fin}}(X) \cup \{A\} \cup \{A\cup \{b\}\}\cup \{X\}$, where $\mathcal{P}_{\text{fin}}(X)$ is the set of all finite subsets of $X$. This family is evidently stable under arbitrary intersections.

The corresponding closure operator has $\text{cl}(B) = B$ if $B$ is finite, and $\text{cl}(B)$ is the least of $A$, $A\cup \{b\}$ and $X = A\cup \{a,b\}$ containing $B$ if $B$ is infinite.

A subset $B\subseteq X$ if free if and only if it is finite. Indeed, any infinite subset $B\subseteq X$ contains infinitely many elements of $A$, and for any $z\in B\cap A$, we have $z\in \text{cl}(B\setminus \{z\})$, since $A\subseteq \text{cl}(B\setminus \{z\})$.

So this structure has a dimension, since for any free $U$ and any $v\notin \text{cl}(U)$, $U\cup \{v\}$ is finite, hence free.

But the closed set $A$ has no basis (since any free set has finite closure). And exchange fails: we have $b\in \text{cl}(A\cup \{a\})$ and $b\notin \text{cl}(A)$, but $a\notin \text{cl}(A\cup \{b\}$.

Your definition of "has a dimension" *is* enough to get bases for closures of finite sets $A$ (just build up a free set by adding elements of $A$ not in the closure of what we've built so far one by one, until the closure of our basis contains $A$ and hence is equal to the closure of $A$). So it's enough to get exchange when the set $A$ appearing in the definition of exchange is finite. The problem arises when you try to "take limits": the union of an increasing sequence of free sets is not necessarily free.

This is one motivation for the definition of finitary matroid. If we assume that $\text{cl}$ is finitary (this is equivalent to assuming that the family $\mathcal{T}$ is stable under *directed unions*), then "has a dimension" will imply the existence of bases and exchange.

That is, a structure $(X,\mathcal{T})$ with a dimension such that $\mathcal{T}$ is stable under directed unions, is essentially the same thing as a finitary matroid.

Conclusion: I doubt that your exact definition has been studied before. Usually people are interested in strengthenings of the notion of closure operator satisfying exchange. Your notion is a weakening, and as the counterexample above shows, without some extra hypotheses, the "has a dimension" assumption can trivialize when looking at closures of infinite sets, simply because not enough free sets exist.

By the last remark above, the finite dimensional sets in your structures with dimension will behave just like they do in finitary matroids. Thus you'll be able to prove things like the theorem in your question. But without any additional assumptions on how closures of infinite sets behave, I suspect you'll have a hard time proving anything interesting about the infinite dimensional sets.

**Edit:** Your Theorem 2 is not correct.

For a counterexample, let $X = \mathbb{R}$, and let $\mathcal{T}$ be the set of all $A\subseteq \mathbb{R}$ such that $A = \mathbb{R}$ or $A\cap \mathbb{N}$ is finite. This family is stable under arbitrary intersections, and the structure $(\mathbb{R}, \mathcal{T})$ has a dimension, since $U\subseteq \mathbb{R}$ is free if and only if $U\cap \mathbb{N}$ is finite, so the union of any free set with any singleton is free.

Now let $V = \mathbb{R}\setminus \mathbb{N}$. We have $\langle \mathbb{N}\rangle = \mathbb{R}$, so $V\subseteq \langle \mathbb{N}\rangle$, and $\text{card}(\mathbb{N})< \text{card}(V)$, but $V$ is free, since $V\cap \mathbb{N} = \emptyset$.

If you were to explain your supposed proof of Theorem 2, I might be able to find where the proof goes wrong and suggest a strenthening of your axioms that makes it true.