Undecidability of finitary set theories and classical arithmetic

[dominik-kirst]

This PR contributes the undecidability of several first-order axiomatisations of finitary set theories and classical arithmetic. The code was developed with @HermesMarc during preparation of the extended version of our ITP'21 paper on incompleteness and ported to Coq 8.15 by @JoJoDeveloping.

In summary, the following new problems are added:

• HF and HFN in ZF.v: core of ZF axioms without infinity (HF) and negated infinity (HFN). The former is shown undecidable by reduction from the core axioms with infinity, the latter by reworking the reduction to ZF by replacing elements of omega by hereditarily transitive sets. These sets are exactly the natural numbers in the employed HFS model of hereditarily finite sets (first constructed in Coq by (Smolka/Stark)[https://www.ps.uni-saarland.de/extras/hfs/] and reimplemented by @DmxLarchey in TRAKHTENBROT/hfs.v).
• FST and FSTI in FST.v: axiomatisations of finitary set theory in the signature using empty set and adjunction based on the axioms formulated by Smolka/Stark, without (FST) and with (FSTI) an induction axiom limiting the size. Again, the former reduction is directly from ZF while the latter is a reworked version of the original reduction to ZF employing the HFS model.
• binFST in binFST.v: variant of FST over the binary signature (just containing membership). The undecidability is shown by direct reduction from the binary variant of ZF.
• cdeduction_FA, cdeduction_Q, and cdeduction_PA in PA.v: classical deduction over the arithmetic systems Q', Q, and PA. We employ a general Friedman translation in Util/Friedman.v to sidestep the usual issue that classical deduction can't be shown sound for the standard model constructively.

[mrhaandi]

I annotated my comments above only once. Of course, they hold for other files in this PR. Ideally, the new proofs should compile with

Set Default Goal Selector "!".
Set Default Proof Using "Type". (* if there are Sections *)
Set Mangle Names. (* make compatible, but remove in the final version *)

and properly encapsulate Notations, Hints, Instances, ...

[yforster]

Is this PR still active or will it be subsumed by the upcoming proper integration of the FOL library?

[dominik-kirst]

This will be subsumed.