Regular formula

From LLWiki
Revision as of 23:01, 28 October 2013 by Olivier Laurent (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

A regular formula is a formula R such that R\linequiv\wn\oc R.

A formula L is co-regular if its dual L\orth is regular, that is if L\linequiv\oc\wn L.

Alternative characterization

R is regular if and only if it is equivalent to a formula of the shape \wn P for some positive formula P.

Proof.  If R is regular then R\linequiv\wn\oc R with \oc R positive. If R\linequiv\wn P with P positive then R is regular since P\linequiv\oc P.

Regular connectives

A connective c of arity n is regular if for any regular formulas R1,...,Rn, c(R_1,\dots,R_n) is regular.

Proposition (Regular connectives)

\parr, \bot and \wn\oc define regular connectives.

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

\bot\linequiv\wn\zero thus it is regular since \zero is positive.

If R is regular then \wn\oc R is regular, since \wn\oc\wn\oc R\linequiv \wn\oc R.

More generally, \wn\oc A is regular for any formula A.

Personal tools