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

Subsections

# Propositionnal connective.

## Conjunction.

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:  )

## Existential quantifiers.

The next definition is useful to get extra parenthesis.

## Equality.

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

## Classical logic.

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

## Definite description.

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

## Contraposition.

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.

Binary relationsChristophe Raffalli, Paul RoziereEquipe 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