View source for Regular formula

A ''regular formula'' is a formula <math>R</math> such that <math>R\linequiv\wn\oc R</math>.

A formula <math>L</math> is ''co-regular'' if its dual <math>L\orth</math> is regular, that is if <math>L\linequiv\oc\wn L</math>.

== Alternative characterization ==

<math>R</math> is regular if and only if it is [[Sequent calculus#Equivalences|equivalent]] to a formula of the shape <math>\wn P</math> for some [[positive formula]] <math>P</math>.

{{Proof|
If <math>R</math> is regular then <math>R\linequiv\wn\oc R</math> with <math>\oc R</math> positive. If <math>R\linequiv\wn P</math> with <math>P</math> positive then <math>R</math> is regular since <math>P\linequiv\oc P</math>.
}}

== Regular connectives ==

A connective <math>c</math> of arity <math>n</math> is ''regular'' if for any regular formulas <math>R_1</math>,...,<math>R_n</math>, <math>c(R_1,\dots,R_n)</math> is regular.

{{Proposition|title=Regular connectives|
<math>\parr</math>, <math>\bot</math> and <math>\wn\oc</math> define regular connectives.
}}

{{Proof|
If <math>R</math> and <math>S</math> are regular, <math>R\parr S \linequiv \wn\oc R \parr \wn\oc S \linequiv \wn{(\oc R\plus\oc S)}</math> thus it is regular since <math>\oc R\plus\oc S</math> is positive.

<math>\bot\linequiv\wn\zero</math> thus it is regular since <math>\zero</math> is positive.

If <math>R</math> is regular then <math>\wn\oc R</math> is regular, since <math>\wn\oc\wn\oc R\linequiv \wn\oc R</math>.
}}

More generally, <math>\wn\oc A</math> is regular for any formula <math>A</math>.