25
Firstly, I want to address the comments to the question, where it was suggested that "false" expresses $P = PSPACE$ because the statement is false. While this might be a good joke, it is actually very much harmful to think this way. When we ask how to express a certain sentence in a certain formal system, we are not talking about truth values. If we were, ...
21
Andrej has already explained that $P=\mathit{PSPACE}$ can be written as a $\Sigma^0_2$-sentence. Let me mention that this classification is optimal in the sense that if the statement is equivalent to a $\Pi^0_2$-sentence, then this fact does not relativize. More precisely, the set of oracles $A$ such that $P^A=\mathit{PSPACE}^A$ is definable by a $\Sigma^0_2$...
12
Take a relation $R \subseteq X \times X$. Now, let $R^\dagger$ be the converse relation to $R$, and let $\Delta_X$ be the identity relation on $X$.
The commutative transitive closure $R^*$ is the smallest relation $S $ such that $\Delta_X \cup R \cup R^\dagger \cup S \circ S \subseteq S$.
Intuitively, think of the relation $R$ as being the edge relation ...
11
As you move to higher-order logics, each new order gives you quantification over exponentially larger objects than before, thus you can simulate exponentially longer computations. Other than that, it works pretty much the same as in the second-order case.
More precisely, define the iterated exponential function $2_d^x$ by
$$\begin{align*}2_0^x&=x,\\2_{d+...
10
Consider the boolean algebra formed from the powerset of a finite set $S$, ordered by set inclusion. Now, consider the operator $P$ defined by
$$
P(X) = \lnot X
$$
Clearly $P$ is a non-positive operator.
Show that there are no fixed points $\mu P$ such that $P(\mu P) = \mu P$. As a result, you can conclude that $\mu X.\;P(X)$ cannot be well-defined.
...
10
If you are having trouble with the concept of least fixed point, I would recommend spending some time getting a background in more general order theory.
Davey and Priestley, Introduction to Lattices and Order is a good intro.
To see why the transitive closure is the least fixed point, imagine building up the closure from an empty set, applying the logical ...
8
Think of $\Sigma^{*}$ encoding some sort of objects, and $Q$ as the set of all objects satisfying some property. Think of $P$ as a function which accepts (the encoding of) a pair $(x, p)$ where $x$ is an object and $p$ is alleged "evidence" of $x \in Q$. The function $P$ is a "proof checker": it verifies that $p$ actually represents valid evidence that $x \...
8
There are recent exciting results concerning the search for a logic capturing PTIME.
The famous example by Cai, Fürer and Immerman showing that LFP+C does not capture
PTIME was based on a seemingly artificial class of graphs, though. Of course, it was constructed for the particular
task of demonstrating the restrictions of LFP+C. Only recently it was shown ...
8
FO-LFP is neither complete (its valid sentences cannot be described by a recursively presented proof system) nor compact (there is an unsatisfiable set of sentences all of whose finite subsets are satisfiable). The basic argument is given in Denis’s answer so I won’t repeat it here, but let me instead point out that as a general principle due to Per ...
6
In fact, the circuit depends on the input structure, not only on the input structure size. We take a tree-decomposition of the graph with additional colours and turn it into a convolution tree. The evaluation of the formula on this tree is reduced to computing the value of the convolution tree. To compute the value of the tree, it is turned into an ...
6
There is a famous example of Cai, Fürer and Immerman, which shows that the $\mathcal{C}_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}_{\infty\omega}^\omega$ cannot express every query on finite structures. The paper is quite famous because it disproved a conjecture that IFP+C captures PTIME. Your proof that $\mathcal{L}_{\infty\...
6
The issue in play here is whether you use a self-terminating encoding (like your C example) or not. If you use a self-terminating encoding, then the subadditivity property does hold. If you don't (as in the common definition), then you need to expend bits on delimiting encodings.
Self-terminating encodings have other advantages, and even though real ...
6
Standard notions of reduction used in Descriptive Complexity are first-order reduction and the weaker first-order projection. Definitions of both these notions are found in Immerman's book on Descriptive Complexity.
5
This is only a partial answer (to the $PSPACE$ characterization), but I don't have the reputation to comment.
$PSPACE$ has the following (equivalent) descriptive characterizations:
$FO[2^{n^{O(1)}}]$, first-order logic with exponentially iterated quantifier blocks.
$SO[n^{O(1)}]$, second-order logic with polynomially iterated quantifier blocks.
$SO[TC]$, ...
5
See the Wikipedia article for propositional proof complexity. p-simulation is similar to reductions between complexity classes. Existence of a p-optimal proof system is a well-known open problem in proof complexity.
It is statement 7 in Krajicek and Pudlak 1989. See page 1066 and 1067 for a list of statements implied/implying it. There are more statements ...
5
You should think of the input of the proof system $P$ as the text of a proof $\pi$ of an element $q \in Q$. If the text is valid that $P(\pi) = q$, otherwise $P(\pi)$ is some fixed $q_0 \in Q$. We want $P$ to be polytime since that means that the proof is easy to verify.
As an example, suppose $Q$ is the set of propositional tautologies, and $P$ is any ...
5
I am not completely sure what you are looking for, but the following might
be interesting to you:
The idea that restricting numerical predicates in FO-formula corresponds to uniformity conditions is explicitly investigated, for example, in the paper
"FO(<)-uniformity" by Behle and Lange.
The survey "Arithmetic, first-order logic, and counting ...
4
Here's a more reality-concerned version of tigreen's answer from the point of a person who actually makes heavy use of (relational) databases: The whole point and complexity of their application is to structure them in a way they'd require as little amount of joins for each and every ever-needed query as possible and that's why they actually Do Work.
In ...
4
People informally use the phrase "a logic for P" for the notion of a logic that captures P, which corresponds to Chen and Flum's definition of a "P-bounded logic for P". Essentially, this means that the logic defines exactly the polynomial-time properties of relational structures and formulae can be evaluated in polynomial time.1 Specifically, ...
4
Answer to your first question http://www.cs.umd.edu/~gasarch/BLOGPAPERS/cfg.pdf.
A summary of the proof given in the link. First, it is shown that proving $L \cap R$ is CFL reduces to proving that $L \cap R'$ is CFL, where $R'$ is a regular language recognized by a DFA with exactly one final state. Then from the grammar for L (in Chomsky normal form) and ...
3
You have a non-deterministic algorithm deciding the problem.
If you want to think of it as a proof system for $EQUIV$, then
the proof of $(u,v) \in EQUIVE$ is just the string
representing the computation of your algorithm on $(u,v)$.
The proof checker just checks that
the given string is in fact an accepting computation of your algorithm on $(u,v)$.
Use ...
3
Part of the answer is in your question: if your language is FO-rewritable, query answering is in $\textrm{AC}_0$ in data complexity, which is almost as good as it gets. However, keep in mind that you have to pay the cost of computing $Q_\Sigma$, which might be expensive, though you have to do it only once.
Other good thing is that, for a FO-rewritable ...
2
this is a very old post so you might have already encountered the answer as desired. Since I have been studying FO(LFP) for the past few months. I have some understanding of the answers you require.
To answer the requirement of positivity, the need comes from the fact that testing whether the formula captures a monotone operator or not is undecidable both ...
2
Here is another attempt at a more comprehensive answer. Your question already contains the formal definition of FO-rewritability, which at its core says that you can reduce a query answering problem:
The problem $D\cup\Sigma\models Q$ is being reduced to a problem $D\models Q_\Sigma$.
Several noteworthy things are happening here. The original problem is ...
2
Martin Grohe made substantial progress on this question recently. He gives a logic capturing polynomial time on classes of graphs embeddable in a fixed surface: https://dl.acm.org/citation.cfm?doid=2371656.2371662
Edit: the general case seems to be unresolved (but I am by no means an expert on this).
2
Kaveh's response exemplifies well the Cook-Reckhow notion of an abstract proof system. Nonetheless, for comparison, I point to a recent preprint of mine and Damien Pous:
A cut-free cyclic proof system for Kleene Algebra
Here we give a more traditional bona fide proof system for equivalence of regular expressions by allowing non-wellfounded reasoning in ...
2
For the case of Schaefer's dichotomy theorem, informally, the universal expressive power of Boolean CNF formulas built from non-Schaefer logical relations is behind the dichotomy. Every logical relation is definable by such formula using existential quantifier. This is stated formally in Schaefer's expressibility theorem (Theorem 2.5).
answered Oct 13 '15 at 7:57
Mohammad Al-Turkistany
19.5k4 gold badges51 silver badges134 bronze badges
2
It does not extend.
Consider FO-LFP with just a binary predicate $<$, and the axioms for $<$ being a total order, with first and last positions, and every position has a successor. Moreover, we add an axiom saying that the last position can be reached from the first by iterating the successor function as a smallest fixpoint. This ensures that the ...
2
First question: A set $M$ is decidable if there is a Turing Machine which halts on all inputs and accepts all inputs $x$ with $x \in M$.
We try to encode $\bigwedge_{\phi \in X} \phi$ for arbitrary sets of $\mathsf{FO}[\tau]$-formulars $X$. Since, $\mathcal{P}(X)$ is uncountable there can be no code with finite alphabet. Hence, there can be no Turing ...
1
This is a classical cross-product construction, originally published
by Bar-Hillel, Perles and Shamir (1961) in On formal properties of
simple phrase structure grammars.It can be found in most elementary
books on automata theory. (the reference to the initial paper appears in the paper suggested by @Jurij, which I could not access as I wrote this answer).
...
Only top voted, non community-wiki answers of a minimum length are eligible
