cp's OEIS Frontend

This is a front-end for the Online Encyclopedia of Integer Sequences, made by Christian Perfect. The idea is to provide OEIS entries in non-ancient HTML, and then to think about how they're presented visually. The source code is on GitHub.

A381324 Number of true implications over all possible pairs of unique logical sentences of n quantified variables in prenex normal form with a fixed proposition.

This page as a plain text file.
%I A381324 #31 May 18 2025 22:24:24
%S A381324 3,17,177,3029,76713,2677637,122836857
%N A381324 Number of true implications over all possible pairs of unique logical sentences of n quantified variables in prenex normal form with a fixed proposition.
%C A381324 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.
%C A381324 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.
%H A381324 Adam Wang, <a href="https://arxiv.org/abs/2504.15294">Determining Implication of Fixed Matrix Prenex Normal Forms Can Be Decided in Linear Time</a>, arXiv:2504.15294 [cs.DS], 2025.
%H A381324 Wikipedia, <a href="https://en.wikipedia.org/wiki/Prenex_normal_form">Prenex Normal Form</a>
%F A381324 a(n) = A000629(n)^2 - A381325(n).
%e A381324 a(1)=3, 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.
%Y A381324 Cf. A000629, A381325.
%K A381324 nonn,more
%O A381324 1,1
%A A381324 _Adam Wang_, Feb 20 2025