# propositions.some_proofs module¶

Some proofs in Propositional Logic.

`propositions.some_proofs.``A_RULE` = ['x', 'y'] ==> '(x&y)'

Conjunction introduction inference rule

`propositions.some_proofs.``AE1_RULE` = ['(x&y)'] ==> 'y'

Conjunction elimination (right) inference rule

`propositions.some_proofs.``AE2_RULE` = ['(x&y)'] ==> 'x'

Conjunction elimination (left) inference rule

`propositions.some_proofs.``prove_and_commutativity`()

Proves `'(q&p)'` from `'(p&q)'` via `A_RULE`, `AE1_RULE`, and `AE2_RULE`.

Return type

`Proof`

Returns

A valid proof of `'(q&p)'` from the single assumption `'(p&q)'` via the inference rules `A_RULE`, `AE1_RULE`, and `AE2_RULE`.

`propositions.some_proofs.``prove_I0`()

Proves `I0` via `MP`, `I1`, and `D`.

Return type

`Proof`

Returns

A valid proof of `I0` via the inference rules `MP`, `I1`, and `D`.

`propositions.some_proofs.``HS` = ['(p->q)', '(q->r)'] ==> '(p->r)'

Hypothetical syllogism

`propositions.some_proofs.``prove_hypothetical_syllogism`()

Proves `HS` via `MP`, `I0`, `I1`, and `D`.

Return type

`Proof`

Returns

A valid proof of `HS` via the inference rules `MP`, `I0`, `I1`, and `D`.

`propositions.some_proofs.``prove_I2`()

Proves `I2` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `I2` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``_NNE` = [] ==> '(~~p->p)'

Double-negation elimination

`propositions.some_proofs.``_prove_NNE`()

Proves `_NNE` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `_NNE` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``prove_NN`()

Proves `NN` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `NN` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``_CP` = [] ==> '((p->q)->(~q->~p))'

Contraposition

`propositions.some_proofs.``_prove_CP`()

Proves `_CP` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `_CP` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``prove_NI`()

Proves `NI` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `NI` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``_CM` = ['(~p->p)'] ==> 'p'

Consequentia mirabilis

`propositions.some_proofs.``_prove_CM`()

Proves `_CM` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `_CM` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``prove_R`()

Proves `R` via `MP`, `I0`, `I1`, `D`, and `N`.

Return type

`Proof`

Returns

A valid proof of `R` via the inference rules `MP`, `I0`, `I1`, `D`, and `N`.

`propositions.some_proofs.``prove_N`()
Return type

`Proof`

Returns

A valid proof of `N` via the inference rules `MP`, `I0`, `I1`, `D`, and `N_ALTERNATIVE`.

`propositions.some_proofs.``prove_NA1`()
Return type

`Proof`

Returns

A valid proof of `NA1` via the inference rules `MP`, `I0`, `I1`, `D`, and `AE1`.

`propositions.some_proofs.``prove_NA2`()
Return type

`Proof`

Returns

A valid proof of `NA2` via the inference rules `MP`, `I0`, `I1`, `D`, and `AE2`.

`propositions.some_proofs.``prove_NO`()

Proves `NO` via `MP`, `I0`, `I1`, `D`, `N`, and `OE`.

Return type

`Proof`

Returns

A valid proof of `NO` via the inference rules `MP`, `I0`, `I1`, `D`, and `OE`.