Skip to main content

Logics is a Python framework for mathematical logic

Project description

Logics is a Python framework for mathematical logic. It aims at generality (being able to represent as many systems as possible), well-documented and readable code and minimal dependencies, rather than speed. Some of its intended applications are educational software (e.g. TAUT, which uses a previous version of this package), and quick prototyping of ideas for research purposes.

To see the documentation, visit this link.

Installation

To install using pip:

$ pip install logics

Or clone it from this repository:

$ git clone https://github.com/ariroffe/logics.git

Examples

The following are some random examples of what you can do with this package. For a full specification of the functionality see the documentation.

Define a language:

>>> from logics.classes.propositional import Language
>>> language = Language(atomics=['p', 'q', 'r'],
...                     constant_arity_dict={'~': 1, '∧': 2},
...                     sentential_constants=['⊥', '⊤'],
...                     metavariables=['A', 'B', 'C'],
...                     context_variables=['Γ', 'Δ', 'Σ', 'Λ', 'Π', 'Θ'])

Construct formulae and inferences/metainferences, and use specific methods of those classes:

>>> from logics.utils.parsers import classical_parser
>>> formula = classical_parser.parse('~(p and not q)')
>>> inference = classical_parser.parse('(p / p) // (q / p & not p)')
>>> type(formula)
<class 'logics.classes.propositional.formula.Formula'>
>>> type(inference)
<class 'logics.classes.propositional.inference.Inference'>
>>> formula.depth
3
>>> formula.is_well_formed(language)
True
>>> formula.is_instance_of(classical_parser.parse('not (A and B)'), language)
True
>>> formula2 = formula.substitute(classical_parser.parse("p"), classical_parser.parse("p or q"))
>>> classical_parser.unparse(formula2)
'~((p ∨ q) ∧ ~q)'
>>> inference.level
2

Define a mixed many-valued model theory, and use it:

>>> from logics.instances.propositional.languages import classical_infinite_language_with_sent_constants
>>> from logics.classes.propositional.semantics import MixedManyValuedSemantics
>>> trivalued_truth_values = ['1', 'i', '0']
>>> trivalued_truth_functions = {
...     '~': ['0', 'i', '1'],
...     '∧': [ #1   #i   #0
...           ['1', 'i', '0'],    # 1
...           ['i', 'i', '0'],    # i
...           ['0', '0', '0']],   # 0
...     '∨': [ #1   #i   #0
...           ['1', '1', '1'],    # 1
...           ['1', 'i', 'i'],    # i
...           ['1', 'i', '0']],   # 0
...     '→': [ #1   #i   #0
...           ['1', 'i', '0'],    # 1
...           ['1', 'i', 'i'],    # i
...           ['1', '1', '1']],   # 0
...     '↔': [ #1   #i   #0
...           ['1', 'i', '0'],    # 1
...           ['i', 'i', 'i'],    # i
...           ['0', 'i', '1']],   # 0
...     }
>>> ST = MixedManyValuedSemantics(language=classical_infinite_language_with_sent_constants,
...                               truth_values=trivalued_truth_values,
...                               premise_designated_values=['1'],
...                               conclusion_designated_values=['1', 'i'],
...                               truth_function_dict=trivalued_truth_functions,
...                               sentential_constant_values_dict={'⊥': '0', '⊤': '1'},
...                               name='ST')
>>> ST.valuation(classical_parser.parse('p then q'), {'p': '1', 'q': 'i'})
'i'
>>> ST.satisfies(classical_parser.parse('(A / B), (B / C) // (A / C)'), {'A': '1', 'B': 'i', 'C': '0'})
False
>>> ST.is_valid(classical_parser.parse('p and ~p / q'))
True
>>> ST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)'))
False
>>> ST.is_globally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)'))
True
>>> # There are also some predefined systems (ST is one of them, the above was unnecesary)
>>> from logics.instances.propositional.many_valued_semantics import TS_mvl_semantics as TS
>>> from logics.instances.propositional.many_valued_semantics import LP_mvl_semantics as LP
>>> LP.is_valid(classical_parser.parse('p and ~p / q'))
False
>>> from logics.classes.propositional.semantics import MixedMetainferentialSemantics
>>> TSST = MixedMetainferentialSemantics([TS, ST])
>>> TSST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)'))
True

As in TAUT, logics has natural deduction module:

>>> # You can define your own natural deduction system, here we will just import a predefined instance:
>>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system
>>> from logics.utils.solvers import classical_natural_deduction_solver
>>> derivation = classical_natural_deduction_solver.solve(classical_parser.parse("A → B, ~B / ~A"))
>>> derivation.print_derivation(classical_parser)
0. A → B; premise; []
1. ~B; premise; []
|  2. A; supposition; []
|  3. B; E→; [0, 2]
|  4. ⊥; E~; [1, 3]
5. ~A; I~; [2, 4]
>>> classical_natural_deduction_system.is_correct_derivation(derivation)
True
>>> # Also in first order!
>>> from logics.utils.parsers import classical_predicate_parser
>>> from logics.utils.solvers.first_order_natural_deduction import first_order_natural_deduction_solver
>>> derivation = first_order_natural_deduction_solver.solve(classical_predicate_parser.parse('~∃x P(x) / ∀x ~P(x)'))
>>> derivation.print_derivation(classical_predicate_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]

I have now added tableaux systems:

>>> from logics.classes.propositional.proof_theories import TableauxNode
>>> # Again, you can define your own tableaux system, here I use a predefined instance
>>> from logics.instances.propositional.tableaux import classical_tableaux_system
>>> n1 = TableauxNode(content=classical_parser.parse('~~~~p'))
>>> n2 = TableauxNode(content=classical_parser.parse('~p'), parent=n1)
>>> n3 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~', parent=n2)
>>> n1.print_tree(classical_parser)
(~~~p)
└── ~p
    └── ~~p (R~~)
>>> classical_tableaux_system.node_is_closed(n2)
False
>>> classical_tableaux_system.tree_is_closed(n1)
True
>>> classical_tableaux_system.rule_is_applicable(n1, 'R~~')
True
>>> classical_tableaux_system.is_correct_tree(n1)
True
>>> # The tableaux solver (unlike ND one) will work for any arbitrary system you define
>>> tree = classical_tableaux_system.solve_tree(classical_parser.parse("~(p ∧ q) / ~p ∨ ~q"))
>>> tree.print_tree(classical_parser)
~(p ∧ q)
└── ~(~p ∨ ~q)
    ├── ~p (R~∧)
    │   └── ~~p (R~∨)
    │       └── ~~q (R~∨)
    └── ~q (R~∧)
        └── ~~p (R~∨)
            └── ~~q (R~∨)
>>> # There is even a tableaux class for indexed tableaux, here is a predefined instance
>>> from logics.instances.propositional.tableaux import LP_tableaux_system
>>> tree2 = LP_tableaux_system.solve_tree(classical_parser.parse("~(p ∨ q) / ~~p ∧ ~~q"))
>>> tree2.print_tree(classical_parser)
~(p ∨ q), 1
└── ~~p ∧ ~~q, 0
    └── ~p ∧ ~q, 1 (R~∨1)
        ├── ~~p, 0 (R∧0)
        │   └── ~p, 1 (R∧1)
        │       └── ~q, 1 (R∧1)
        │           └── p, 0 (R~~0)
        └── ~~q, 0 (R∧0)
            └── ~p, 1 (R∧1)
                └── ~q, 1 (R∧1)
                    └── q, 0 (R~~0)

And sequent calculi:

>>> sequent = classical_parser.parse("Gamma, A ==> B, Delta")
>>> classical_parser.unparse(sequent)
'Γ, A ⇒ B, Δ'
>>> sequent2 = sequent.substitute(language, "Γ", classical_parser.parse("D"))
>>> classical_parser.unparse(sequent2)
'D, A ⇒ B, Δ'
>>> # Again, you can define your sequent calculus, here I use a predefined instance
>>> from logics.instances.propositional.sequents import LK
>>> LK.sequent_is_axiom(classical_parser.parse("p or q ==> p or q"))
True
>>> from logics.classes.propositional.proof_theories import SequentNode
>>> n1 = SequentNode(content=classical_parser.parse('A ==> A'), justification='identity')
>>> n2 = SequentNode(content=classical_parser.parse('A ==> A, Delta'), justification='WR', children=[n1])
>>> n3 = SequentNode(content=classical_parser.parse('Gamma, A ==> A, Delta'), justification='WL', children=[n2])
>>> n3.print_tree(classical_parser)  # the root of the tree is the derived node
Γ, A ⇒ A, Δ (WL)
└── A ⇒ A, Δ (WR)
    └── A ⇒ A (identity)
