Talk:Deolalikar P vs NP paper

I think Dr. Dawar's concern regarding non-order-invariance of individual stages of the LFP formula is the biggest issue here; because the formula itself is order-invariant does not entitle us to wish that its stages are; this includes a (necessarily) non-operation-preserving mapping to its successor, if I am truly able to read math at this level. My question is: can a method be found to show mutual congruence of some or all differently-ordered LFP stages, or at least to show equivalence wrt LFP?