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

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

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

`propositions.axiomatic_systems.``HILBERT_AXIOMATIC_SYSTEM_ALTERNATIVE` = frozenset({[] ==> '((~q->~p)->((~q->p)->q))', [] ==> '(q->(p->q))', ['p', '(p->q)'] ==> 'q', [] ==> '((p->(q->r))->((p->q)->(p->r)))'})

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