<p>You want to have a look at what some people call Grädel's Theorem. You can find it in Papadimitriou's book "Computational Complexity" (it's Theorem 8.4 in page 176) or in Grädel's original <a href="http://portal.acm.org/citation.cfm?id=136273">paper</a>.</p>

<p>In a nutshell, Grädel's Theorem is to P what Fagin's Theorem is to NP. It states that on the class of finite structures with a successor relation, the collection of polynomial-time decidable properties coincides with those expressible in the Horn-fragment of existential second-order logic. These are the sentences of second-order logic of the form
$$
(\exists R)(\forall x)(\phi)
$$
where $R$ is a sequence of second-order relation variables, $x$ is a sequence of first-order variables, and $\phi$ is a quantifier-free formula that, when written in CNF form, is a conjunction of $R$-Horn clauses (i.e. clauses that have at most one non-negated atom involving the variables in $R$).</p>

CC BY-SA 2.5
2010-09-27T18:05:32.860Z
Oops, now that I read your question again I realize that it is a bit different from the previous version. Now you ask for an operator X so that FOL+X captures a large fragment of P. In that case you should have a look at Dawar's <a href="http://logcom.oxfordjournals.org/content/5/2/213.abstract">paper</a>. He shows that if there is a logic for P, then there is one by extending FOL with generalized quantifiers.
slimton
CC BY-SA 2.5
2010-09-27T18:07:52.323Z
I should add that the Horn-fragment of existential second-order logic on naked structures is rather weak: a proper subset of LFP on naked structures. We need the successor to get Grädel's theorem. Dawar's result is for naked structures.
slimton
CC BY-SA 2.5
2010-09-27T17:58:40.910Z
2010-09-27T17:58:40.910Z
slimton
<p>There are recent exciting results concerning the search for a logic capturing PTIME. 
The famous example by <a href="http://dl.acm.org/citation.cfm?id=1398656">Cai, Fürer and Immerman </a>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 by <a href="http://link.springer.com/chapter/10.1007/978-3-540-69937-8_2">Dawar</a> that 
the class is not artificial at all. It can rather be seen as an example for the fact that LFP+C cannot
solve linear equation systems!</p>

<p>Hence <a href="http://www.automata.rwth-aachen.de/~grohe/pub/dawgrohollau09.pdf">Dawar, Grohe, Holm and Laubner</a> extended logics by operators from linear algebra, for example by an operator to define the rank of a definable matrix.
The resulting logic LFP+rank can express strictly more than LFP+C, in fact, there is no known PTIME property that LFP+rank cannot express. </p>

<p>Even FO+rk is surprisingly powerful, it can express deterministic and symmetric transitive closure. It is still open 
whether it can express the general transitive closure of a graph. </p>

CC BY-SA 3.0
2013-09-25T19:06:01.887Z
Note that Anderson/Dawar/Holm recently showed that FP+C can express linear programming (http://arxiv.org/abs/1304.6870).  This undermines an interpretation of Dawar's earlier result along the lines of "FP+C cannot solve linear equation systems"; Dawar only claimed that _some_ "natural problems involving systems of linear equations are not definable in this logic" with which he seems to have meant rank computations.
András Salamon
CC BY-SA 3.0
2013-09-25T09:37:34.887Z
2013-09-25T09:37:34.887Z
Sebastian Siebertz
<p>Depending on what you mean by "capture," <a href="http://www.google.com/url?sa=t&amp;source=web&amp;cd=2&amp;ved=0CB0QFjAB&amp;url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.6.1196%26rep%3Drep1%26type%3Dpdf&amp;rct=j&amp;q=polynomial%20time%20logic&amp;ei=tKd_TLfIOcjInAfcjJmFAQ&amp;usg=AFQjCNGLJ5S7rVs6MyxxVmFkFkRuLc2Uqw&amp;sig2=Iwnra3vcDRLpjwA_9bIgYw&amp;cad=rja" rel="noreferrer">Soft Linear Logic and Polynomial Time</a> by Yves Lafont may be of interest.  There is a 1-1 correspondence to proofs in this logic and PTIME algorithms that take a string as input and output 0 or 1.</p>

<p>The Wikipedia article on Linear Logic is <a href="http://en.wikipedia.org/wiki/Linear_logic" rel="noreferrer">here</a>.  It's not a fixpoint logic.  The intuition of "classical logic over $C^*$ algebras instead of boolean algebras" is the easiest for me to grasp.</p>

CC BY-SA 2.5
2010-09-02T15:46:17.163Z
I think András wants a logic in the sense of descriptive complexity.
Kaveh
CC BY-SA 2.5
2010-09-02T13:44:20.423Z
2010-09-02T13:44:20.423Z
Aaron Sterling
<blockquote>As far as I understand, linear logic can only express statements about structures that have quite restrictive form. I would ideally like to see a reference to, or a sketch of, a logic that can express properties of arbitrary sets of relational structures, while still avoiding fixed points. If I am wrong about the expressive power of linear logic then a pointer or hint would be welcome.</blockquote>

<p>This isn't right: all residuated commutative monoidal lattices are models of linear logic. Here's an easy way to create such a lattice from finite graphs. Start with the set </p>

<p>$$M = \{(g, n) \;|\; g\mbox{ is a finite graph and }n \subseteq \mathrm{nodes}(g)\}$$ </p>

<p>So our forcing relation will be $(g,n) \models \phi$, and the intuition is that $n$ is the set of nodes "owned" by the formula $\phi$. There is a partial operation $(\cdot) : M \times M \to M$, defined as:
$$
(g,n) \cdot (g&#39;,n&#39;) = \left\{\begin{array}{ll}
                               (g, n \uplus n&#39;) &amp; \mbox{when } g = g&#39; \land n \cap n&#39; = \emptyset \\ 
                               \mathrm{undefined} &amp; \mbox{otherwise}
                             \end{array}\right.
$$</p>

<p>This combines two elements by mergining their owned sets, if the graphs are equal and the owned sets are disjoint. </p>

<p>Now, we can give a model of linear logic as follows:</p>

<p>$$
\begin{array}{lcl}
(g,n) \models I &amp; \iff &amp; 
    n = \emptyset \\
(g,n) \models \phi \otimes \psi &amp; \iff &amp; 
   \exists n_1,n_2.\; n = n_1 \uplus n_2 \mbox{ and } (g,n_1) \models \phi \mbox{ and } (g,n_2) \models \psi \\
(g,n) \models \phi \multimap \psi &amp; \iff &amp; 
    \forall n&#39;.\; \mbox{if } n \cap n&#39; = \emptyset \mbox{ and } (g,n&#39;) \models \phi \mbox{ then } (g,n \uplus n&#39;) \models \psi \\
(g, n) \models \top &amp; \iff &amp; 
    \mbox{always} \\
(g,n) \models \phi \land \psi &amp; \iff &amp; 
    (g,n) \models \phi \mbox{ and } (g,n) \models \psi
\end{array}
$$</p>

<p>This model is actually a variant of the ones used in separation logic, which is widely used in the verification of heap-manipulating programs. (If you like, think of the graph as the pointer structure of the heap, and the analogy is exact!) </p>

<p>This isn't really the right way to think about linear logic, though: its real intuitions are proof-theoretic, and the connection to complexity comes via the computational complexity of the cut-elimination theorem. The model theory of linear logic is the shadow cast by its proof theory. </p>

CC BY-SA 3.0
2013-09-26T12:05:37.377Z
What role does the graph structure play in the above model?  The above definition seems to work fine if we say that g ranges over the discrete graphs.
Charles Stewart
CC BY-SA 3.0
2013-09-26T14:37:29.567Z
Since any (partial) commutative monoid can be used to give a model of BI/linear logic, the graph structure is not used to interpret the $\otimes$ and $\multimap$ connectives -- it only matters for the atomic propositions. For example, in separation logic, there is a "points-to" atomic proposition $n \mapsto n'$, which we use the pointer structure to interpret.
Neel Krishnaswami
CC BY-SA 3.0
2011-09-27T08:48:06.147Z
2011-09-28T07:39:30.997Z
2011-09-28T07:39:30.997Z
Neel Krishnaswami
<p>Some older work on this problem, again in the Linear Logic vein is, 
Jean-Yves Girard, Andre Scedrov, and Philip Scott. <em>Bounded linear logic: A modular approach to polynomial-time computability.</em> Theoretical Computer Science, 97(1):1–66, 1992.</p>

<p>More recent work includes <a href="http://arxiv.org/abs/0904.2675" rel="noreferrer"><em>Bounded Linear Logic, Revisited</em></a> by Ugo Dal Lago    and Martin Hofmann.</p>

CC BY-SA 2.5
2010-09-27T16:27:42.277Z
2010-09-27T16:27:42.277Z
Dave Clarke
<p>Let <span class="math-container">$L \subset K$</span> be two signatures and <span class="math-container">$\mathcal{L,K}$</span> be a nonempty classes of <span class="math-container">$L$</span>-structures and <span class="math-container">$K$</span>-structures respectively such that</p>
<ul>
<li>every structure in <span class="math-container">$\mathcal{L}$</span> has an expansion in <span class="math-container">$\mathcal{K}$</span>, and</li>
<li>the <span class="math-container">$L$</span>-reduct of every structure in <span class="math-container">$\mathcal{K}$</span> is contained in <span class="math-container">$\mathcal{L}$</span>.</li>
</ul>
<p>Let <span class="math-container">$\varphi$</span> be a <span class="math-container">$K$</span>-sentence. (Think first-order, but really it could be in any language.) We say that <span class="math-container">$\varphi$</span> is <em><span class="math-container">$\mathcal{(L,K)}$</span>-invariant</em> in case any two structures <span class="math-container">$A,B \in \mathcal{K}$</span> agree on <span class="math-container">$\varphi$</span> if their <span class="math-container">$L$</span>-reducts are isomorphic. This means that, morally speaking, <span class="math-container">$\varphi$</span> is meaningful over structures in <span class="math-container">$\mathcal{L}$</span>. We might define a quantifier <span class="math-container">$\mathfrak{Q}$</span> by
<span class="math-container">$$ M \models \mathfrak{Q}.\varphi \iff \text{for some/for any expansion $N$ of $M$ in $\mathcal{L}$, } N \models \varphi, $$</span>
where <span class="math-container">$M \in \mathcal{L}$</span>. So <span class="math-container">$\mathfrak{Q}$</span> is a sort of weak second-order quantifier that bounds the symbols in <span class="math-container">$K \setminus L$</span>. Now we can study <em><span class="math-container">$(\mathcal{L,K})$</span>-invariant FO definability,</em> i.e., subsets of <span class="math-container">$\mathcal{L}$</span> carved out by sentences of the form <span class="math-container">$\mathfrak{Q}.\varphi$</span>.</p>
<p>For applications to descriptive complexity theory, we want <span class="math-container">$\mathcal{L}$</span> to be the set of all <em>finite</em> <span class="math-container">$L$</span>-structures. (This means, note, that <span class="math-container">$\mathcal{K}$</span> is a set of arbitrarily large finite <span class="math-container">$K$</span>-structures.) For example, if <span class="math-container">$\mathcal{K}$</span> is the set of structures in <span class="math-container">$\mathcal{L}$</span> expanded by any linear order, we get <em>order-invariant first-order logic.</em> There is some hope of capturing (large) fragments of PTIME in this way. For example, <em>traversal-invariant</em> and <em>breadth-first traversal-invariant</em> FO logic capture L and NL respectively. (It's not perfect: we have to close under some very simple reductions.) But generally, the smaller <span class="math-container">$\mathcal{K}$</span> is, the more powerful <span class="math-container">$(\mathcal{L,K})$</span>-invariant definability is.</p>
<p>It's not a logic, properly speaking: we can't decide in general whether a formula is <span class="math-container">$(\mathcal{L,K})$</span>-invariant. (So I'm not sure whether this counts as a &quot;generalized quantifier.&quot;) But at least it's a candidate for capturing PTIME over arbitrary signatures, using something of the form FOL + X, where X is &quot;not based on fixed points.&quot;</p>

CC BY-SA 4.0
2024-05-22T19:02:19.693Z
2024-05-22T19:02:19.693Z
Siddharth
<p>The <a href="http://en.m.wikipedia.org/wiki/Least_fixed_point">Immerman-Vardi theorem</a> states that PTIME (or P) is precisely the class of languages that can be described by a sentence of First-Order Logic together with a fixed-point operator, over the class of ordered structures.  The fixed-point operator can be either least fixed-point (as considered by Immerman and by Vardi), or inflationary fixed-point.  (Stephan Kreutzer, <a href="http://dx.doi.org/10.1016/j.apal.2004.02.001"><em>Expressive equivalence of least and inflationary fixed-point logic</em></a>, Annals of Pure and Applied Logic <strong>130</strong> 61–78, 2004).</p>

<p>Yuri Gurevich conjectured that there is no logic capturing PTIME (<a href="http://research.microsoft.com/en-us/um/people/gurevich/Opera/74.pdf"><em>Logic and the Challenge of Computer Science</em></a>, in Current Trends in Theoretical Computer Science, ed. Egon Boerger, 1–57, Computer Science Press, 1988), while Martin Grohe has stated he is less sure (<a href="http://www2.informatik.hu-berlin.de/~grohe/pub/gro08b.pdf"><em>The Quest for a Logic Capturing PTIME</em></a>, FOCS 2008).</p>

<p>The fixed-point operator is meant to capture the power of recursion.  Fixed-points are powerful, but it isn't obvious to me that they are necessary.</p>

<blockquote>
  <p>Is there an operator X that is not based on fixed-points, such that FOL+X captures a (large) fragment of PTIME?</p>
</blockquote>

<p><strong>Edit:</strong> As far as I understand, linear logic can only express statements about structures that have quite restrictive form.  I would ideally like to see a reference to, or a sketch of, a logic that can express properties of arbitrary sets of relational structures, while still avoiding fixed points.  If I am wrong about the expressive power of linear logic then a pointer or hint would be welcome.</p>

CC BY-SA 2.5
2010-11-09T05:52:28.790Z
@Neel Krishnaswami: There are already classical first-order theories that capture P in that sense, i.e. the provably total function are exactly polytime computable ones, for example Steve Cook's evaluational theory $PV$ (1975) Sam Buss's theory $S^1_2$ (1985), but that's different from the descriptive complexity/finite model theoretical sense asked in this question.
Kaveh
CC BY-SA 3.0
2011-07-02T20:30:21.273Z
András, I think Gurevich conjectures that there is not a order-free logic that captures polytime order invariant graph properties, i.e. all queries in the language should return the same answer for a graph independent of the labeling of the vertices.
Kaveh
CC BY-SA 3.0
2011-09-26T21:59:48.497Z
I think [slimton's comment](http://cstheory.stackexchange.com/questions/869/is-there-a-logic-without-induction-that-captures-much-of-p/1732#comment-3446) answers your question more or less. Take an arbitrary polynomial-time computable property outside $\mathsf{FO}$ and you can turn it into a quantifier and add it to $\mathsf{FO}$.
Kaveh
CC BY-SA 3.0
2011-09-27T09:19:25.083Z
Kaveh, this is why I awarded the bounty to slimton.  A more detailed answer would still be nice.
András Salamon
CC BY-SA 2.5
2010-09-03T08:29:32.647Z
With "logic" I mean what Grohe means: a decidable set of sentences over the vocabulary, and a relation "is a model of" between finite structures and sentences, with the property that the set of models of a sentence is always closed under isomorphism.
András Salamon
CC BY-SA 2.5
2010-09-03T08:41:13.420Z
See also http://cstheory.stackexchange.com/questions/174/major-unsolved-problems-in-theoretical-computer-science/251#251 for the question of whether there is a logic that captures PTIME.
András Salamon
CC BY-SA 2.5
2010-09-27T21:00:33.717Z
Linear logic is a *propositional* logic which contains classical propositional logic. It can be extended to allow quantifiers. But if I remember correctly the relation between linear logic (propositional) and complexity classes is different from what Grohe has in his mind, at least I don't see how to relate linear logic to queries over finite structures.
Kaveh
CC BY-SA 2.5
2010-10-15T12:06:11.013Z
There are set theories built on linear logic, such as Terui's Light Affine Set Theory, which have the property that a function can be proved total in it, if and only if the function is computable in polynomial time. See http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730
Neel Krishnaswami
<cc.complexity-theory><lo.logic><descriptive-complexity><finite-model-theory>
Is there a logic without induction that captures much of P?
András Salamon
# Is there a logic without induction that captures much of P?

(Asked by: username_0 on 2010-09-02)

The [Immerman-Vardi theorem](http://en.m.wikipedia.org/wiki/Least_fixed_point) states that PTIME (or P) is precisely the class of languages that can be described by a sentence of First-Order Logic together with a fixed-point operator, over the class of ordered structures. The fixed-point operator can be either least fixed-point (as considered by Immerman and by Vardi), or inflationary fixed-point. (Stephan Kreutzer, [*Expressive equivalence of least and inflationary fixed-point logic*](http://dx.doi.org/10.1016/j.apal.2004.02.001), Annals of Pure and Applied Logic **130** 61–78, 2004).

Yuri Gurevich conjectured that there is no logic capturing PTIME ([*Logic and the Challenge of Computer Science*](http://research.microsoft.com/en-us/um/people/gurevich/Opera/74.pdf), in Current Trends in Theoretical Computer Science, ed. Egon Boerger, 1–57, Computer Science Press, 1988), while Martin Grohe has stated he is less sure ([*The Quest for a Logic Capturing PTIME*](http://www2.informatik.hu-berlin.de/~grohe/pub/gro08b.pdf), FOCS 2008).

The fixed-point operator is meant to capture the power of recursion. Fixed-points are powerful, but it isn't obvious to me that they are necessary.

> Is there an operator X that is not based on fixed-points, such that FOL+X captures a (large) fragment of PTIME?

**Edit:** As far as I understand, linear logic can only express statements about structures that have quite restrictive form. I would ideally like to see a reference to, or a sketch of, a logic that can express properties of arbitrary sets of relational structures, while still avoiding fixed points. If I am wrong about the expressive power of linear logic then a pointer or hint would be welcome.

**Tags:** cc.complexity-theory, lo.logic, descriptive-complexity, finite-model-theory

> **Comments:**
> **username_0**: With "logic" I mean what Grohe means: a decidable set of sentences over the vocabulary, and a relation "is a model of" between finite structures and sentences, with the property that the set of models of a sentence is always closed under isomorphism.  
> **username_0**: See also http://cstheory.stackexchange.com/questions/174/major-unsolved-problems-in-theoretical-computer-science/251#251 for the question of whether there is a logic that captures PTIME.  
> **username_1**: Linear logic is a *propositional* logic which contains classical propositional logic. It can be extended to allow quantifiers. But if I remember correctly the relation between linear logic (propositional) and complexity classes is different from what Grohe has in his mind, at least I don't see how to relate linear logic to queries over finite structures.  
> **username_2**: There are set theories built on linear logic, such as Terui's Light Affine Set Theory, which have the property that a function can be proved total in it, if and only if the function is computable in polynomial time. See http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.730  
> **username_1**: @username_2: There are already classical first-order theories that capture P in that sense, i.e. the provably total function are exactly polytime computable ones, for example Steve Cook's evaluational theory $PV$ (1975) Sam Buss's theory $S^1_2$ (1985), but that's different from the descriptive complexity/finite model theoretical sense asked in this question.  
> **username_1**: András, I think Gurevich conjectures that there is not a order-free logic that captures polytime order invariant graph properties, i.e. all queries in the language should return the same answer for a graph independent of the labeling of the vertices.  
> **username_1**: I think [username_3's comment](http://cstheory.stackexchange.com/questions/869/is-there-a-logic-without-induction-that-captures-much-of-p/1732#comment-3446) answers your question more or less. Take an arbitrary polynomial-time computable property outside $\mathsf{FO}$ and you can turn it into a quantifier and add it to $\mathsf{FO}$.  
> **username_0**: username_1, this is why I awarded the bounty to username_3.  A more detailed answer would still be nice.  

---

## 6 answers

### Answer by username_3 on 2010-09-27. Score: 26

You want to have a look at what some people call Grädel's Theorem. You can find it in Papadimitriou's book "Computational Complexity" (it's Theorem 8.4 in page 176) or in Grädel's original [paper](http://portal.acm.org/citation.cfm?id=136273).

In a nutshell, Grädel's Theorem is to P what Fagin's Theorem is to NP. It states that on the class of finite structures with a successor relation, the collection of polynomial-time decidable properties coincides with those expressible in the Horn-fragment of existential second-order logic. These are the sentences of second-order logic of the form
$$
(\exists R)(\forall x)(\phi)
$$
where $R$ is a sequence of second-order relation variables, $x$ is a sequence of first-order variables, and $\phi$ is a quantifier-free formula that, when written in CNF form, is a conjunction of $R$-Horn clauses (i.e. clauses that have at most one non-negated atom involving the variables in $R$).

> **Comments:**
> **username_3**: Oops, now that I read your question again I realize that it is a bit different from the previous version. Now you ask for an operator X so that FOL+X captures a large fragment of P. In that case you should have a look at Dawar's <a href="http://logcom.oxfordjournals.org/content/5/2/213.abstract">paper</a>. He shows that if there is a logic for P, then there is one by extending FOL with generalized quantifiers.  
> **username_3**: I should add that the Horn-fragment of existential second-order logic on naked structures is rather weak: a proper subset of LFP on naked structures. We need the successor to get Grädel's theorem. Dawar's result is for naked structures.  

---

### Answer by username_4 on 2013-09-25. Score: 11

There are recent exciting results concerning the search for a logic capturing PTIME.
The famous example by [Cai, Fürer and Immerman](http://dl.acm.org/citation.cfm?id=1398656) 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 by [Dawar](http://link.springer.com/chapter/10.1007/978-3-540-69937-8_2) that
the class is not artificial at all. It can rather be seen as an example for the fact that LFP+C cannot
solve linear equation systems!

Hence [Dawar, Grohe, Holm and Laubner](http://www.automata.rwth-aachen.de/~grohe/pub/dawgrohollau09.pdf) extended logics by operators from linear algebra, for example by an operator to define the rank of a definable matrix.
The resulting logic LFP+rank can express strictly more than LFP+C, in fact, there is no known PTIME property that LFP+rank cannot express.

Even FO+rk is surprisingly powerful, it can express deterministic and symmetric transitive closure. It is still open
whether it can express the general transitive closure of a graph.

> **Comments:**
> **username_0**: Note that Anderson/Dawar/Holm recently showed that FP+C can express linear programming (http://arxiv.org/abs/1304.6870).  This undermines an interpretation of Dawar's earlier result along the lines of "FP+C cannot solve linear equation systems"; Dawar only claimed that _some_ "natural problems involving systems of linear equations are not definable in this logic" with which he seems to have meant rank computations.  

---

### Answer by username_5 on 2010-09-02. Score: 8

Depending on what you mean by "capture," [Soft Linear Logic and Polynomial Time](http://www.google.com/url?sa=t&source=web&cd=2&ved=0CB0QFjAB&url=http%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fdownload%3Fdoi%3D10.1.1.6.1196%26rep%3Drep1%26type%3Dpdf&rct=j&q=polynomial%20time%20logic&ei=tKd_TLfIOcjInAfcjJmFAQ&usg=AFQjCNGLJ5S7rVs6MyxxVmFkFkRuLc2Uqw&sig2=Iwnra3vcDRLpjwA_9bIgYw&cad=rja) by Yves Lafont may be of interest. There is a 1-1 correspondence to proofs in this logic and PTIME algorithms that take a string as input and output 0 or 1.

The Wikipedia article on Linear Logic is [here](http://en.wikipedia.org/wiki/Linear_logic). It's not a fixpoint logic. The intuition of "classical logic over $C^\*$ algebras instead of boolean algebras" is the easiest for me to grasp.

> **Comments:**
> **username_1**: I think András wants a logic in the sense of descriptive complexity.  

---

### Answer by username_2 on 2011-09-27. Score: 8

> As far as I understand, linear logic can only express statements about structures that have quite restrictive form. I would ideally like to see a reference to, or a sketch of, a logic that can express properties of arbitrary sets of relational structures, while still avoiding fixed points. If I am wrong about the expressive power of linear logic then a pointer or hint would be welcome.

This isn't right: all residuated commutative monoidal lattices are models of linear logic. Here's an easy way to create such a lattice from finite graphs. Start with the set

$$M = \{(g, n) \;|\; g\mbox{ is a finite graph and }n \subseteq \mathrm{nodes}(g)\}$$

So our forcing relation will be $(g,n) \models \phi$, and the intuition is that $n$ is the set of nodes "owned" by the formula $\phi$. There is a partial operation $(\cdot) : M \times M \to M$, defined as:
$$
(g,n) \cdot (g',n') = \left\{\begin{array}{ll}
(g, n \uplus n') & \mbox{when } g = g' \land n \cap n' = \emptyset \\
\mathrm{undefined} & \mbox{otherwise}
\end{array}\right.
$$

This combines two elements by mergining their owned sets, if the graphs are equal and the owned sets are disjoint.

Now, we can give a model of linear logic as follows:

$$
\begin{array}{lcl}
(g,n) \models I & \iff &
n = \emptyset \\
(g,n) \models \phi \otimes \psi & \iff &
\exists n\_1,n\_2.\; n = n\_1 \uplus n\_2 \mbox{ and } (g,n\_1) \models \phi \mbox{ and } (g,n\_2) \models \psi \\
(g,n) \models \phi \multimap \psi & \iff &
\forall n'.\; \mbox{if } n \cap n' = \emptyset \mbox{ and } (g,n') \models \phi \mbox{ then } (g,n \uplus n') \models \psi \\
(g, n) \models \top & \iff &
\mbox{always} \\
(g,n) \models \phi \land \psi & \iff &
(g,n) \models \phi \mbox{ and } (g,n) \models \psi
\end{array}
$$

This model is actually a variant of the ones used in separation logic, which is widely used in the verification of heap-manipulating programs. (If you like, think of the graph as the pointer structure of the heap, and the analogy is exact!)

This isn't really the right way to think about linear logic, though: its real intuitions are proof-theoretic, and the connection to complexity comes via the computational complexity of the cut-elimination theorem. The model theory of linear logic is the shadow cast by its proof theory.

> **Comments:**
> **username_6**: What role does the graph structure play in the above model?  The above definition seems to work fine if we say that g ranges over the discrete graphs.  
> **username_2**: Since any (partial) commutative monoid can be used to give a model of BI/linear logic, the graph structure is not used to interpret the $\otimes$ and $\multimap$ connectives -- it only matters for the atomic propositions. For example, in separation logic, there is a "points-to" atomic proposition $n \mapsto n'$, which we use the pointer structure to interpret.  

---

### Answer by username_7 on 2010-09-27. Score: 7

Some older work on this problem, again in the Linear Logic vein is,
Jean-Yves Girard, Andre Scedrov, and Philip Scott. *Bounded linear logic: A modular approach to polynomial-time computability.* Theoretical Computer Science, 97(1):1–66, 1992.

More recent work includes [*Bounded Linear Logic, Revisited*](http://arxiv.org/abs/0904.2675) by Ugo Dal Lago and Martin Hofmann.


---

### Answer by username_8 on 2024-05-22. Score: 0

Let $L \subset K$ be two signatures and $\mathcal{L,K}$ be a nonempty classes of $L$-structures and $K$-structures respectively such that

* every structure in $\mathcal{L}$ has an expansion in $\mathcal{K}$, and
* the $L$-reduct of every structure in $\mathcal{K}$ is contained in $\mathcal{L}$.

Let $\varphi$ be a $K$-sentence. (Think first-order, but really it could be in any language.) We say that $\varphi$ is *$\mathcal{(L,K)}$-invariant* in case any two structures $A,B \in \mathcal{K}$ agree on $\varphi$ if their $L$-reducts are isomorphic. This means that, morally speaking, $\varphi$ is meaningful over structures in $\mathcal{L}$. We might define a quantifier $\mathfrak{Q}$ by
$$ M \models \mathfrak{Q}.\varphi \iff \text{for some/for any expansion $N$ of $M$ in $\mathcal{L}$, } N \models \varphi, $$
where $M \in \mathcal{L}$. So $\mathfrak{Q}$ is a sort of weak second-order quantifier that bounds the symbols in $K \setminus L$. Now we can study *$(\mathcal{L,K})$-invariant FO definability,* i.e., subsets of $\mathcal{L}$ carved out by sentences of the form $\mathfrak{Q}.\varphi$.

For applications to descriptive complexity theory, we want $\mathcal{L}$ to be the set of all *finite* $L$-structures. (This means, note, that $\mathcal{K}$ is a set of arbitrarily large finite $K$-structures.) For example, if $\mathcal{K}$ is the set of structures in $\mathcal{L}$ expanded by any linear order, we get *order-invariant first-order logic.* There is some hope of capturing (large) fragments of PTIME in this way. For example, *traversal-invariant* and *breadth-first traversal-invariant* FO logic capture L and NL respectively. (It's not perfect: we have to close under some very simple reductions.) But generally, the smaller $\mathcal{K}$ is, the more powerful $(\mathcal{L,K})$-invariant definability is.

It's not a logic, properly speaking: we can't decide in general whether a formula is $(\mathcal{L,K})$-invariant. (So I'm not sure whether this counts as a "generalized quantifier.") But at least it's a candidate for capturing PTIME over arbitrary signatures, using something of the form FOL + X, where X is "not based on fixed points."


---

