Finitely Axiomatized Set Theory: a nonclassical first-order theory implying ZF

TL;DR

This paper introduces FAST, a finite, nonclassical first-order set theory extending ZF with new logical concepts, enabling finite axiomatization and derivation of ZF axioms.

Contribution

It presents a novel finite axiomatization of ZF using extended logic and a new axiom, FAM, which generalizes pair axioms and derives ZF schemes.

Findings

FAST is finite and nonclassical.

FAM enables derivation of ZF axioms.

Loewenheim-Skolem theorem does not hold for FAST.

Abstract

It is well-known that a finite axiomatization of Zermelo-Fraenkel set theory (ZF) is not possible in the same first-order language. In this note we show that a finite axiomatization is possible if we extent the language of ZF with the new logical concept of 'universal quantification over a family of variables indexed in an arbitrary set X' and with a concept of generalized disjunction. We axiomatically introduce Finitely Axiomatized Set Theory (FAST), which consists of eleven theorems of ZF plus a new constructive axiom called the family set axiom (FAM), the latter is a generalization of the pair axiom of ZF, and uses the new concepts. We prove that FAM enables to derive the axioms schemes of separation and substitution of ZF from FAST, and that the Loewenheim-Skolem theorem does not hold for FAST. The conclusions are (i) that FAST is a finite, nonclassical first-order theory, and (ii) that FAST implies ZF.