1
$\begingroup$

If we measure the length of a sentence by the number of occurrences of atomic subformulas in it. So, for example in set theory written in $\sf FOL(\in)$, the length of a sentence is the number of occurrences of $x_i \in y_j$ subformulas of it plus adjustments for negation. We can add other qualification that all occurrences of the same variable must be bound by the same quantifier. Now, it is obvious that $\sf ZFC$ is complete for sentences of length 1. Since, those with their truth values are:

$\forall x \forall y \ (x \in y) \ \ \bot \\ \exists x \exists y \, (x \in y) \ \ \top \\ \forall x \exists y \, (x \in y) \ \ \top \\ \forall x \exists y \, (y \in x) \ \ \bot \\ \exists x \forall y \, (x \in y) \ \ \bot \\ \exists x \forall y \, (y \in x) \ \ \bot$

Lets consider the $\neg$ symbol to add the value of $0.5$ to the length criterion. So, the negation of the above sentences would be of $1.5$ length.

Now clearly all of those are decidable by $\sf ZFC$.

Now if we assume the consistency of $\sf ZFC$, then can we know?

What is the minimal length of an undecidable sentences by $\sf ZFC$-$\sf Infinity$+$\text{all sets are finite}$.

What is the minimal length of undecidable sentences by $\sf ZFC$?

What is the minimal length of undecidable sentences by $\sf ZFC + V=L$?

What is the minimal length of undecidable sentences by $\sf ZFC + GCH + V=HOD$?

Improve this question
$\endgroup$
7
  • $\begingroup$ If you had asked about ZF, we could use AC, which is fairly short, for an upper bound. See mathoverflow.net/a/178808/1946. But in general, the sentences known to be independent will be very long when written in the base language (and this is rarely done if ever), and so I don't expect that we shall get the optimal answers for any of these questions. $\endgroup$
    – Joel David Hamkins
    Commented Jun 30 at 12:30
  • 1
    $\begingroup$ There's probably an equivalent of "there exists an inaccessible cardinal" that isn't too long, which gives an upper bound for all of the theories with Infinity. Although I have no idea what the shortest way to phrase that actually is. (It would presumably depend on exactly what language for FOL we're using, given the rule about counting negations, and the fact that subformulas can get duplicated when converting between different sets of connectives, like $\varphi \leftrightarrow \psi$ becoming $(\varphi \to \psi) \land (\psi \to \varphi)$). $\endgroup$
    – paste bee
    Commented Jun 30 at 13:10
  • 1
    $\begingroup$ This feels like it's going to be difficult for the same reason that computing the Busy Beaver function is difficult. And given that we don't even know BB(5), getting far enough through an exhaustive analysis of all statements (because what else can you do to answer a question like this?) to reach a statement complicated enough to be independent is probably not going to happen. If we did try, we would presumably get stuck far earlier on some statement for which we can't tell if it's a theorem or not. $\endgroup$
    – paste bee
    Commented Jun 30 at 13:16
  • $\begingroup$ @pastebee, the connective are only the four usual ones. $\leftrightarrow$ must be broken down. I thought one can solve such a question in ways other than by brute force exhaustive analysis, since this is hard to do. $\endgroup$
    – Zuhair Al-Johar
    Commented Jun 30 at 14:00
  • 2
    $\begingroup$ But doesn't insisting on that treatment of $\leftrightarrow$ only underline that this will not be a genuine mathematical phenomenon, but one dependent on what otherwise are irrelevant distinctions of formalism? The BB function has a similar problem, since the exact values depend on whether one uses one tape or many, 2 symbols or more, etc. For this reason, knowing exact values of BB(k) for particular $k$, or the smallest etc., are not interesting. What matters are the metamathematical features one can prove in general, regardless of the formalism. $\endgroup$
    – Joel David Hamkins
    Commented Jun 30 at 17:22

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .