In Shoenfield's Mathematical Logic, chapter 4, problem 6, it asks us to show that the following formal system is equivalent to first-order logic (the problem is here).
I suspect that there is a mistake in the not-or rule because from it I can derive a theorem that shouldn't be in FOL (namely, define A and C to be any False proposition and B to be a True proposition).
Thanks!