Is there a logic without induction that captures much of P? The Immerman-Vardi theorem 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, 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, 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, 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.
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.

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$).