Natural Deduction

Base Classes

The Derivation and NaturalDeductionStep classes are shared with the propositional ND module.

class logics.classes.predicate.proof_theories.PredicateNaturalDeductionRule(rule, arbitrary_cts=None)

The differences between this class and the propositional one stem only from the rules requiring that a given constant is arbitrary up to that point in the derivation

Examples

>>> from logics.classes.predicate import PredicateFormula as Formula
>>> from logics.classes.predicate.proof_theories.natural_deduction import NaturalDeductionStep, PredicateNaturalDeductionRule
>>> univ_intro = PredicateNaturalDeductionRule([
...     '(...)',
...     NaturalDeductionStep(Formula(['[α/χ]A']), open_suppositions=[]),
...     '(...)',
...     NaturalDeductionStep(Formula(['∀', 'x', ['A']]), 'I∀', [0], open_suppositions=[])
... ], arbitrary_cts=['α'])
>>> univ_intro.arbitrary_cts
['α']
>>> # The rest works the same than in the propositional case
>>> univ_intro.premises
[['[α/χ]A']]
>>> univ_intro.index(NaturalDeductionStep(Formula(['∀', 'x', ['A']]), open_suppositions=[]))
1

Natural Deduction System

class logics.classes.predicate.proof_theories.PredicateNaturalDeductionSystem(language, rules)

The differences between this class and the propositional one stem from rules with arbitrary constants and rules with formulae of the form [α/χ]A. The user interface is the same, though.

Examples

>>> from logics.utils.parsers.predicate_parser import classical_predicate_parser as parser
>>> from logics.instances.predicate.natural_deduction import predicate_classical_natural_deduction_system as nd_system
>>> deriv = parser.parse_derivation('''
...     ∃x R(x, a); premise; []; []
...     ∃y ∃x R(x, y); I∃; [0]; []
... ''', natural_deduction=True)
>>> nd_system.is_correct_application(deriv, 1, nd_system.rules['I∃'])
True
>>> deriv = parser.parse_derivation('''
...     P(a); premise; []; []
...     ∀x P(x); I∀; [0]; []
... ''', natural_deduction=True)
>>> rule = nd_system.substitute_rule(deriv, 1, nd_system.rules['I∀'])  # to get a specific instance of the rule
>>> is_correct, error = nd_system.check_arbitrary_constants(deriv, 1, rule)
>>> is_correct
False
>>> error
"Constant 'a' is not arbitrary"
>>> deriv = parser.parse_derivation('''
...     ∃x R(x, x); premise; []; []
...     R(a, a); supposition; []; [1]
...     ∃y R(y, y); I∃; [1]; [1]
...     R(a, a) → ∃y R(y, y); I→; [1,2]; []
...     ∃y R(y, y); E∃; [0, 3]; []
... ''', natural_deduction=True)
>>> nd_system.is_correct_derivation(deriv)
True

Notes

The class is hardcoded to work with the usual quantifier rules. If you want to give it different ones, you may need to adjust the code

Instances

logics.instances.predicate.natural_deduction.predicate_classical_natural_deduction_system

Has same rules as the propositional system 1, plus the following rules:

first_order_primitive_rules.update({
    'E∀': PredicateNaturalDeductionRule([
        '(...)',
        NaturalDeductionStep(PredicateFormula(['∀', 'χ', ['A']]), open_suppositions=[]),
        '(...)',
        NaturalDeductionStep(PredicateFormula(['[α/χ]A']), 'E∀', [0], open_suppositions=[])
    ]),

    'I∀': PredicateNaturalDeductionRule([
        '(...)',
        NaturalDeductionStep(PredicateFormula(['[α/χ]A']), open_suppositions=[]),
        '(...)',
        NaturalDeductionStep(PredicateFormula(['∀', 'χ', ['A']]), 'I∀', [0], open_suppositions=[])
    ], arbitrary_cts=['α']),

    'I∃': PredicateNaturalDeductionRule([
        '(...)',
        NaturalDeductionStep(PredicateFormula(['[α/χ]A']), open_suppositions=[]),
        '(...)',
        NaturalDeductionStep(PredicateFormula(['∃', 'χ', ['A']]), 'I∃', [0], open_suppositions=[])
    ]),

    'E∃': PredicateNaturalDeductionRule([
        '(...)',
        NaturalDeductionStep(PredicateFormula(['∃', 'χ', ['A']]), open_suppositions=[]),
        '(...)',
        NaturalDeductionStep(PredicateFormula(['→', ['[α/χ]A'], ['B']]), open_suppositions=[]),
        '(...)',
        NaturalDeductionStep(PredicateFormula(['B']), 'E∃', [0, 1], open_suppositions=[]),
    ], arbitrary_cts=['α']),
})

Natural Deduction Solver

class logics.utils.solvers.first_order_natural_deduction.FirstOrderNaturalDeductionSolver(language, simplification_rules, derived_rules_derivations, heuristics)

First-order natural deduction solver. Has the same user interface than the propositional one.

Examples

>>> from logics.utils.parsers.predicate_parser import classical_predicate_parser as parser
>>> from logics.utils.solvers.first_order_natural_deduction import first_order_natural_deduction_solver as solver
>>> deriv = solver.solve(parser.parse('~∃x (P(x)) / ∀x (~P(x))'))
>>> deriv.print_derivation(parser)
0. ~∃x (P(x)); premise; []
|  1. P(a); supposition; []
|  2. ∃x (P(x)); I∃; [1]
|  3. ⊥; E~; [0, 2]
4. ~P(a); I~; [1, 3]
5. ∀x (~P(x)); I∀; [4]

Instances

logics.utils.solvers.first_order_natural_deduction.first_order_natural_deduction_solver

A solver for the natural deduction system presented above.