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.I0 = [] ==> '(p->p)'

Self implication

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->~(p->q)))', [] ==> '(p->~~p)', [] ==> '((q->p)->((~q->p)->p))', [] ==> '(q->(p->q))', [] ==> '(p->p)', ['p', '(p->q)'] ==> 'q', [] ==> '((~q->~p)->(p->q))', [] ==> '(~p->(p->q))', [] ==> '((p->(q->r))->((p->q)->(p->r)))'})

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({[] ==> '((~q->~p)->(p->q))', [] ==> '((p->(q->r))->((p->q)->(p->r)))', ['p', '(p->q)'] ==> 'q', [] ==> '(q->(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.T = [] ==> 'T'

Truth introduction

propositions.axiomatic_systems.NF = [] ==> '~F'

Negative falsity introduction

propositions.axiomatic_systems.AXIOMATIC_SYSTEM_FULL = frozenset({[] ==> '(p->(~q->~(p->q)))', [] ==> '(p->~~p)', [] ==> '((q->p)->((~q->p)->p))', [] ==> '(q->(p->q))', [] ==> '(~p->~(p&q))', [] ==> '(p->(q->(p&q)))', [] ==> '(~q->~(p&q))', [] ==> '(p->p)', [] ==> '(p->(p|q))', ['p', '(p->q)'] ==> 'q', [] ==> 'T', [] ==> '((~q->~p)->(p->q))', [] ==> '(q->(p|q))', [] ==> '(~p->(p->q))', [] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '~F', [] ==> '(~p->(~q->~(p|q)))'})

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->(q->r))->((p->q)->(p->r)))', [] ==> '((~q->~p)->((~q->p)->q))', ['p', '(p->q)'] ==> 'q', [] ==> '(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)->p)', [] ==> '(q->(p->q))', [] ==> '(p->(q->(p&q)))', [] ==> '(p->(p|q))', ['p', '(p->q)'] ==> 'q', [] ==> '((p&q)->q)', [] ==> '((~q->~p)->(p->q))', [] ==> 'T', [] ==> '(q->(p|q))', [] ==> '((p->(q->r))->((p->q)->(p->r)))', [] ==> '~F', [] ==> '((p->r)->((q->r)->((p|q)->r)))'})

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.