Editing Paraconsistent logic (section)

=== Included ===
Some tautologies of paraconsistent logic are:
* All axiom schemas for paraconsistent logic:
:<math>P \to (Q \to P)</math> ** for deduction theorem and ?→{''t'',''b''} = {''t'',''b''}
:<math>(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))</math> ** for deduction theorem (note: {''t'',''b''}→{''f''} = {''f''} follows from the deduction theorem)
:<math>\lnot (P \to Q) \to P</math> ** {''f''}→? = {''t''}
:<math>\lnot (P \to Q) \to \lnot Q</math> ** ?→{''t''} = {''t''}
:<math>P \to (\lnot Q \to \lnot (P \to Q))</math> ** {''t'',''b''}→{''b'',''f''} = {''b'',''f''}
:<math>\lnot \lnot P \to P</math> ** ~{''f''} = {''t''}
:<math>P \to \lnot \lnot P</math> ** ~{''t'',''b''} = {''b'',''f''} (note: ~{''t''} = {''f''} and ~{''b'',''f''} = {''t'',''b''} follow from the way the truth-values are encoded)
:<math>P \to (P \lor Q)</math> ** {''t'',''b''}v? = {''t'',''b''}
:<math>Q \to (P \lor Q)</math> ** ?v{''t'',''b''} = {''t'',''b''}
:<math>\lnot (P \lor Q) \to \lnot P</math> ** {''t''}v? = {''t''}
:<math>\lnot (P \lor Q) \to \lnot Q</math> ** ?v{''t''} = {''t''}
:<math>(P \to R) \to ((Q \to R) \to ((P \lor Q) \to R))</math> ** {''f''}v{''f''} = {''f''}
:<math>\lnot P \to (\lnot Q \to \lnot (P \lor Q))</math> ** {''b'',''f''}v{''b'',''f''} = {''b'',''f''}
:<math>(P \land Q) \to P</math> ** {''f''}&? = {''f''}
:<math>(P \land Q) \to Q</math> ** ?&{''f''} = {''f''}
:<math>\lnot P \to \lnot (P \land Q)</math> ** {''b'',''f''}&? = {''b''.''f''}
:<math>\lnot Q \to \lnot (P \land Q)</math> ** ?&{''b'',''f''} = {''b'',''f''}
:<math>(\lnot P \to R) \to ((\lnot Q \to R) \to (\lnot (P \land Q) \to R))</math> ** {''t''}&{''t''} = {''t''}
:<math>P \to (Q \to (P \land Q))</math> ** {''t'',''b''}&{''t'',''b''} = {''t'',''b''}
:<math>(P \to Q) \to ((\lnot P \to Q) \to Q)</math> ** ? is the union of {''t'',''b''} with {''b'',''f''}
* Some other theorem schemas:
:<math>P \to P</math>
:<math>(\lnot P \to P) \to P</math>
:<math>((P \to Q) \to P) \to P</math>
:<math>P \lor \lnot P</math>
:<math>\lnot (P \land \lnot P)</math>
:<math>(\lnot P \to Q) \to (P \lor Q)</math>
:<math>((\lnot P \to Q) \to Q) \to (((P \land \lnot P) \to Q) \to (P \to Q))</math> ** every truth-value is either ''t'', ''b'', or ''f''.
:<math>((P \to Q) \to R) \to (Q \to R)</math>