>>> LK.is_correct_tree(n1)
True
>>> LK.tree_is_closed(n3)
True
>>> # There is also a solver that will work whenever your system has no elimination rules
>>> # A system that the solver can work with easily, see the docs for a description
>>> from logics.instances.propositional.sequents import LKminEA
>>> tree = LKminEA.reduce(classical_parser.parse("Gamma ==> A or ~A"))
>>> tree.print_tree(classical_parser)
Γ ⇒ A ∨ ~A (∨R1)
└── Γ ⇒ A, ~A (~R)
    └── Γ, A ⇒ A (WL)
        └── A ⇒ A (identity)

There are also some predicate logic tools:

>>> from logics.classes.predicate.semantics import Model
>>> model = Model({
...     'domain': {1, 2},
...     'a': 1,
...     'b': 2,
...     'P': {1},
...     'R': {(1,1), (1,2)},
...     'f': {((1,), 2), ((2,), 1)},
...     'g': {((1, 1), 1), ((1, 2), 2), ((2, 1), 1), ((2, 2), 2)}
... })
>>> model.denotation('f')
{((2,), 1), ((1,), 1)}
>>> # Again, predefined instance, you can define this yourself
>>> from logics.instances.predicate.model_semantics import classical_functional_model_semantics
>>> classical_functional_model_semantics.valuation(parser.parse("P(a)"), model)
'1'
>>> classical_functional_model_semantics.valuation(parser.parse("R(a, b)"), model)
'1'
>>> classical_functional_model_semantics.valuation(parser.parse("R(f(a), g(f(a), b))"), model)
'0'
>>> classical_functional_model_semantics.valuation(parser.parse("exists x (P(f(x)))"), model)
'1'
>>> classical_functional_model_semantics.valuation(parser.parse("forall X (exists x (X(f(x))))"), model)
'0'
>>> # You can also define theories with fixed denotations for some terms by subclassing Model
>>> from itertools import count
>>> from logics.instances.predicate.model_subclasses import ArithmeticModel
>>> from logics.utils.parsers.predicate_parser import arithmetic_parser
>>> from logics.instances.predicate.model_semantics import arithmetic_model_semantics
>>> arithmetic_model = ArithmeticModel({'domain': count(0)})
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("s(0) > 0"), arithmetic_model)
'1'
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("s(0) + s(0) = s(s(0))"), arithmetic_model)
'1'
>>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("exists x (x = s(0))"), arithmetic_model)
'1'

And many more things! (see the documentation)

Acknowledgements

logics is a project by Ariel Jonathan Roffé (CONICET / University of Buenos Aires)

Contributors to the project:

The author also wishes to thank the Buenos Aires Logic Group who supported this project.

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

logics-1.10.3.tar.gz (149.6 kB view details)

Uploaded Source

Built Distribution

logics-1.10.3-py3-none-any.whl (169.1 kB view details)

Uploaded Python 3

File details

Details for the file logics-1.10.3.tar.gz.

File metadata

  • Download URL: logics-1.10.3.tar.gz
  • Upload date:
  • Size: 149.6 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/3.4.1 importlib_metadata/3.7.3 pkginfo/1.7.0 requests/2.25.0 requests-toolbelt/0.9.1 tqdm/4.59.0 CPython/3.10.12

File hashes

Hashes for logics-1.10.3.tar.gz
Algorithm Hash digest
SHA256 1b4da29fdeb0582f58751297e79d472137afea62d9fa29b6547256afca2f3a58
MD5 096e7750adb86368ea97c3e764987616
BLAKE2b-256 980897aa97c47659f55b539e4b34c118b0d79f2888408b87f518d3cf71f404d0

See more details on using hashes here.

File details

Details for the file logics-1.10.3-py3-none-any.whl.

File metadata

  • Download URL: logics-1.10.3-py3-none-any.whl
  • Upload date:
  • Size: 169.1 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/3.4.1 importlib_metadata/3.7.3 pkginfo/1.7.0 requests/2.25.0 requests-toolbelt/0.9.1 tqdm/4.59.0 CPython/3.10.12

File hashes

Hashes for logics-1.10.3-py3-none-any.whl
Algorithm Hash digest
SHA256 61a447b10938dfae06383a6a26ce6fce419f0be2c3948bd560a4350763857540
MD5 a176a0d3a5574f1fb540ac2582ee018a
BLAKE2b-256 7bee8425a3767b1ee3d03bbb4f540e32a3ef979587063f49ee4ebc8f035ea2ee

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page