feat: add Logics/Propositional/NaturalDeduction/* (#91) # Natural deduction for minimal logic This PR adds the definitions and basic properties of natural deduction for propositional logic. Key developments: - Definition of `Theory.Derivation`, the type of derivation trees. - Definitions of derivability and equivalence. - Operations on derivations: weakening, substitution and cut. --------- Co-authored-by: twwar Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com> Co-authored-by: Claude Co-authored-by: Chris Henson Co-authored-by: Shrys Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com> Co-authored-by: Ching-Tsun Chou Co-authored-by: Fabrizio Montesi Co-authored-by: Maximiliano Onofre-Martínez Co-authored-by: Tristan F.-R. Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com> Co-authored-by: euprunin Co-authored-by: kei <70096720+thelissimus@users.noreply.github.com> Co-authored-by: Juan Pablo Yamamoto Co-authored-by: Alexandre Rademaker Co-authored-by: Clark Barrett Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> Co-authored-by: Xueying Qin <32066429+XYUnknown@users.noreply.github.com> Co-authored-by: Jesse Alama Co-authored-by: mathlib4-bot Co-authored-by: milianoPhilosophyHub Co-authored-by: Tanner Duve <122851174+tannerduve@users.noreply.github.com> Co-authored-by: Tanner Duve Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: ADA <120643053+ADA-Projects@users.noreply.github.com> Co-authored-by: Aristotle Harmonic Co-authored-by: Sorrachai Yingchareonthawornchai Co-authored-by: Chris-F5 <60847556+Chris-F5@users.noreply.github.com> Co-authored-by: Garmelon Co-authored-by: Arjun Bhamra <33864884+abhamra@users.noreply.github.com> Co-authored-by: Bolton Bailey Co-authored-by: Benjamin Bisping Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com> Co-authored-by: Burkhardt Renz Co-authored-by: Eric Wieser Co-authored-by: Elimia <56419338+sehun1024@users.noreply.github.com> Co-authored-by: mathlib-nightly-testing[bot] Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com> Co-authored-by: Eric Wieser Co-authored-by: WegmannDavid <147524946+WegmannDavid@users.noreply.github.com> Co-authored-by: Pieter Cuijpers Co-authored-by: Marcelo Lynch Co-authored-by: Kim Morrison

document -/ #91

Description

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions