Axiom Systems¶

Base Classes¶

class logics.classes.propositional.proof_theories.DerivationStep(content, justification, on_steps=None)¶

Step within an axiomatic derivation.

Parameters:

content (logics.classes.propositional.Formula) – The formula present in the step
justification (str) – The name of the rule or axiom used in obtaining this step. May be ‘premise’ as well.
on_steps (list of int) – Steps to which the derivation rule was applied to (may be empty). These are 0-based (first step of the derivation is step 0).

Examples

A derivation step will have the following form

>>> from logics.classes.propositional.proof_theories import DerivationStep
>>> from logics.utils.parsers import classical_parser
>>> s = DerivationStep(content=classical_parser.parse('p or ~q'), justification='mp', on_steps=[0, 2])
>>> s  # note the format in which it prints to the console
['∨', ['p'], ['~', ['q']]]; mp; [0, 2]

Also note that you can parse an entire derivation, which will be comprised of DerivationStep

>>> classical_parser.parse_derivation("p → (p → p); ax1")
>>> deriv = classical_parser.parse_derivation("p → (p → p); ax1")
>>> deriv[0]
['→', ['p'], ['→', ['p'], ['p']]]; ax1; []
>>> type(deriv[0])
<class 'logics.classes.propositional.proof_theories.derivation.DerivationStep'>

See also

logics.utils.parsers.classical_parser

class logics.classes.propositional.proof_theories.Derivation(iterable=(), /)¶

An axiomatic or natural deduction derivation.

Extends list. A derivation is a list of DerivationStep. Each step contains formula, justification, [on_steps]

Examples

>>> from logics.classes.propositional.proof_theories import DerivationStep, Derivation
>>> from logics.classes.propositional import Formula
>>> derivation = Derivation([
...     DerivationStep(Formula(['∧', ['p'], ['q']]), 'premise'),
...     DerivationStep(Formula(['p']), 'E∧', [2])
... ])
>>> derivation
0. ['∧', ['p'], ['q']]; premise; []
1. ['p']; E∧; [2]

would be a derivation of p from p ∧ q, using the rule E∧ ((A ^ B) / A). Note that you can also obtain a Derivation using the parser, e.g.

>>> from logics.utils.parsers import classical_parser
>>> classical_parser.parse_derivation('''
... p ∧ q; premise
... p; E∧; [0]
... ''')
0. ['∧', ['p'], ['q']]; premise; []
1. ['p']; E∧; [0]

Slicing a Derivation also returns a Derivation

>>> derivation[1:]
0. ['p']; E∧; [2]
>>> type(derivation[1:])
<class 'logics.classes.propositional.proof_theories.derivation.Derivation'>

property premises¶: Returns a list of the premises of the derivation (the DerivationStep’s with a justification of ‘premise’)

property conclusion¶: Returns the formula in the last step of the derivation (or None if the derivation is empty)

print_derivation(parser)¶

For even prettier printing of a derivation in the console, you can pass a parser and it will unparse the formula

Examples

>>> from logics.classes.propositional.proof_theories import DerivationStep, Derivation
>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional import Formula
>>> derivation = Derivation([
...     DerivationStep(Formula(['∧', ['p'], ['q']]), 'premise'),
...     DerivationStep(Formula(['p']), 'E∧', [2])
... ])
>>> derivation.print_derivation(classical_parser)
0. (p ∧ q); premise; []
1. p; E∧; [2]

Axiom System¶

class logics.classes.propositional.proof_theories.AxiomSystem(language, axioms, rules)¶

Class for obtaining axiom systems

Parameters:

language (language: logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
axioms (dict (str: logics.classes.propositional.Formula)) – The keys are strings (the name of the axiom) and the values are (schematic) Formula
rules (dict (str: logics.classes.propositional.Inference)) – The keys are strings (the name of the rule) and the values are (schematic) Inference

Examples

Classical propositional logic with only negation and conditional

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import AxiomSystem
>>> from logics.instances.propositional.languages import classical_infinite_language_only_negation_conditional
>>> axioms = {
... 'ax1': classical_parser.parse('A → (B → A)'),
... 'ax2': classical_parser.parse('(A → (B → C)) → ((A → B) → (A → C))'),
... 'ax3': classical_parser.parse('(~A → ~B) → (B → A)')
... }
>>> rules = {'mp': classical_parser.parse('A, A → B / B')}
>>> classical_logic_axiom_system = AxiomSystem(language=classical_infinite_language_only_negation_conditional,
...                                            axioms=axioms, rules=rules)

This particular instance is also predefined in the instances module

>>> from logics.instances.propositional.axiom_systems import classical_logic_axiom_system

is_correct_derivation(derivation, inference=None, return_error_list=False, exit_on_first_error=False)¶

Determines if a derivation has been correctly performed.

Will check that the steps with a justification of ‘premise’ are premises of inference, that every other step is obtained by instantiating an axiom or via the application of a rule to a previous step, and that the last step is the conclusion of inference. For axioms, you may write the specific name of the axiom, or just write down ‘axiom’ and this will check all axioms

Parameters:

derivation (logics.classes.propositional.proof_theories.Derivation) – The derivation the algorithm will look at
inference (logics.classes.propositional.Inference or None) – If None, will just check correct application of the rules. If an inference, will check that the steps labelled as ‘premise’ are premises of the inference, and that the last step is the conclusion of the inference
return_error_list (bool) – If False, will just return True or False (exits when it finds an error, more efficient) If True, will return (True, a list of logics.classes.errors.CorrectionError)
exit_on_first_error (bool, optional) – If return_error_list and this are both true, it will return a list with a single error instead of many. More efficient, since it makes early exits.

Examples

Demostration of / p → p

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.axiom_systems import classical_logic_axiom_system
>>> i = classical_parser.parse('/ p → p')
>>> deriv = classical_parser.parse_derivation('''
... p → ((p → p) → p); ax1
... (p → ((p → p) → p)) → ((p → (p → p)) → (p → p)); ax2
... p → (p → p); ax1
... ((p → (p → p)) → (p → p)); mp; [0,1]
... p → p; mp; [2,3]''')
>>> classical_logic_axiom_system.is_correct_derivation(deriv, i)
True

Using ‘axiom’ instead of the name of the specific axiom

>>> deriv2 = classical_parser.parse_derivation('''
... p → ((p → p) → p); axiom
... (p → ((p → p) → p)) → ((p → (p → p)) → (p → p)); axiom
... p → (p → p); axiom
... ((p → (p → p)) → (p → p)); mp; [0,1]
... p → p; mp; [2,3]''')
>>> classical_logic_axiom_system.is_correct_derivation(deriv2, i)
True

An incorrect derivation

>>> deriv3 = classical_parser.parse_derivation('''
... p → ((p → p) → p); axiom
... (p → ((p → p) → p)) → ((p → (p → p)) → (p → p)); axiom
... p → p; mp; [0,1]''')
>>> classical_logic_axiom_system.is_correct_derivation(deriv3, i)
False
>>> correct, error_list = classical_logic_axiom_system.is_correct_derivation(deriv3, i, return_error_list=True)
>>> error_list
[2: ['→', ['p'], ['p']] was marked as mp, but it is not a correct application of that rule]

Instances¶

logics.instances.propositional.axiom_systems.classical_logic_axiom_system¶: Classical logic with only negation and conditional. See above for the axioms and rules.