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

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.