Minimal axiom system for a set of provable statements

Question

I am not a mathematician, so forgive me if this question is trivial. The basic idea of my question is: For a given set of provable statements, can we find an axiom system with the smallest number of true statements (smallest by inclusion)? So here we go with my question.

Suppose we have a set of axioms A and a logic system L that we use to prove theorems arising from A. Let P(A) be the set of provable statements from A using L. Let S be the set of all other sets axiom systems B for which P(A) is a subset of P(B).

Now for any axiom system B in S, let T(B) be the set of all true statements arising from B and L. Partially order the set of axioms in S such that for B1, B2 in S, B1 < B2 if T(B1) is a subset of T(B2).

Question: Does there exist an axiom system M in S such that M < B for all B in S?

Answer 1

Andrew's correct, but there is something similar which is a serious research area -- it's called reverse mathematics. The thing is, most basic theorems of mathematics can be formulated and proved in second-order arithmetic (which is kind of like the Peano axioms on hypersteroids -- you get to quantify over sets, which gives you lots of extra room to work). But a lot of the stuff that people care about in practice doesn't need the full power of second-order arithmetic. Reverse mathematics tries to find the largest "fragments" that you need to prove these sorts of things.

Answer 2

This question certainly makes sense to ask, and the answer is no, because of how flexible the definition of "logical system" is.

First, your definition of B1 < B2 can be simplified: "T(B1) is a subset of T(B2)" is equivalent to "B2 proves B1".

Now, suppose we form a logical system whose only statement symbols are x_n, where n can be an integer, and (countably many) rules of inference stating that x_m implies x_n when m > n. If A is the set of axioms {x₁,x₂,x₃...}, then there is no minimal set of axioms implying A (and P(A)). This is because a set of axioms B will imply A if and only if it contains a sequence of axioms with subscripts approaching infinity, in which case we can always remove finitely many axioms from B so that it still implies A.

(FYI, systems with infinitely many axioms and/or rules of inference are typical of modern mathematics; ZFC, the most commonly accepted foundation, is itself not finitely axiomatizable.)