Definition
Subformula (Propositional Logic)
The subformulas of a formula
are the formulas out of which is built, included; the set of them is defined recursively over the structure of : Each case adds
to the subformulas of its immediate parts; an atom — likewise the constants , (verum, falsum) — has only itself. Being a subformula is a partial order, whose strict companion is the proper subformula relation. An occurrence of a subformula in is fixed by a propositional formula position; distinct positions may carry the same formula.
Polarity
Definition
Link to originalPolarity (Propositional Logic)
Let
be a propositional formula. The polarity of an occurrence of a subformula in is defined recursively from the root of . We write
for the polarity of the occurrence at position in : An occurrence is called positive, negative, or neutral according as its polarity is
, , or .
Examples
In
the subformulas are
, , and .
In
the subformulas are
, , , and .