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.
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.