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'>
-
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]
-
property
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]