Infeasible inconsistency

[Joe Shipman]

Does anyone know an interesting example of a consistent formal system in which 
1) There is a statement not-P with a proof of infeasible length
2) There are statements Q such that P—>Q has a feasible proof, Q does not have a feasible proof, and not-Q is not provable 

In other words, adding P as an axiom is not known to introduce a feasible inconsistency, but does allow feasible proofs of things which were either independent or previously had only infeasible proofs. 

— JS

Sent from my iPhone