It is a nontrivial fact that half the primes are $\equiv 1 \pmod{4}$ and the other half are $\equiv 3\pmod{4}$. The Chebyshev bias suggests, however, that the latter class of primes is winning the race more often. Under a logarithmic measure, Rubinstein and Sarnak showed in 1994 that about 99.59% of the time, the latter class is beating the former class.
With this motivating example in mind, let us switch gears to the subject of my question. Consider the standard model of the natural numbers. It seems intuitively obvious that, when working in a fixed first order formal language containing negation, then half the statements about the natural numbers are true and half are false. The idea is that if $\varphi$ is a statement with an even number of negations at the beginning (including zero negations), then $\neg \varphi$ will be a corresponding formula having the opposite truth value.
There are some obvious issues with this argument. First, the density could potentially depend highly on the numbering we give to formulas, especially to how our numbering of formulas involves the negation symbol. Second, we have no algorithmic way of deciding whether a statement is true or false.
If we number formulas in a "natural" way (such as one commonly taught in a first course in logic), does the density exist? If not, would a modified measure (like the logarithmic measure used for primes) fix the problem? If there is a density under some measure, is there a bias in the race between true and false formulas? What if we restrict to provable vs. refutable statements (say, using PA, or Robinson arithmetic)?
Edited to add: To make things concrete, let's use the following scheme (somewhat following a suggestion of Joel David Hamkins). Work in the standard language of arithmetic, $+,\cdot,0,1,<$. Also, allow all logical connectives (not just the standard Boolean ones), and write formulas using reverse Polish notation, to remove parentheses. Also suppose we have an infinite list of variables, all of length 1. Up to logical equivalence, there are only finitely many statements of length $n$. As $n$ increases, is it likely (in some sense similar to the Chebyshev bias) that more sentences of length $\leq n$ are true than false in the standard model?
Second edit: It may be important to first answer the following computability question. Fix some length function on formulas, that counts symbols. (This length could either take into account, or ignore, the index on a variable, as one desires.) Let $P(n)$ be the assertion that if we choose a statement at random, from among the sentences of length $\leq n$, that involves only the variables $v_1,v_2,\ldots, v_n$, then it is more likely true than false.
Is there a way to compute the truth value of $P(n)$, for each $n\geq 1$? Or do the undecidable statements overwhelm any ability to determine the truth value of $P(n)$ as $n$ increases?
