Next:Definition of functions on Up:User's manual of the Previous:Usual definitions on binary Contents

Subsections

Properties of basic operations and predicates on the booleans.

Basic definitions.

To define the booleans, we extend the language with two contant symbols TT and FF. Then the booleans are defined by the following predicate I B x:

$\begin{definition}[ Booleans ]\hspace{1cm} \begin{itemize} \item % \afdmath{}\hb... ...h{} \SaveVerb{Verb}B x\marginpar{\UseVerb{Verb}} \end{itemize}\end{definition}$

The introduction rules for I B.

$\begin{fact}[ % \afdmath{}\top\endafdmath{} and % \afdmath{}\bot\endafdmath{} ar... ...eak{0.2em}{2.em} \bot\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{fact}$

True.total.B added as introduction rule (abbrev: True , options: -i -c )

False.total.B added as introduction rule (abbrev: False , options: -i -c )

$\begin{fact}[% \afdmath{}\text{\rm is}\_\text{\rm True}.\text{\rm total}.\text{\... ...em} \text{\it b}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

is_True.total.B added as introduction rule (abbrev: is_True , options: )

$\begin{fact}[% \afdmath{}\text{\rm is}\_\text{\rm False}.\text{\rm total}.\text{... ...2em}{2.em} \text{\it b}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

is_False.total.B added as introduction rule (abbrev: is_False , options: )

Elimination rules for I B.

$\begin{fact}[% \afdmath{}\text{\rm case}.\text{\rm B}\endafdmath{}]Case analysis... ...em} \text{\it b}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

case.B added as elimination rule (abbrev: case , options: )

These theorems are added respectively as introduction and elimination rules for the predicate I B with the given abbreviation (This implies for instance that elim True.total.B is equivalent to intro True). Moreover the last rule is invertible and the third rule is not necessary for completeness.

Left rules for I B.

$\begin{proposition}[% \afdmath{}\text{\rm True}\_\text{\rm not}\_\text{\rm False... ... \prettybox{}\bot\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{fact}[% \afdmath{}\text{\rm True}\_\text{\rm not}\_\text{\rm False}\_\tex... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

True_not_False_left.B added as elimination rule (abbrev: True_not_False , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm False}\_\text{\rm not}\_\text{\rm True}\_\tex... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

False_not_True_left.B added as elimination rule (abbrev: False_not_True , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm equal}\_\text{\rm True}\_\text{\rm left}.\tex... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

equal_True_left.B added as elimination rule (abbrev: equal_True_left , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm True}\_\text{\rm equal}\_\text{\rm left}.\tex... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

True_equal_left.B added as elimination rule (abbrev: left_True , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm equal}\_\text{\rm False}\_\text{\rm left}.\te... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

equal_False_left.B added as elimination rule (abbrev: equal_False_left , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm False}\_\text{\rm equal}\_\text{\rm left}.\te... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

False_equal_left.B added as elimination rule (abbrev: left_False , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm elim}.\text{\rm B}\endafdmath{}]Left rule for... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

elim.B added as elimination rule (abbrev: elim , options: -n )

$\begin{theorem}[% \afdmath{}\text{\rm B}\_\text{\rm is}\_\text{\rm excluded}\_\t... ...endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{theorem}$

Boolean equality.

Using the previous axiom, we can prove (instuitionistically) the decidability of the equality on booleans.

$\begin{fact}[% \afdmath{}\text{\rm eq}\_\text{\rm dec}.\text{\rm B}\endafdmath{}... ...}{2.em} \hbox{{\rm I\hspace{-0.2em}B}}\endprettybox{}\endafdmmath{} \end{fact}$

eq_dec.B added as introduction rule (abbrev: B , options: -i -t )

Next:Definition of functions on Up:User's manual of the Previous:Usual definitions on binary Contents

Christophe Raffalli 2005-03-02