# Rule of Commutation

Jump to navigation
Jump to search

This page has been identified as a candidate for refactoring of medium complexity.In particular: extensionUntil this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Theorem

## Conjunction

### Formulation 1

- $p \land q \dashv \vdash q \land p$

### Formulation 2

- $\vdash \paren {p \land q} \iff \paren {q \land p}$

## Disjunction

### Formulation 1

- $p \lor q \dashv \vdash q \lor p$

### Formulation 2

- $\vdash \paren {p \lor q} \iff \paren {q \lor p}$

Its abbreviation in a tableau proof is $\text{Comm}$.

## Also known as

The **rule of commutation** is also known as the **commutative law**.

Note that this term is also used throughout mathematics in the context of addition and multiplication of numbers:

so it is wise to be aware of the context.

## Also see

## Technical Note

When invoking the **Rule of Commutation** in a tableau proof, use the `{{Commutation}}`

template:

`{{Commutation|line|pool|statement|depends|type}}`

where:

`line`

is the number of the line on the tableau proof where Rule of Commutation is to be invoked`pool`

is the pool of assumptions (comma-separated list)`statement`

is the statement of logic that is to be displayed in the**Formula**column,**without**the`$ ... $`

delimiters`depends`

is the line (or lines) of the tableau proof upon which this line directly depends`type`

is the type of Rule of Commutation: specifically`Disjunction`

or`Conjunction`

, whose link will be displayed in the**Notes**column.