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, AE2_RULE, and AE1_RULE.

Return type

Proof

Returns

A valid proof of '(q&p)' from the single assumption '(p&q)' via the inference rules A_RULE, AE2_RULE, and AE1_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()

Proves N via MP, I0, I1, D, and N_ALTERNATIVE.

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

Proves NA1 via MP, I0, I1, D, N, and AE1.

Return type

Proof

Returns

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

propositions.some_proofs.prove_NA2()

Proves NA2 via MP, I0, I1, D, N, and AE2.

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.