Skip to main content
minor edit
Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders: $$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any coatom in the Lindenbaum–Tarski algebra of aan incomplete theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders: $$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any coatom in the Lindenbaum–Tarski algebra of a theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders: $$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any coatom in the Lindenbaum–Tarski algebra of an incomplete theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.

small corrections; added 3 characters in body
Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders: $$\forall x \lnot (x \lt x),$$$$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any atomcoatom in the Lindenbaum–Tarski algebra of a theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of dense linear orders: $$\forall x \lnot (x \lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any atom in the Lindenbaum–Tarski algebra of a theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of (nontrivial) dense linear orders: $$\exists x \exists y (x \lt y), \qquad \forall x (x \not\lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any coatom in the Lindenbaum–Tarski algebra of a theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.

Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

Here is a classical example of a theory that has minimal unprovable statements. Let $T$ be the theory of dense linear orders: $$\forall x \lnot (x \lt x),$$ $$\forall x \forall y(x \neq y \to x \lt y \lor y \lt x),$$ $$\forall x \forall y \forall z (x \lt y \land y \lt z \to x \lt z),$$ $$\forall x \forall y (x \lt y \to \exists z(x \lt z \land z \lt y)).$$ It is well known that $T$ has four completions obtained by adding any one of the four axioms $\min \land \max$, $\min \land \lnot\max$, $\lnot\min \land \max$, $\lnot \min \land \lnot \max$, where $\min$ is $$\exists x \forall y (x = y \lor x \lt y)$$ and $\max$ is $$\exists x \forall y (x = y \lor y \lt x).$$ These four sentences are maximally unprovable statements over $T$ and therefore their negations are all minimally unprovable. In other words, $\min \lor \max$, $\min \lor \lnot\max$, $\lnot\min \lor \max$, $\lnot \min \lor \lnot \max$ are all minimally unprovable sentences over $T$.

In general, any atom in the Lindenbaum–Tarski algebra of a theory will be a minimally unprovable statement for that theory. Many common theories (including PA and ZFC) have atomless Lindenbaum–Tarski algebras.