# Is it possible to construct a formal system such that all interesting statements from ZFC can be proven within the system?

I'm familiar with Godel's incompleteness theorem, which very basically states that there exists a statement that can be neither proved or disproved within a formal system powerful enough to include elementary arithmetic, and that a consistent formal system can't be proven to be consistent from within that system.

However, let's say I'm am only interested in being able to prove a certain (finite) set of mathematical statements that are 1) Provable or 2) Neither provable or disprovable in ZFC (Let's call those statements "interesting"). Specifically, the set i choose does not include "all" statements of type 2) in ZFC, just a proper subset.

The question is: for any finite set of interesting statements from ZFC, where the set of statements are consistent, is it possible to construct a new formal system that can prove all interesting statements while keeping the system consistent, if one is allowed to choose the axioms arbitrarily?

Obviously, the system need not be provably consistent.

The intuitive construction is to just take the "not provable or disprovable" statements in ZFC and add them as axioms, but I'm not sure if this is possible in all cases.

There is also a meta-question in case there is no clear answer to the first: Is it possible to answer the first question?

EDIT: added "where the set of statements are consistent"

• What if your finite set of statements is $\{ CH, \lnot CH \}$? Jan 30, 2018 at 1:47
• @DanielSchepler I see your point. Would it suffice to add the restriction to the choice of set that no two elements of the set are contradictory in PL? Jan 30, 2018 at 1:59
• You really need them all to be consistent together, not just pairwise consistent. Jan 30, 2018 at 2:01
• @TobiasBengtsson: No, pairwise compatibility is not enough -- consider for example if your goal statements are $\{\mathfrak c\ne\aleph_1, \mathfrak c\ne\aleph_2,\mathfrak c\in\{\aleph_1,\aleph_2\}\}$. Jan 30, 2018 at 2:02
• @TobiasBengtsson For any $n$ we can find a set of $(n+1)$-many sentences which is inconsistent, such that any $n$-element subset is consistent. Jan 30, 2018 at 2:02

• @TobiasBengtsson I think there might be no specific reference as this is something that "just falls off" when studying this topic. If some statement is independent of your axioms, then just declare it (or its negation) to an axiom $-$ whatever you prefer. This is basically the way by definition. Jan 30, 2018 at 11:44