[FOM] A question on Core Logic

[Astor, Eric P.]

A (hopefully brief) request for clarification. I will skip the context (as it's actually irrelevant) and focus on something Neil said:

"Yes one can, in Core Logic.  There is the primitive rule (for arithmetic)

          t+1 = 0
         _______
               #
               
               
 So there is the proof
 
          _______________(1)
           ((1+1)+...)+1 = 0
           ________________
                        #
       ________________________(1)
       ((1+1)+...)+1 = 0  ->  1=0
"
       
Let me check something. Neil tells us that Core Logic does not admit EFQ (i.e., we cannot derive Q from #).

However, (possibly Classical) Core Logic DOES allow us to derive (P -> Q) from (P -> #), yes? This would seem to be used by the proof given above. (If not, please consider this post moot - though I'd appreciate an off-list explanation.)

If so, then since Core Logic does not prove EFQ, then it seems that at least one of the following derivations must be impossible in Core Logic:
1) Derive Q from (T -> Q),
2) Derive (T -> Q) from Q,
as otherwise, I think we can construct a naïve derivation of EFQ... unless I'm missing something that renders another step invalid. 
 
I'm certain at least one of the above things is invalid in Core Logic. However, as I'm not experienced with it... which one?

Thanks,
- Eric Astor