cp's OEIS Frontend

The total number of unique logical sentences of n quantified variables in prenex normal form (PNF) with a fixed proposition is given by A000629. Essentially, a logical sentence is in PNF iff it is a string of quantifiers followed by a proposition.

Note that for an arbitrary proposition, the only two possible implications are: firstly, "for all x_1" -> "exists x_1", and, secondly, "exists x_1 forall x_2" -> "forall x_2 exists x_1". The sequence is formed by counting all the number of implications between all valid PNFs for a fixed proposition.

For example, a(1)=1, because "forall x P(x)" and "exists x P(x)" both imply themselves, and the former implies the latter. However, the latter does not imply the former.