propositions.axiomatic_systems module¶

Axiomatic inference rules of propositional logic.

propositions.axiomatic_systems.MP = ['p', '(p->q)'] ==> 'q'¶: Modus ponens / implication elimination

propositions.axiomatic_systems.I1 = [] ==> '(q->(p->q))'¶: Implication introduction (right)

propositions.axiomatic_systems.D = [] ==> '((p->(q->r))->((p->q)->(p->r)))'¶: Self-distribution of implication

propositions.axiomatic_systems.I2 = [] ==> '(~p->(p->q))'¶: Implication introduction (left)

propositions.axiomatic_systems.N = [] ==> '((~q->~p)->(p->q))'¶: Converse contraposition

propositions.axiomatic_systems.NI = [] ==> '(p->(~q->~(p->q)))'¶: Negative-implication introduction

propositions.axiomatic_systems.NN = [] ==> '(p->~~p)'¶: Double-negation introduction

propositions.axiomatic_systems.R = [] ==> '((q->p)->((~q->p)->p))'¶: Resolution

propositions.axiomatic_systems.AXIOMATIC_SYSTEM = frozenset({[] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '(p->~~p)', [] ==> '((~q->~p)->(p->q))', ['p', '(p->q)'] ==> 'q', [] ==> '(p->(~q->~(p->q)))', [] ==> '(~p->(p->q))', [] ==> '((q->p)->((~q->p)->p))', [] ==> '(q->(p->q))', [] ==> '(p->p)'})¶: Large axiomatic system for implication and negation, consisting of MP, I0, I1, D, I2, N, NI, NN, and R.

propositions.axiomatic_systems.HILBERT_AXIOMATIC_SYSTEM = frozenset({['p', '(p->q)'] ==> 'q', [] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '(q->(p->q))', [] ==> '((~q->~p)->(p->q))'})¶: Hilbert axiomatic system for implication and negation, consisting of MP, I1, D, and N.

propositions.axiomatic_systems.A = [] ==> '(p->(q->(p&q)))'¶: Conjunction introduction

propositions.axiomatic_systems.NA1 = [] ==> '(~q->~(p&q))'¶: Negative-conjunction introduction (right)

propositions.axiomatic_systems.NA2 = [] ==> '(~p->~(p&q))'¶: Negative-conjunction introduction (left)

propositions.axiomatic_systems.NF = [] ==> '~F'¶: Negative-falsity introduction

propositions.axiomatic_systems.AXIOMATIC_SYSTEM_FULL = frozenset({[] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '(~q->~(p&q))', [] ==> '(~p->~(p&q))', [] ==> '(p->~~p)', [] ==> '(~p->(~q->~(p|q)))', [] ==> '(p->(p|q))', [] ==> '((~q->~p)->(p->q))', [] ==> 'T', ['p', '(p->q)'] ==> 'q', [] ==> '~F', [] ==> '(p->(~q->~(p->q)))', [] ==> '(~p->(p->q))', [] ==> '(p->(q->(p&q)))', [] ==> '((q->p)->((~q->p)->p))', [] ==> '(q->(p->q))', [] ==> '(q->(p|q))', [] ==> '(p->p)'})¶: Large axiomatic system for all operators, consisting of the rules in AXIOMATIC_SYSTEM, as well as A, NA1, NA2, O1, O2, NO, T, and NF.

propositions.axiomatic_systems.N_ALTERNATIVE = [] ==> '((~q->~p)->((~q->p)->q))'¶: Reductio ad absurdum

propositions.axiomatic_systems.HILBERT_AXIOMATIC_SYSTEM_ALTERNATIVE = frozenset({['p', '(p->q)'] ==> 'q', [] ==> '((~q->~p)->((~q->p)->q))', [] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '(q->(p->q))'})¶: Hilbert axiomatic system for implication and negation, with N replaced by N_ALTERNATIVE.

propositions.axiomatic_systems.AE1 = [] ==> '((p&q)->q)'¶: Conjunction elimination (right)

propositions.axiomatic_systems.AE2 = [] ==> '((p&q)->p)'¶: Conjunction elimination (left)

propositions.axiomatic_systems.OE = [] ==> '((p->r)->((q->r)->((p|q)->r)))'¶: Disjunction elimination

propositions.axiomatic_systems.HILBERT_AXIOMATIC_SYSTEM_FULL = frozenset({[] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '((p&q)->p)', [] ==> '(p->(p|q))', [] ==> 'T', ['p', '(p->q)'] ==> 'q', [] ==> '~F', [] ==> '((p&q)->q)', [] ==> '(p->(q->(p&q)))', [] ==> '((p->r)->((q->r)->((p|q)->r)))', [] ==> '(q->(p->q))', [] ==> '(q->(p|q))', [] ==> '((~q->~p)->(p->q))'})¶: Hilbert axiomatic system for all operators, consisting of the rules in HILBERT_AXIOMATIC_SYSTEM, as well as A, AE1, AE2, O1, O2, OE, T, and NF.