As a positive answer to your final question, normalization proofs of polymorphic lambda calculi such as the calculus of constructions require at least higher-order arithmetic, and stronger systems (such as the calculus of inductive constructions) are equiconsistent with ZFC plus countably many inaccessibles.
As a negative answer to your final question, Ben-David and Halevi have shown that if $P \not= NP$ is independent of $PA_1$, Peano arithmetic extended with axioms for all universal arithmetic truths, then there is an almost polynomial algorithm $DTIME(n^{\log^{*}(n)})$ for SAT. Furthermore, there are presently no known ways to generate sentences which are independent of $PA$ but not $PA_1$.
More philosophically, do not make the mistake of equating consistency strength with the strength of an abstraction.
The correct way to organize a subject may involve apparently wild set-theoretic principles, even though they may not be strictly necessary in terms of consistency strength. For example, strong collection principles are very useful for stating uniformity properties -- e.g., category theorists end up wanting weak large cardinal axioms to manipulate things like category of all groups as if they were objects. The most famous example is algebraic geometry, whose development makes extensive use of Grothendieck universes, but all of whose applications (such as Fermat's Last Theorem) apparently lie within third-order arithmetic. As a much more trivial example, note that the generic identity and composition operations are not functions, since they are indexed over the whole universe of sets.
On the other hand, sometimes the relationship between consistency strength and abstractness goes in the opposite direction. Consider the relationship between measures and motivic measures. Measures are defined on families of subsets ($\sigma$-algebras) over a set $X$, whereas motivic measures are defined directly on formulas interpreted in $X$. So even though motivic measure generalizes measure, the set-theoretic complexity goes down, since one use of powerset goes away.
EDIT: Logical system A has greater consistency strength than system B, if the consistency of A implies the consistency of B. For example, ZFC has greater consistency strength than Peano arithmetic, since you can prove the consistency of PA in ZFC. A and B have the same consistency strength if they are equiconsistent. As an example, Peano arithmetic is consistent if and only if Heyting (constructive) arithmetic is.
IMO, one of the most amazing facts about logic is that consistency strength boils down to the question "what is the fastest-growing function you can prove total in this logic?" As a result, the consistency of many classes of logics can be linearly ordered! If you have an ordinal notation capable of describing the fastest growing functions your two logics can show total, then you know by trichotomy that either one can prove the consistency of the other, or they are equiconsistent.
But this astonishing fact is also why consistency strength is not the right tool for talking about mathematical abstractions. It is an invariant of a system including coding tricks, and a good abstraction lets you express an idea without tricks. However, we do not know enough about logic to express this idea formally.
