Independent/Easy fraction of sentences over PA Let $S(n)$ be the set of all sentences over PA of length at most $n$ (counting the quantifier symbols, boolean connectives, arithmetic operations and constants, and counting each variable as length $1$).
Let $I(n) = \{ φ : φ \in S(n) \land \text{$φ$ is independent of PA} \}$.
Let $E(n) = \{ φ : φ \in S(n) \land \text{PA$^-$ proves or disproves $φ$} \}$.   [PA$^-$ is defined here.]
$
\def\lfrac#1#2{{\large\frac{#1}{#2}}}
$

I think $\lfrac{\#(I(n))}{\#(S(n))} \to 0$ as $n \to \infty$, contrary to the conjecture at the end of this paper.

My intuition is that it is relatively easy for a random sentence to be provable or disprovable just because of some provable example or counter-example. But I am not sure how to go about proving this. Is there any simple trick I am missing?

Also, I suspect $\lfrac{\#(I(n))+\#(E(n))}{\#(S(n))} \to 1$ as $n \to \infty$, but I am unsure.

This is actually an attempt to capture the idea that most statements that are not decided by PA$^-$ cannot be decided by PA. In intuitive terms I am trying to say that most statements are either easy to prove or disprove or independent of PA. Is any such thing true?
I posted this question on Math SE about a year ago but did not get any response, so I hope someone here can help. I would be quite surprised if my first conjecture is false! But neither conjecture seem to yield to structural induction or padding tricks.
 A: The question of limiting fractions is obviously sensitive to the presentation and ordering of sentences.  Meanwhile we can get some results for sentences of the form $$Q\vec{x}\ p(\vec{x})=0$$ where $Q\vec{x}$ is a sequence of quantifiers over variables in $\mathbf{N}$, and $p$ is a polynomial with coefficients in $\mathbf{Z}$, in which every variable in $\vec{x}$ appears non-trivially.  We can regard these as abbreviations of sentences of the form $Q\vec{x}\ p(\vec{x})=q(\vec{x})$, where $p$ and $q$ have coefficients in $\mathbf{N}$.
Since every sentence of first-order arithmetic is equivalent under $PA^-$ to such a sentence, this is a reasonable set of sentences to consider.  We can order the sentences to put the low-coefficient, low-degree, low-variable polynomials first.  We find the following.


*

*When $Q$ is $\emptyset$:  $PA^-$ settles all sentences of the form $p(1)=0$.

*When $Q$ is $\forall x$:  $PA^-$ settles all sentences of the form $\forall x \ p(x)=0$, and proves them false.

*When $Q$ is $\exists x$:  $PA^-$ settles all sentences of the form $\exists x \ p(x)=0$.  Given $p$, we can find a bound on the roots, prove in $PA^-$ that $p$ is positive for $x$ above that bound, and test in $PA^-$ whether any there are any roots with $x$ below that bound.

*When $Q$ is $\forall x \forall y$:  $PA^-$ settles all sentences of the form $\forall x\forall y \ p(x,y)=0$, and proves them false.

*When $Q$ is $\exists x \forall y$:  $PA^-$ settles all sentences of the form $\exists x\forall y \ p(x,y)=0$, mostly proving them false.  Either we can instantiate an $x$, and $PA^-$ proves the claim $\forall y$; or we can choose a number of $y$'s depending on the degree of $p$ and $PA^-$ proves that $p(x,0),\ p(x,1),\ldots p(x,d)$ have no common root.
After this things get more interesting:


*

*When $Q$ is $\forall x \exists y$: $PA^-$ cannot settle all of these, but $PA$ can.  For instance, $PA$ proves $\forall x \exists y\ (x-2y)(x-2y-1)=0$.  However, this is false in the model of $PA^-$ whose domain is the eventually non-negative polynomials in $\mathbf{Z}[t]$, so it is independent of $PA^-$.

*When $Q$ is $\exists x \exists y$: $PA^-$ cannot settle all of these, and it's open whether $PA$ can.  For instance, $PA$ disproves $\exists x \exists y\ (x+1)^2-2y^2=0$.  However, this is true in the model of $PA^-$ whose domain is the eventually non-negative polynomials in $\mathbf{Z}[\sqrt{2}][t]$ with integer constant terms, so it is independent of $PA^-$.  An effective version of Falting's theorem would presumably show that $PA$ settles all of these sentences.
It seems to me that as the degrees and quantifiers increase, a positive fraction of these sentences will be settled by $PA$ but not by $PA^-$, which is contrary to the second conjecture.  In any case, this seems to be one interesting way to focus the question.
