Hm. I spent a little more time digging here. The specific reachability problem in question concerns Petri nets; this is good, because reachability is definitely solvable in polynomial time [for finite directed graphs](https://en.wikipedia.org/wiki/Floyd%E2%80%93Warshall_algorithm). The issue seems to be that Petri nets induce an infinite directed graph of a particular character, whose vertices are sets of resources (the set of tokens placed on the Petri net at a given time, I believe) and whose edges are given by the action of the Petri net itself. There is a considerable amount of regularity to this graph -- as one would expect of something with a finite description! -- but not enough to give anything resembling a reasonable algorithm. (Phrased this way, it's somewhat surprising it's decidable at all.)

On the other hand, Petri net reachability _is_ decidable. This isn't true of most proof systems of any strength. John's book explains why this is interesting:

> On the bright side, it means that Petri nets might be fairly powerful when viewed as computers themselves! After all, for a universal Turing machine, the analogue of the reachability problem is undecidable. So if the reachability problem for Petri nets were decidable, they couldn’t serve as universal computers. But if it were decidable but hard, Petri nets might be fairly powerful—though still not universal—computers.

As for satisfiability, we're given a formula of finite size \\(n\\) and asked to determine if it has any satisfying assignment. There can only be at most \\(2^n\\) assignments, so we can brute-force all of them to give a singly-exponential algorithm. This is a significantly better bound than anything referenced in Section 25.1 of John's book, so I am inclined to believe that (a) Petri net reachability is significantly more powerful than propositional satisfiability, and that (b) if an equivalence were established, that would be worth a publication.

(EDIT: Still mulling this one over. It isn't obvious whether Petri net reachability is in NP at all. I can imagine that there exist reachability problems where the shortest witnesses are exponential in the size of the Petri net. From problem 51 (Section 25.2) in John's book, this would probably involve giving a presentation of the desired arrow in terms of the Petri net morphisms and tensor product. Given such a presentation, we can surely check that it does indeed produce the arrow we desire; but if no polynomial-sized presentation is guaranteed to exist, we can't rightly say the problem is in NP.)

On the other hand, Petri net reachability _is_ decidable. This isn't true of most proof systems of any strength. John's book explains why this is interesting:

> On the bright side, it means that Petri nets might be fairly powerful when viewed as computers themselves! After all, for a universal Turing machine, the analogue of the reachability problem is undecidable. So if the reachability problem for Petri nets were decidable, they couldn’t serve as universal computers. But if it were decidable but hard, Petri nets might be fairly powerful—though still not universal—computers.

As for satisfiability, we're given a formula of finite size \\(n\\) and asked to determine if it has any satisfying assignment. There can only be at most \\(2^n\\) assignments, so we can brute-force all of them to give a singly-exponential algorithm. This is a significantly better bound than anything referenced in Section 25.1 of John's book, so I am inclined to believe that (a) Petri net reachability is significantly more powerful than propositional satisfiability, and that (b) if an equivalence were established, that would be worth a publication.

(EDIT: Still mulling this one over. It isn't obvious whether Petri net reachability is in NP at all. I can imagine that there exist reachability problems where the shortest witnesses are exponential in the size of the Petri net. From problem 51 (Section 25.2) in John's book, this would probably involve giving a presentation of the desired arrow in terms of the Petri net morphisms and tensor product. Given such a presentation, we can surely check that it does indeed produce the arrow we desire; but if no polynomial-sized presentation is guaranteed to exist, we can't rightly say the problem is in NP.)