Random idea for the Lobian obstacle that turned out not to work, but I decided to post anyway on the off chance someone can salvage it:

Inspired by the human brains bicameral system: Split the system into two, A and B. A has ((B proves C) -> C), B has ((A proves C) -> C). A, trusting B, can build B' as strong as B; B, trusting A, can build A' as strong as A.

Obvious flaw: A has ((B proves ((A proves C) -> C)) -> ((A proves C) -> C), so A has ((A proves C) -> C), and vice versa.