How to find a minimum set of axioms within a set of propositions?

I have a set of propositions, for example $\{a_1,a_2,\dots,a_n\}$. Some propositions depend on others (for example, $a_1,a_2\Rightarrow a_3$, means if $a_1,a_2$ are true, then $a_3$ is true). I want to find a subset of the propositions to be defined as axioms, in the sense that, these propositions being true imply that all the others are true. The number of axioms should be as small as possible. I want to know whether there are some methods?

• These are called functional dependencies in database theory and a set of minimal axioms is called a candidate key Commented Dec 22, 2015 at 7:34
• maybe a more useful reference is the wiki article about candidate keys. Commented Dec 22, 2015 at 8:11
• Do you know anything about the set of propositions? If they come from arbitrary propositional logic, then I suspect there's no better algorithm than trying all possible subsets. On the other hand if they come from some restricted set of propositions (e.g., Horn clauses or something like that), then maybe there's some room for more sophisticated algorithms.
– D.W.
Commented Dec 22, 2015 at 19:52
• (at least the plural of basis is correct now) An algorithm to find a basis (a minimal set but not necessarily the smallest that generates all propositions) is rather simple (see wiki candidate keys). The problem to decide if there is a basis with the number of elements smaller then a given number seems to be NP hard. An algorithm that calculates all bases that is polynomial in the number of different bases and the number of propositions can be found in the wiki entry for the candidate key. But the number of bases may be large so this algorithm is not polynomial in the number of propositions. Commented Dec 22, 2015 at 22:48

Determining whether a proposition follows from a set of axioms is an NP-Complete problem. Finding a minimal set of axioms from a set of propositions naturally invokes this problem many times as a subroutine.

For example, consider the following set of propositions:

$$P = \{v_1, v_3 \vee v_2, v_1 \wedge v_3\}$$

A minimum set of axioms from this set is $\{v_1 \wedge v_3\}$. But to find it, you have to prove $v_1$ and $v_3\vee v_2$, and those proofs are in general hard to find. The problem is there a set of axioms $A$ for a set of propositions $P$ with at most $k$ axioms? is in $\Sigma_{3}^{p}$, which means it's in the third level of the polynomial hierarchy, which means that it's two levels higher than NP in the way that NP is one level higher than P, to give you an idea of its complexity. I do not know if it is also in a lower level. Browsing through this survey (link) [1] of problems that are complete for various levels of the polynomial hierarchy, I do not see this problem among them, so it's possible that it's not $\Sigma_{3}^{p}$-Complete, but it wouldn't surprise me.

Before you go out to look for a set of axioms, you may want to know whether the set of propositions is sound and any subset is complete (untrue propositions cannot be proved, all true propositions can be proved). These problems have similar NP-scary complexity. First, Is this set of propositions complete? is a problem in $\Pi_{2}^{p}$ of the polynomial hierarchy, because it asks, for all $p\in P$, can $p$ be proved from propositions $P\setminus \{p\}$? Completeness of your system is in co-NP as it asks, Forall all $p\in P$, can $p$ not be proved from $P \setminus \{p\}$? So it seems that checking for soundness and completeness is easier than finding a minimal axiom set, but not by much. (I'm less sure about this paragraph. Is it true that a logical system of propositions $P$ is sound iff for all $p\in P\colon \neg p$ cannot be proved from $P\setminus \{p\}$?)

The comments to your question pertain to the context of database entries, but they are purely syntactic and only establish redundancy in the database, whereas if your question is about propositions, as I understand it, then the contents of the database must be inspected semantically, and this leads you to this complexity nightmare.

[1] M. Schaefer, C. Umans, Completenss in the Polynomial Hierarchy, A Compendium, 2008.