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

Subsections

Propositionnal connective.

Conjunction.

$\begin{definition}[ Conjunction. ]~ \begin{center}% \afdmath{}\text{\it X}\hspac... ...h{} \SaveVerb{Verb}X & Y\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[ Conjunction rules. ]\hspace{1cm} \begin{itemize} \item % \a... ...{\it X}\right)\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{proposition}$

conjunction.left added as elimination rule (abbrev: s , options: -n -i )

conjunction.left.elim added as elimination rule (abbrev: l , options: )

conjunction.right.elim added as elimination rule (abbrev: r , options: )

$\begin{definition}[ Equivalence. ]~ \begin{center}% \afdmath{}\text{\it X}\hspac... ...} \SaveVerb{Verb}X <-> Y\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Disjunction.

$\begin{definition}[ Disjunction. ]~ \begin{center}% \afdmath{}\text{\it X}\hspac... ...{} \SaveVerb{Verb}X or Y\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[ Disjunction rules. ]\hspace{1cm} \begin{itemize} \item % \a... ...le (abbrev: \verb ...$

Propositional constants and negation.

$\begin{definition}[ Propositional constants and negation. ]\hspace{1cm} \begin{i... ...h{} \SaveVerb{Verb}~ X\marginpar{\UseVerb{Verb}} \end{itemize}\end{definition}$

$\begin{proposition}[ Propositional constants and negation rules. ]\hspace{1cm} \... ...{\it Y}\right)\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{proposition}$

Existential quantifiers.

$\begin{definition}[ Existential quantifiers definitions. ]\hspace{1cm} \begin{it... ...SaveVerb{Verb}\/!x A x\marginpar{\UseVerb{Verb}} \end{itemize}\end{definition}$

$\begin{proposition}[ Existential rules ]\hspace{1cm} \begin{itemize} \item % \af... ...le (abbrev: \verb ...$

$\begin{definition}[ The arrow type ]~ \begin{center}% \afdmath{}\text{\it E}\hsp... ...{} \SaveVerb{Verb}E => D\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

The next definition is useful to get extra parenthesis.

$\begin{definition}[]~ \begin{center}% \afdmath{}\left( \text{\it e}\right)\hspac... ...} \SaveVerb{Verb}{{ e }}\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Equality.

$\begin{axiom}[% \afdmath{}\text{\rm equal}.\text{\rm proposition}\endafdmath{}]~... ...m} \text{\it Y}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{axiom}$

equal.proposition added as introduction rule (abbrev: prop , options: )

$\begin{axiom}[% \afdmath{}\text{\rm equal}.\text{\rm extensional}\endafdmath{}]~... ...m} \text{\it Y}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{axiom}$

$\begin{proposition}[% \afdmath{}\text{\rm equal}.\text{\rm symmetric}\endafdmath... ...ext{\it x}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm equal}.\text{\rm transitive}\endafdmat... ...ext{\it z}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\it x}\hspace{0.3em}\neq\h... ...{} \SaveVerb{Verb}x != y\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[% \afdmath{}\text{\rm not}\_\text{\rm equal}\_\text{\rm refl... ...ext{\it x}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm equal}.\text{\rm decid... ...b{Verb}equal.decidable P\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

Some tautologies.

$\begin{proposition}[% \afdmath{}\text{\rm int}\_\text{\rm contraposition}\_\text... ... X}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm int}\_\text{\rm contraposition}\endafd... ...ext{\it A}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm equivalence}.\text{\rm int}\_\text{\rm... ... B}\endprettybox{}\right)\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm equivalence}.\text{\rm reflexive}\enda... ...37em}{2.em} \text{\it A}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm equivalence}.\text{\rm symmetrical}\en... ....em} \text{\it A}\right)\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm equivalence}.\text{\rm transitive}\end... ....em} \text{\it C}\right)\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm disjunction}.\text{\rm reflexive}\enda... ...37em}{2.em} \text{\it A}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm disjunction}.\text{\rm symmetrical}\en... ...36em}{2.em} \text{\it A}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm disjunction}.\text{\rm associative}\en... ...36em}{2.em} \text{\it C}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm conjunction}.\text{\rm reflexive}\enda... ...37em}{2.em} \text{\it A}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm conjunction}.\text{\rm symmetrical}\en... ...ext{\it A}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm conjunction}.\text{\rm associative}\en... ...ext{\it C}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm disj}\_\text{\rm conj}.\text{\rm distr... ... C}\right)\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm conj}\_\text{\rm disj}.\text{\rm distr... ...ext{\it C}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

Classical logic.

$\begin{axiom}[% \afdmath{}\text{\rm peirce}\_\text{\rm law}\endafdmath{}]~ \afdm... ...eak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{axiom}$

If you want to do intuitionnistic logic only, do not use this axiom ! You can always use the command depend to see if a theorem uses the Peirce's law

$\begin{proposition}[% \afdmath{}\text{\rm not}\_\text{\rm idempotent}\endafdmath... ...36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm absurd}\endafdmath{}]~ \afdmmath{}\pre... ...36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm contradiction}\endafdmath{}]~ \afdmmat... ...36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm excluded}\_\text{\rm middle}\endafdmat... ...ext{\it X}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

