Frequentist definition of probability; does there exist a formal definition? Is there any formal (mathematical) definition of what frequentists understand under ''probability''.  I read that it is the relative frequency of occurrence ''in the long run'', but is there some formal way to define it ? Are there any known references where I can find that definition ?
EDIT: 
With frequentist (see comment by @whuber and my comments to the answer @Kodiologist and @Graeme Walsh below that answer) I mean those that ''believe'' that this long run relative frequency exists. Maybe this (partly) answers the question of @Tim also
 A: I don't think there is a mathematical definition, no. The difference between the various interpretations of probability is not a difference in how probability is mathematically defined. Probability could be mathematically defined this way: if $(Ω, Σ, μ)$ is a measure space with $μ(Ω) = 1$, then the probability of any event $S ∈ Σ$ is just $μ(S)$. I hope you agree that this definition is neutral to questions like whether we should interpret probabilities in a frequentist or Bayesian fashion.
A: TL;DR It doesn't seem like it is possible to define a frequentist definition of probability consistent with the Kolmogorov framework which isn't completely circular (i.e. in the sense of circular logic).
Not too long so I did read: I want to address what I see as some potential problems with the candidate frequentist definition of probability $$\underset{n \to \infty}{\lim} \frac{n_A}{n} $$ First, $n_A$ can only be reasonably be interpreted as a random variable, so the above expression is not precisely defined in a rigorous sense. We need to specify the mode of convergence for this random variable, be it almost surely, in probability, in distribution, in mean, or in mean squared.
But all of these notions of convergence require a measure on the probability space to be defined to be meaningful. The intuitive choice, of course, would be to pick convergence almost surely. This has the feature the limit needs to exist pointwise except on an event of measure zero. What constitutes a set of measure zero will coincide for any family of measures which are absolutely continuous with respect to each other -- this allows us to define a notion of almost sure convergence making the above limit rigorous while still being somewhat agnostic about what the underlying measure for the measurable space of events is (i.e. because it could be any measure absolutely continuous with respect to some chosen measure). This would prevent circularity in the definition which would arise from fixing a given measure in advance, since that measure could (and in the Kolmogorov framework usually is) defined to be the "probability".
However, if we are using almost sure convergence, then that means we are confining ourselves to the situation of the strong law of large numbers (henceforth SLLN). Let me state that theorem (as given on p. 133 of Chung) for the sake of reference here: 

Let $\{X_n\}$ be a sequence of independent, identically distributed random variables. Then we have $$ \mathbb{E}|X_1| < \infty \implies \frac{S_n}{n} \to \mathbb{E}(X_1)\quad  a.s.$$ $$\mathbb{E}|X_1| = \infty \implies \underset{n \to \infty}{\lim\sup}\frac{|S_n|}{n} = + \infty \quad a.s. $$ where $S_n:= X_1 + X_2 + \dots + X_n$.

So let's say we have a measurable space $(X, \mathscr{F})$ and we want to define the probability of some event $A \in \mathscr{F}$ with respect to some family of mutually absolutely continuous probability measures $\{\mu_i\}_{i \in I}$. Then by either the Kolmogorov Extension Theorem or Ionescu Tulcea Extension Theorem (I think both work), we can construct a family of product spaces $\{(\prod_{j=1}^{\infty} X_j)_i\}_{i \in I}$, one for each $\mu_i$. (Note that the existence of infinite product spaces which is a conclusion of Kolmogorov's theorem requires the measure of each space to be $1$, hence why I am now restricting to probability, instead of arbitrary, measures). Then define $\mathbb{1}_{A_j}$ to be the indicator random variable, i.e. which equals $1$ if $A$ occurs in the $j$th copy and $0$ if it does not, in other words $$n_A = \mathbb{1}_{A_1} + \mathbb{1}_{A_2} + \dots + \mathbb{1}_{A_n}.$$ Then clearly $0 \le \mathbb{E}_i \mathbb{1}_{A_j} \le 1 $ (where $\mathbb{E}_i$ denotes expectation with respect to $\mu_i$), so the strong law of large numbers will in fact apply to $(\prod_{j=1}^{\infty} X_j)_i$ (because by construction the $\mathbb{1}_{A_j}$ are identically and independently distributed - note that being independently distributed means that the measure of the product space is multiplicative with respect to the coordinate measures) so we get that $$\frac{n_A}{n} \to \mathbb{E}_i \mathbb{1}_{A_1} \quad a.s. $$ and thus our definition for the probability of $A$ with respect to $\mu_i$ should naturally be $\mathbb{E}_1 \mathbb{1}_{A}$.
I just realized however that even though the sequence of random variables $\frac{n_A}{n}$ will converge almost surely with respect to $\mu_{i_1}$ if and only if it converges almost surely with respect to $\mu_{i_2}$, (where $i_1, i_2 \in I$) that doesn't necessarily mean that it will converge to the same value; in fact, the SLLN guarantees that it won't unless $\mathbb{E}_{i_1} \mathbb{1}_A = \mathbb{E}_{i_2} \mathbb{1}_A$ which is not true generically.
If $\mu$ is somehow "canonical enough", say like the uniform distribution for a finite set, then maybe this works out nicely, but doesn't really give any new insights. In particular, for the uniform distribution, $\mathbb{E}\mathbb{1}_A = \frac{|A|}{|X|}$, i.e. the probability of $A$ is just the proportion of points or elementary events in $X$ which belong to $A$, which again seems somewhat circular to me. For a continuous random variable I don't see how we could ever agree on a "canonical" choice of $\mu$.
I.e. it seems like it makes sense to define the frequency of an event as the probability of the event, but it does not seem like it makes sense to define the probability of the event to be the frequency (at least without being circular). This is especially problematic, since in real life we don't actually know what the probability is; we have to estimate it.
Also note that this definition of frequency for a subset of a measurable space depends on the chosen measure being a probability space; for instance, there is no product measure for countably many copies of $\mathbb{R}$ endowed with the Lebesgue measure, since $\mu(\mathbb{R})=\infty$. Likewise, the measure of $\prod_{j=1}^n X$ using the canonical product measure is $(\mu(X))^n$, which either blows up to infinity if $\mu(X) >1$ or goes to zero if $\mu(X) <1$, i.e. Kolmogorov's and Tulcea's extension theorems are very special results peculiar to probability measures.
