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

136 Views Asked by At

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"

1

There are 1 best solutions below

2
On BEST ANSWER

You can indeed just declare all of your "interesting" statements to be axioms.

If your interesting statements conflict with each other, such as if you think both the continuum hypothesis and its negation are interesting (as suggested by @Daniel Schepler), then the result will of course be inconsistent -- but that happens if and only if there is no consistent theory that will prove all of your "interesting" statements.

So declaring your goals to be axioms is an universal solution to constructing a theory with a given finite set of desired consequences.