Definite description.

$\begin{constant}[]~ \begin{center}% \afdmath{}\Delta\endafdmath{} : ( 'a $\right... ...ow$\ 'a \SaveVerb{Verb}Def\marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

$\begin{axiom}[% \afdmath{}\text{\rm Def}.\text{\rm axiom}\endafdmath{}]definite ... ...\endprettybox{}}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{axiom}$

Def.axiom added as introduction rule (abbrev: Def , options: -o 10.0 -t )

$\begin{proposition}[% \afdmath{}\text{\rm Def}.\text{\rm lemma}\endafdmath{}]~ \... ...rettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

Contraposition.

$\begin{proposition}[% \afdmath{}\text{\rm contraposition}\endafdmath{}]~ \afdmma... ...ext{\it B}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm equivalence}.\text{\rm contraposition}... ...ext{\it B}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{definition}[]~ \begin{center}List of theorems: contrapose := contraposition equivalence.contraposition \end{center}\end{definition}$

For reasoning by contraposition (classical reasoning) you can use: "rewrite -p 0 -r contrapose." For the intuitionnistic instance of reasoning by contraposition: rewrite contrapose.

De Morgan Laws.

$\begin{proposition}[% \afdmath{}\text{\rm conjunction}.\text{\rm demorgan}\endaf... ...rettybox{}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm conjarrowleft}.\text{\rm demorgan}\end... ...rettybox{}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm conjarrowright}.\text{\rm demorgan}\en... ...rettybox{}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm disjunction}.\text{\rm demorgan}\endaf... ...rettybox{}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm arrow}.\text{\rm demorgan}\endafdmath{... ...rettybox{}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm negation}.\text{\rm demorgan}\endafdma... ...em} \text{\it X}\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm forall}.\text{\rm demorgan}\endafdmath... ...{}\endprettybox{}\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm exists}.\text{\rm demorgan}\endafdmath... ...{}\endprettybox{}\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{definition}[]~ \begin{center}List of theorems: demorgan := disjunction.de... ...s.demorgan conjunction.demorgan negation.demorgan \end{center}\end{definition}$

$\begin{definition}[]~ \begin{center}List of theorems: demorganl := disjunction.d... ...demorgan conjarrowleft.demorgan negation.demorgan \end{center}\end{definition}$

$\begin{definition}[]~ \begin{center}List of theorems: demorganr := disjunction.d... ...emorgan conjarrowright.demorgan negation.demorgan \end{center}\end{definition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}{\mathop{\text{\rm Let}}}\hspace... ...Verb}Let x = e inside e'\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[% \afdmath{}\text{\rm and}\_\text{\rm arrow}\endafdmath{}]~ ... ...36em}{2.em} \text{\it Z}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm exists}\_\text{\rm arrow}\endafdmath{}... ...ext{\it Z}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

Binary relations Christophe Raffalli, Paul Roziere Equipe de Logique, Université Chambéry, Paris VII

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

Christophe Raffalli 2005-03-02