A strictly finitary non-triviality proof for a paraconsistent system of set theory deductively equivalent to classical ZFC minus foundation (Q1590193)

The paraconsistent system CPQ-ZFC/F is defined, where CPQ can be regarded as the first-order logic obtained from classical logic by removing modus ponens. Then CPQ-ZFC/F is a paraconsistent version of classical ZFC minus the axiom of foundation. It is shown using strong nonfinitary methods that CPQ-ZFC/F has the same deductive powers as classical ZFC/F. It is then shown using strictly finitary methods that CPQ-ZFC/F is non-trivial.