Editing Consistency (section)

===Definition===
*A set of [[Well-formed formula|formulas]] <math>\Phi</math> in first-order logic is '''consistent''' (written <math>\operatorname{Con} \Phi</math>) if there is no formula <math>\varphi</math> such that <math>\Phi \vdash \varphi</math> and <math>\Phi \vdash \lnot\varphi</math>.  Otherwise <math>\Phi</math> is '''inconsistent''' (written <math>\operatorname{Inc}\Phi</math>).
*<math>\Phi</math> is said to be '''simply consistent''' if for no formula <math>\varphi</math> of <math>\Phi</math>, both <math>\varphi</math> and the [[negation]] of <math>\varphi</math> are theorems of <math>\Phi</math>.{{clarify|reason=Assuming that 'provable from' and 'theorem of' is equivalent, there seems to be no difference between 'consistent' and 'simply consistent'. If that is true, both definitions should be joined into a single one. If not, the difference should be made clear.|date=September 2018}}
*<math>\Phi</math> is said to be '''absolutely consistent''' or '''Post consistent''' if at least one formula in the language of <math>\Phi</math> is not a theorem of <math>\Phi</math>.
*<math>\Phi</math> is said to be '''maximally consistent''' if <math>\Phi</math> is consistent and for every formula <math>\varphi</math>, <math>\operatorname{Con} (\Phi \cup \{\varphi\})</math> implies <math>\varphi \in \Phi</math>.
*<math>\Phi</math> is said to '''contain witnesses''' if for every formula of the form <math>\exists x \,\varphi</math> there exists a [[Term (logic)|term]] <math>t</math> such that <math>(\exists x \, \varphi \to \varphi {t \over x}) \in \Phi</math>, where <math>\varphi {t \over x}</math> denotes the [[substitution (logic)|substitution]] of each <math>x</math> in <math>\varphi</math> by a <math>t</math>; see also [[First-order logic]].{{citation needed|date=September 2018}}