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 has open_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 has on_steps=[0,1] since the non-'(...)' steps are the 0 and 1 steps.

Finally, note that the '(...)' will not count for either the index or len 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

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 and E∧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 and q / p')
>>> deriv = classical_parser.parse_derivation('''
... p and q; premise; []; []
... p; E∧; [0]; []''',
... natural_deduction=True)
>>> classical_natural_deduction_system.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

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 method

Examples

>>> 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:

classical_primitive_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=[]),
        '(...)',
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. The I~ rule takes a formula of the form A ∧ ~A instead of ⊥ as the last step inside the supposition. The rest is identical.

# Negation introduction is with the conjunction instead of Falsum
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=[])
])

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.