Natural Deduction¶
Base classes¶
- class logics.classes.propositional.proof_theories.NaturalDeductionStep(content, justification=None, on_steps=None, open_suppositions=None)¶
Step of a natural deduction derivation.
Extends logics.classes.propositional.proof_theories.DerivationStep adding an additional parameter open_suppositions (list of int)
Examples
A natural deduction step will have the following form
>>> from logics.classes.propositional.proof_theories import NaturalDeductionStep >>> from logics.utils.parsers import classical_parser >>> s = NaturalDeductionStep(content=classical_parser.parse('p or ~q'), justification='I∨', ... on_steps=[0], open_suppositions=[1]) >>> s ['∨', ['p'], ['~', ['q']]]; I∨; [0]; [1]
- class logics.classes.propositional.proof_theories.NaturalDeductionRule(iterable=(), /)¶
Class for natural deduction rules.
Extends logics.classes.propositional.proof_theories.Derivation. A rule is basically a Derivation of NaturalDeductionStep’s. The premises of the rule need not have justifications and on_steps (by default, they will be
None
and[]
). They can also have steps which are simply the string'(...)'
, which will mark that there can be any number of steps between the previous and the next.Examples
Conditional introduction for classical logic will look like this:
>>> from logics.utils.parsers import classical_parser >>> from logics.classes.propositional.proof_theories import NaturalDeductionStep, NaturalDeductionRule >>> cond_intro = NaturalDeductionRule([ ... '(...)', ... NaturalDeductionStep(classical_parser.parse('A'), 'supposition', open_suppositions=[0]), ... '(...)', ... NaturalDeductionStep(classical_parser.parse('B'), open_suppositions=[0]), ... NaturalDeductionStep(classical_parser.parse('A → B'), 'I→', [0, 1], open_suppositions=[]) ... ])
Since there is a
'(...)'
before A, that step need not be first step of the derivation. There can also be any number of steps between A and B. However, step A → B must come immetiately after B since there is no'(...)'
inbetween.Also note that the indexes of the on_step and the open_supposition parameters within the rule ignore the
'(...)'
members. For example, the first step hasopen_suppositions=[0]
which means that a supposition is being opened in that step (which is not index 0, but is step 0). The last step also hason_steps=[0,1]
since the non-'(...)'
steps are the 0 and 1 steps.Finally, note that the
'(...)'
will not count for either theindex
orlen
methods, but will count for__getitem__
:>>> cond_intro.index(NaturalDeductionStep(classical_parser.parse('B'), open_suppositions=[0])) 1 >>> len(cond_intro) 3 >>> cond_intro[0] '(...)'
Natural Deduction System¶
- class logics.classes.propositional.proof_theories.NaturalDeductionSystem(language, rules)¶
Class for natural deduction systems.
- Parameters:
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
rules (dict (str: logics.classes.propositional.proof_theories.NaturalDeductionRule)) – The keys are strings (the name of the rule) and the values are NaturalDeductionRule
Examples
Example (toy) system with only conjunction rules:
>>> from logics.utils.parsers import classical_parser >>> from logics.classes.propositional.proof_theories import NaturalDeductionStep, NaturalDeductionRule, NaturalDeductionSystem >>> from logics.instances.propositional.languages import classical_infinite_language >>> rules = { ... 'I∧': NaturalDeductionRule([ ... '(...)', ... NaturalDeductionStep(classical_parser.parse('A')), ... '(...)', ... NaturalDeductionStep(classical_parser.parse('B')), ... '(...)', ... NaturalDeductionStep(classical_parser.parse('A ∧ B'), 'I∧', [0, 1], open_suppositions=[]) ... ]), ... ... 'E∧1': NaturalDeductionRule([ ... '(...)', ... NaturalDeductionStep(classical_parser.parse('A ∧ B')), ... '(...)', ... NaturalDeductionStep(classical_parser.parse('A'), 'E∧1', [0], open_suppositions=[]) ... ]), ... ... 'E∧2': NaturalDeductionRule([ ... '(...)', ... NaturalDeductionStep(classical_parser.parse('A ∧ B')), ... '(...)', ... NaturalDeductionStep(classical_parser.parse('B'), 'E∧2', [0], open_suppositions=[]) ... ])} >>> toy_system = NaturalDeductionSystem(language=classical_infinite_language, rules=rules)
For more realistic instances you may look at instances below. In the examples below we will be working with a full classical logic instance defined in
>>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_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 via the application of a rule to a previous step, and that the last step is the conclusion of inference.
- Parameters:
derivation (logics.classes.propositional.proof_theories.Derivation) – The derivation the algorithm will look at
inference (logics.classes.propositional.Inference or None, optional) – 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, optional) – 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
A correct derivation of modus ponens using all the classical rules
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system >>> inf = classical_parser.parse('q, p → q / q') >>> deriv = classical_parser.parse_derivation(''' ... q; premise; []; [] ... ~q; supposition; []; [1] ... ~q; repetition; [1]; [1] ... (q ∧ ~q); I∧; [0, 2]; [1] ... q; E∧1; [3]; [1] ... ⊥; E~; [1, 4]; [1] ... p; EFSQ; [5]; [1] ... ⊥; repetition; [5]; [1] ... ~~q; I~; [1, 7]; [] ... q; ~~; [8]; [] ... q; supposition; []; [10] ... q; repetition; [10]; [10] ... (q → q); I→; [10, 11]; [] ... q; E→; [12, 9]; [] ... (q ∨ p); I∨1; [13]; [] ... (p → q); premise; []; [] ... q; E∨; [14, 12, 15]; []''', ... natural_deduction=True) >>> classical_natural_deduction_system.is_correct_derivation(deriv, inf) True
Using a step in a closed supposition (inference left as
None
)>>> deriv2 = classical_parser.parse_derivation(''' ... p; supposition; []; [0] ... p; repetition; [0]; [0] ... (p → p); I→; [0, 1]; [] ... p; E→; [2, 0]; []''', ... natural_deduction=True) >>> correct, error_list = classical_natural_deduction_system.is_correct_derivation(deriv2, return_error_list=True) >>> correct False >>> error_list [3: Step 0 is in a closed supposition]
Incorrectly closing a supposition, with a rule that does not allow that
>>> deriv3 = classical_parser.parse_derivation(''' ... p; premise ... p; supposition; []; [1] ... p; repetition; [0]; [1] ... (p ∨ q); I∨1; [0]; []''', ... natural_deduction=True) >>> correct, error_list = classical_natural_deduction_system.is_correct_derivation(deriv3, return_error_list=True) >>> correct False >>> error_list [3: Incorrect supposition handling]
Notes
For rules that have more than one variant (e.g.
E∧1
andE∧2
) you can omit the number. E.g.:>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system >>> inf = classical_parser.parse('p ∧ q / p') >>> deriv = classical_parser.parse_derivation(''' ... p ∧ q; premise; []; [] ... p; E∧; [0]; []''', ... natural_deduction=True) >>> classical_natural_deduction_system.is_correct_derivation(deriv, inf) True
Also note that
on_steps
need to be provided in the order they were specified in the rule. E.g., the conditional elimination rule states:>>> cond_elim = NaturalDeductionRule([ >>> '(...)', >>> NaturalDeductionStep(Formula(['→', ['A'], ['B']]), open_suppositions=[]), >>> '(...)', >>> NaturalDeductionStep(Formula(['A']), open_suppositions=[]), >>> '(...)', >>> NaturalDeductionStep(Formula(['B']), 'E→', [0, 1], open_suppositions=[]) >>> ]),
So, if we do:
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system >>> inf = classical_parser.parse('p → q, p / q') >>> deriv = classical_parser.parse_derivation(''' ... p → q; premise; []; [] ... p; premise; []; [] ... q; E→; [1, 0]; []''', ... natural_deduction=True) >>> classical_natural_deduction_system.is_correct_derivation(deriv, inf) False
The last step is incorrect because the conditional elimination rule specifies that the first
on_step
is the conditional statement and the second is the antecedent.If you want to be able to specify them in reverse order, the solution is to add another rule to the system with the
on_steps
reversed. There are some predefined systems that do this (for rules that do not involve suppositions), see the Instances below.>>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system_unordered >>> # define the same inference and derivation as in the example above >>> classical_natural_deduction_system_unordered.is_correct_derivation(deriv, inf) True
- is_correct_application(derivation, step, rule, return_error=False)¶
Determines if a rule has been correctly applied at a particular derivation step.
- Parameters:
derivation (logics.classes.propositional.proof_theories.Derivation) – The derivation in which the step is located
step (int) – The index of the step in the derivation
rule (logics.classes.propositional.proof_theories.NaturalDeductionRule) – The rule to check for correct application
return_error (bool) – If False, the method will just return True or False. If True will also return a single instance of
logics.classes.errors.CorrectionError
.
Examples
A derivation with the first two steps correctly applied, and an incorrect third step
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system >>> deriv = classical_parser.parse_derivation( ... '''p; supposition; []; [0] ... p; repetition; [0]; [0] ... (p → p); I→; [0, 1]; [] ... p; E→; [2, 0]; []''', ... natural_deduction=True) >>> classical_natural_deduction_system.is_correct_application(deriv, 1, classical_natural_deduction_system.rules['repetition']) True >>> classical_natural_deduction_system.is_correct_application(deriv, 2, classical_natural_deduction_system.rules['I→']) True >>> classical_natural_deduction_system.is_correct_application(deriv, 3, classical_natural_deduction_system.rules['E→']) False >>> classical_natural_deduction_system.is_correct_application(deriv, 3, classical_natural_deduction_system.rules['E→'], ... return_error=True) (False, 3: Step 0 is in a closed supposition)
- static solve_derivation(inference, solver)¶
Take an inference and a solver, and returns a derivation for the former.
The solver in question must have a
solve
methodExamples
>>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system >>> from logics.utils.solvers import classical_natural_deduction_solver >>> from logics.utils.parsers import classical_parser >>> deriv = classical_natural_deduction_system.solve_derivation(classical_parser.parse('p then q, ~q / ~p'), ... classical_natural_deduction_solver) >>> deriv.print_derivation(classical_parser) 0. (p → q); premise; [] 1. ~q; premise; [] | 2. p; supposition; [] | 3. q; E→; [0, 2] | 4. ⊥; E~; [1, 3] 5. ~p; I~; [2, 4]
Instances¶
- logics.instances.propositional.natural_deduction.classical_natural_deduction_system¶
Has the following rules:
'I~': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), 'supposition', open_suppositions=[0]), '(...)', NaturalDeductionStep(Formula(['⊥']), open_suppositions=[0]), NaturalDeductionStep(Formula(['~', ['A']]), 'I~', [0, 1], open_suppositions=[]) ]), 'E~': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['~', ['A']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['⊥']), 'E~', [0, 1], open_suppositions=[]) ]), '~~': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['~', ['~', ['A']]]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), '~~', [0], open_suppositions=[]) ]), 'I→': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), 'supposition', open_suppositions=[0]), '(...)', NaturalDeductionStep(Formula(['B']), open_suppositions=[0]), NaturalDeductionStep(Formula(['→', ['A'], ['B']]), 'I→', [0, 1], open_suppositions=[]) ]), 'E→': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['→', ['A'], ['B']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['B']), 'E→', [0, 1], open_suppositions=[]) ]), 'I∧': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['B']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['∧', ['A'], ['B']]), 'I∧', [0, 1], open_suppositions=[]) ]), 'E∧1': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['∧', ['A'], ['B']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), 'E∧1', [0], open_suppositions=[]) ]), 'E∧2': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['∧', ['A'], ['B']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['B']), 'E∧2', [0], open_suppositions=[]) ]), 'I∨1': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['∨', ['A'], ['B']]), 'I∨1', [0], open_suppositions=[]) ]), 'I∨2': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['∨', ['B'], ['A']]), 'I∨2', [0], open_suppositions=[]) ]), 'E∨': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['∨', ['A'], ['B']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['→', ['A'], ['C']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['→', ['B'], ['C']]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['C']), 'E∨', [0, 1, 2], open_suppositions=[]) ]), 'repetition': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), 'repetition', [0], open_suppositions=[]) ]), 'EFSQ': NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['⊥']), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), 'EFSQ', [0], open_suppositions=[]) ]),
- logics.instances.propositional.natural_deduction.classical_natural_deduction_system2¶
Alternative (but also usual) presentation of the classical natural deduction system. Has no repetition nor EFSQ as primitive rules. The
E~
rule is double negation. TheI~
rule takes a formula of the formA ∧ ~A
instead of⊥
as the last step inside the supposition. The rest is identical.classical_natural_deduction_system2.rules['I~'] = NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['A']), 'supposition', open_suppositions=[0]), '(...)', NaturalDeductionStep(Formula(['∧', ['B'], ['~', ['B']]]), open_suppositions=[0]), NaturalDeductionStep(Formula(['~', ['A']]), 'I~', [0, 1], open_suppositions=[]) ]) # Negation elimination is double negation classical_natural_deduction_system2.rules['E~'] = NaturalDeductionRule([ '(...)', NaturalDeductionStep(Formula(['~', ['~', ['A']]]), open_suppositions=[]), '(...)', NaturalDeductionStep(Formula(['A']), 'E~', [0], open_suppositions=[]) ])
The following systems are identical to the two above, but do not take into account on_steps
order:
- logics.instances.propositional.natural_deduction.classical_natural_deduction_system_unordered¶
- logics.instances.propositional.natural_deduction.classical_natural_deduction_system2_unordered¶
See the note to is_correct_derivation
above.
Natural Deduction Solver¶
- class logics.utils.solvers.natural_deduction.NaturalDeductionSolver(language, simplification_rules, derived_rules_derivations, heuristics)¶
A heuristic solver for natural deduction
Works by doing a combination of heuristic reasoning (e.g. if you need to derive a conditional, suppose its antecedent and try to reach its consequent) and blind derivation. Blind derivation works with simplification rules only, i.e. rules that do not add new formulae to their conclusion. These can be primitive or derived. In the second case, you should provide a hardcoded derivation of the derived rule, so that after the solver is finished, the steps where that rule is used are replaced with their derivation using only primitive rules.
- Parameters:
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – The language of the system
simplification_rules (dict of {str: logics.classes.propositional.Inference}) – The strings are the rule names, the values are inferences (not NaturalDeductionRule) that can function as elimination rules (they must not contain anything new in the conclusion)
derived_rules_derivations (dict of {str: logics.classes.propositional.proof_theories.Derivation}) – If among the simplification rules there are some derived rules, and in the final output you wish to replace their application with subderivations using only primitive rules, you can use this dict. The keys are the names of the rules, the values are derivations of the derived rule. See below for some examples.
heuristics (list of logics.utils.solvers.natural_deduction.Heuristic) – A list of heuristics to apply (see below). Will be applied in the order they are given in the list.
Examples
Most of the time you will be using the predefined classical solver instance and its solve method, as follows:
>>> from logics.utils.solvers import classical_natural_deduction_solver >>> classical_natural_deduction_solver.solve(classical_parser.parse("A → B, ~B / ~A")) 0. ['→', ['A'], ['B']]; premise; [] 1. ['~', ['B']]; premise; [] | 2. ['A']; supposition; [] | 3. ['B']; E→; [0, 2] | 4. ['⊥']; E~; [1, 3] 5. ['~', ['A']]; I~; [2, 4]
If you want to define your own solver instance, you can do that in the following way. For illustration, we will define a toy solver that uses only conjunction elimination and idempotence for disjunction as its simplification rules, and has only conjunction heuristics
>>> from logics.utils.parsers import classical_parser >>> from logics.instances.propositional.languages import classical_infinite_language_with_sent_constants_nobiconditional as cl_language >>> from logics.utils.solvers.natural_deduction import NaturalDeductionSolver >>> from logics.utils.solvers.natural_deduction import conjunction_heuristic # See below for more on heuristics >>> simplification_rules = { ... # Primitive rules ... 'E∧1': classical_parser.parse('A ∧ B / A'), ... 'E∧2': classical_parser.parse('A ∧ B / B'), ... # Derived rules ... 'IdemDisj': classical_parser.parse('A ∨ A / A') ... } >>> # Since we have used the non-primitive IdemDisj above, we need to give a hardcoded derivation for it ... derived_rules_derivations = {'IdemDisj': classical_parser.parse_derivation(''' ... A ∨ A; premise; []; [] ... A; supposition; []; [1] ... A; repetition; [1]; [1] ... (A → A); I→; [1, 2]; [] ... (A → A); repetition; [3]; [] ... A; E∨; [0, 3, 4]; []''', natural_deduction=True)} >>> toy_natural_deduction_solver = NaturalDeductionSolver(language=cl_language, ... simplification_rules=simplification_rules, ... derived_rules_derivations=derived_rules_derivations, ... heuristics=[conjunction_heuristic])
We can now begin deriving things with our new solver
>>> toy_natural_deduction_solver.solve(classical_parser.parse("A ∧ (B ∧ (C ∨ C)) / C")) 0. ['∧', ['A'], ['∧', ['B'], ['∨', ['C'], ['C']]]]; premise; [] 1. ['∧', ['B'], ['∨', ['C'], ['C']]]; E∧2; [0] 2. ['∨', ['C'], ['C']]; E∧2; [1] | 3. ['C']; supposition; [] | 4. ['C']; repetition; [3] 5. ['→', ['C'], ['C']]; I→; [3, 4] 6. ['→', ['C'], ['C']]; repetition; [5] 7. ['C']; E∨; [2, 5, 6]
- solve(inference)¶
Takes an Inference and returns a derivation for it
Examples
See above for an example using the predefined classical solver instance
- class logics.utils.solvers.natural_deduction.Heuristic¶
Parent class for defining heuristics.
To define your own heuristic, inherit from this class and override the is_applicable and apply_heuristic methods.
Examples
See the source code for examples on how to define heuristics.
- is_applicable(goal)¶
Determines whether the heuristic is applicable given the current goal.
Takes the goal as parameter and should return a boolean. The other two parameters are basically for the existential heuristic in the predicate solver
- apply_heuristic(derivation, goal, solver, tried_existentials)¶
Applies the heuristic.
Takes the current deriation, goal, current open suppositions and solver, and returns a derivation. The parameter jump_steps is present because of how the conjunction heuristic works (see the source code for the conjunction heuristic for more on this)
Instances¶
- logics.utils.solvers.classical_natural_deduction_solver¶
A solver for the natural deduction system presented above.
- logics.utils.solvers.classical_natural_deduction_solver2¶
A solver for the alternative natural deduction system.