Artificial intelligent assistant

Independence and Consistence of Formal Systems Let $S$ be a formal system with axioms $A,A_1,\dots,A_n$. The system $S$ is said to be consistent if no contradiction can be proved (i.e. we can’t prove both a formula and its negation). If $S$ is consistent, the axiom $A$ is said to be dependent from $A_1,\dots,A_n$ if $A$ can be proved using only $A_1,\dots,A_n$. Given these definitions, if $S$ and $S'$ are both consistent, with $S’$ created from $S$ by negating $A$ (i.e. the axioms of $S'$ are $\lnot A,A_1, \dots,A_n$), then obviously $A$ is not dependent from $A_1,\dots,A_n$. Does the opposite holds? That is can we prove that if $S$ is consistent ad $S’$ is not consistent then $A$ can be derived from $A_1,\dots,A_n$?

The answer is positive, at least in first-order classical logic (which is the logic you refer to, I guess), where you have completeness and soundness theorems.

_Completeness_ theorem states that if every model of $A_1, \dots, A_n$ is a model of $A$ then $A$ can be derived from $A_1, \dots, A_n$.

_Soundness_ theorem is the converse of completeness, it states that if $A$ can be derived from $A_1, \dots, A_n$ then every model of $A_1, \dots, A_n$ is a model of $A$.

If $S' = \\{A_1, \dots, A_n, \lnot A\\}$ is not consistent then $S'$ is not satisfiable i.e. there is no model satisfying $A_1, \dots, A_n, \lnot A$ (because by soundness theorem, if there were such a model, it would satisfy a contradiction, that is impossible). So, every model of $A_1, \dots, A_n$ cannot be a model of $\lnot A$ and hence it is a model of $A$. Therefore, $A$ is derivable from $A_1, \dots, A_n$ by completeness theorem.

Note that the hypothesis that $S$ is consistent is superfluous.

xcX3v84RxoQ-4GxG32940ukFUIEgYdPy 69a799a8f6f3f2dfb7980f619d66f385