@Jonathan Castello

I suspect a better way to view the reachability and satisfiability as being equivalent would be to view a proof (more specifically modus ponens) as being a path between propositions.

I believe homotopy type theory makes this more explicit.