Is there a rigorous definition of a Young tableau? In all combinatorics and algebra texts that I have seen so far, the notion of a "Young tableau" is defined in a somewhat informal fashion. The most common approach is stating that a Young tableaux is a "filling" of a Young diagram (or Ferrers diagram, in some texts) with symbols from some (usually totally ordered) alphabet. 
In the specific case of standard Young tableaux, the alphabet is the set of numbers from $1$ to $n$, and the entries should increase along the lines and columns.
My question is: is there a way of making this definition rigorous? Specifically, I have a problem with the word "filling" in the above definition. What exactly does that mean, in a formalized way?
(I do realize that a rigorous definition os a Young tableau is not really necessary to work with that notion; I really have no problem following and accepting most standard proofs of theorems involving Young tableaux. I was just curious to know if there is such a formalization.)
 A: Frankly, it's as formal as it needs to be. But if you're just curious for curiosity sake, it is not too difficult to create an ad hoc formal definition to capture our conceptual understanding.
For naturals $n\ge1$, use the standard notation $[n]=\{1,\cdots,n\}$. Encode a Ferrers diagram by an integer partition $(\lambda_1,\cdots,\lambda_k)$ (i.e. a nonincreasing sequence of positive integers). Define a semi-standard tableau to be a function $f$ from $\bigsqcup[\lambda_i]:=\bigcup\big(\{i\}\times[\lambda_i]\big)$ into an ordered set $A$ (where $A$ is usually something like $[m]$ for some fixed $m$, or $[n]$ with $n:=\lambda_1+\cdots+\lambda_k$, or  $\bf N$) such that 


*

*Strictly increasing columns: $i<j, c\le \lambda_j\implies f(i,c)<f(j,c)$

*Weakly increasing rows: $a\le b\le \lambda_i\implies f(i,a)\le f(i,b)$


This is implicitly the definition used in e.g. the article The Littlewood-Richardson rule, and related combinatorics.
A: This is a very good question, and I strongly object to the statement that the usual account is "as formal as it needs to be." I've never seen Young diagrams formalized either, but here's what I came up with after pondering it for a couple of hours. Let me know if there's any problems or mistakes.

Definition 0. Given a monoid $M$ and a set $S$, a partial action of $M$ on $S$ is a function $f : M \rightarrow \mathrm{Par}(S,S)$ satisfying: $$f(1_M) = \mathrm{id}_S, \qquad f(ab) \geq f(a)f(b).$$
In other words, its a partial function $M \times S \rightarrow M$ subject to the following axioms: $$1_M s = s, \qquad (ab)s \geq a(bs)$$
(I write $\mathrm{LHS} \geq \mathrm{RHS}$ to mean that the LHS is denoting if the RHS is, in which case they're equal.)
Definition 1. A board consists of a set $S$ together with a partial action of $(\mathbb{Z}^2,+,0)$ on $S$. We'll tend to write this $a,x \mapsto a+x$.
Definition 2. Let $P$ denote a poset. Then a $P$-valued Young board is a board $B$ together with a function $f : B \rightarrow P$ satisfying the following:

*

*For all $a \in \mathbb{Z}_{\geq 0}$ and all $x \in B$, if $ae_0+x$ exists, then $f(ae_0+x) \geq f(x)$, where $e_0 = (1,0) \in \mathbb{Z}^2$.


*For all $a \in \mathbb{Z}_{> 0}$ and all $x \in B$, if $ae_1+x$ exists, then $f(ae_1+x) > f(x)$, where $e_1 = (0,1) \in \mathbb{Z}^2$.

An easy way of getting boards is to note that every subset of $\mathbb{Z}^2$ can be viewed as a board in the obvious way. So define:

Definition 3. Consider a pair $(n,x)$, where $n \in \mathbb{N}$ and $x$ is an $n$-long sequence of natural numbers. Then $$\mathrm{Diagram}(n,x) = \{(a,b) \in \mathbb{N}^2 : a<n \wedge b<x_a\},$$ viewed as board by inheriting the structure from $\mathbb{Z}^2.$
Definition 4. Let $B$ denote a board. Then $B$ has the Young diagram property iff there exists a pair $(n,x)$ such that $n \in \mathbb{N}$, $x$ is a decreasing $n$-long sequence of positive natural numbers, and $B \cong \mathrm{Diagram}(n,x)$ as boards.
Definition 5. Let $P$ denote a poset. Then a $P$-valued Young tableau is a $P$-valued Young board that has the Young diagram property.

