[FOM] Fwd: A request--2nd reply to Mario Carneiro

[Tennant, Neil]

Mario Carneiro asked various questions, which I try here to answer.

"What is the complexity of a single derivation step in Core, since just tacking the new rule at the end is apparently insufficient?"
Unable to answer, since I don't know what is meant by the complexity of a derivation step. If it means the complexity of the decision problem "Is the final step of this proof-tree a correct application of a primitive rule of inference in Core Logic?", then I would venture the guess that it is the same as it would be for orthodox systems of natural deduction, for system like Classical, Intuitionistic and Minimal Logic.

"Is the normalization process proof-relevant, i.e. given two proofs of A |- B is it possible that an application of some inference rule like B |- C may yield A |- C for the first proof and A |- # or A' |- C for the other?"

Just to clarify, let me re-pose this question slightly more generally, with talk about sets of premises: suppose P1 and P2 are two different core proofs of the sequent X:B; and suppose also that P is a core proof of the sequent B,Y:C. Might it be that [P1,P] proves a sequent X',Y':# (for some subsets X', Y' of X, Y respectively) but that [P2,P] proves a sequent X*,*':# (for some subsets X*, Y* of X, Y respectively)?

I would cautiously answer in the affirmative, but have no concrete example at hand.

"Is it linear in the number of previous steps, or is it something worse, say exponential or super-exponential?"
Super-exponential, as for traditional cut-elimination.

BTW, I think there might have been an inversion of notation when Mario wrote
'If A |-c B then we could say "the assumptions in A imply B", or "A proves B classically", while if A |- B then we say "A exactly proves B" or "there is a normalized proof of A implies B" or "A proves B in core logic".'
Perhaps the two turnstiles need to be interchanged?

Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150909/185ec810/attachment-0001.html>