Abstract This paper presents the logics with second-order quantifiers that range over relations of polylogarithmic size (log-quantifiers). The logic $\text{SO}^{\text{plog}} \text{-} \text{FO}$ is constituted of the formulas that extend first-order formulas by log-quantifier prefixes. We show that $\text{SO}^{\text{plog}} \text{-} \text{FO}$ collapses to its binary fragment where log-quantifiers range only over unary and binary relations. We further investigate the 0-1 law for $\text{SO}^{\text{plog}}\text{-}\text{FO}$, demonstrating that it fails in general, yet holds for its monadic existential fragment over the vocabulary that contains only unary relation symbols. Finally, we study the logical characterizations for complexity classes with limited non-determinism. On ordered structures, we show that if a logic $\mathcal L$ captures a complexity class $\mathcal C$, then the logic $\varSigma ^{\log ^{k}}_{1}\text{-}\mathcal L$ captures the complexity class $GC(\log ^{k+1}(n), \mathcal C)$, where $\mathcal L \in \{\text{DTC}, \text{TC}, \text{IFP}\}$. Consequently, $\varSigma _{1}^{\text{plog}}\text{-} \text{IFP}$ captures $\beta \text{P}$ on ordered structures.

Showing that a problem is hard for a model of computation is one of the most challenging tasks in theoretical computer science, logic and mathematics. For example, it remains beyond reach to find an explicit problem that cannot be computed by polynomial size propositional formulas (PF). As a model of computation, logic programs (LP) under answer set semantics are as expressive as PF and also \(\mathtt{NP}\) -complete for satisfiability checking. In this article, we show that the PAR problem is hard for LP, i.e., deciding whether a binary string contains an odd number of \(1\) ’s requires exponential size LP. The proof idea is first to transform logic programs into equivalent boolean circuits and then apply a probabilistic method known as random restriction to obtain an exponential lower bound. Based on the main result, we generalize a sufficient condition for identifying hard problems for LP and give a separation map for an LP family from a computational point of view, whose members are all equally expressive and share the same reasoning complexity.

We study the expressive power and complexity of second-order revised Krom logic (SO-KROM$^{r}$). On ordered finite structures, we show that its existential fragment $\Sigma^1_1$-KROM$^r$ equals $\Sigma^1_1$-KROM, and captures NL. On all finite structures, for $k\geq 1$, we show that $\Sigma^1_{k}$ equals $\Sigma^1_{k+1}$-KROM$^r$ if $k$ is even, and $\Pi^1_{k}$ equals $\Pi^1_{k+1}$-KROM$^r$ if $k$ is odd. The result gives an alternative logic to capture the polynomial hierarchy. We also introduce an extended version of second-order Krom logic (SO-EKROM). On ordered finite structures, we prove that SO-EKROM collapses to $\Pi^{1}_{2}$-EKROM and equals $\Pi^1_1$. Both SO-EKROM and $\Pi^{1}_{2}$-EKROM capture co-NP on ordered finite structures.

In this paper we investigate the existence of model-equivalence reduction between NP-logic systems which are logic systems with model existence problem in NP. It is shown that among all NP-systems with model checking problem in NP, the existentially quantified propositional logic (\exists PF) is maximal with respect to poly-time model-equivalent reduction. However, \exists PF seems not a maximal NP-system in general because there exits a NP-system with model checking problem D^P-complete.