5
$\begingroup$

What is the shortest definition of "$x$ is a finite class" that can be formulated in the class theory presented at:

Is it possible to derive the rules of set theory as transfers from the pure finite set world, and can we extend this further?

Here shortness is measured by the total number of occurrences of atomic formulas in the formula.

Some constraints are that:

  • the formula must not use any defined symbol
  • the logical primitives are the customary four logical connectives and the two quantifier symbols
  • the language is MONO-SORTED FIRST order logic with the extra-logical primitives of identity and membership
  • the axioms are the first 5 axioms of that theory and the identity axioms and the logical axioms

In other words we are looking for that equivalence in the hereditarily finite sector of mono-sorted first order Morse-Kelley $\text{MK}$ class theory.

For instance, the following formula contains only 8 occurrences of atomic sub-formulas and may be optimal:

A class $a$ is finite if and only if:

\begin{align} \forall k [&\exists m (m \in k)\\ &\land \forall x \forall y (x \in a \lor y \in k \to \forall z (\forall n (n \in z \to n=x \lor n \in y ) \to z \in k)) \\ & \to a \in k] \end{align}

After-note: now that Matt F. had written the following formula which is SHORTER than the above formula for finiteness, then the question would be whether there is a shorter formula of finiteness than that?

$$\neg\exists y (\exists z (z \in y) \mathbin\& \forall a (a \in y \to \exists b (b \in y \mathbin\& b \neq a \mathbin\& \forall c (c \in a \to c \in b\mathbin\& c \in x))))$$

An even shorter formula comporized of only 6 atomic formulas had been presented by Emil Jeřábek, that is:

$$\neg\exists y\,(x\in y\land\forall a\in y\,\exists b\in y\,b\subsetneq a)$$ where $b\subsetneq a$ expands to: $b\ne a\land\forall c\,(c\in b\to c\in a)$.

Improve this question
$\endgroup$
21
  • 5
    $\begingroup$ In general, we cannot usually prove directly that a given formula is the shortest to provably have a certain property, since if your underlying theory is inconsistent, then any formula is provably equivalent to finiteness. So a solution here will need to make consistency assumptions. $\endgroup$
    – Joel David Hamkins
    Commented May 7, 2018 at 18:41
  • 5
    $\begingroup$ A search for minimal examples is common in research mathematics, eg the latest Polymath project. Harvey Friedman asks questions like this about set theory too; it is not everyone’s taste in research mathematics, but I think it clearly qualifies. $\endgroup$
    – user44143
    Commented May 7, 2018 at 20:19
  • 3
    $\begingroup$ @MonroeEskew, see Friedman at papers.ssrn.com/sol3/papers.cfm?abstract_id=3158348 on short formulas of set theory. E.g.: He proves that all 3-quantifier sentences are settled by ZF. He conjectures that all 4-quantifier sentences are settled by ZF. But (details at citeseerx.ist.psu.edu/viewdoc/…) there is an independent 5-quantifier sentence, equivalent to the existence of a subtle cardinal. $\endgroup$
    – user44143
    Commented May 9, 2018 at 12:51
  • 6
    $\begingroup$ 6 atomic formulas suffice: $\neg\exists y\,(x\in y\land\forall a\in y\,\exists b\in y\,b\subsetneq a)$, where $b\subsetneq a$ expands to $b\ne a\land\forall c\,(c\in b\to c\in a)$. $\endgroup$
    – Emil Jeřábek
    Commented May 10, 2018 at 13:53
  • 5
    $\begingroup$ I would also vote to reopen, were the question formulated for some standard set theory rather than an ad hoc system. $\endgroup$
    – Emil Jeřábek
    Commented May 10, 2018 at 13:57

0

Reset to default

Browse other questions tagged .