feat (Logics/Propositional/NaturalDeduction): Natural deduction for propositional logic

[thomaskwaring]

NJ

This pull request formalises (a version of) Gentzen's system NJ for propositional logic.

Files

• Propositional.Defs : defines the type of propositions.
• Propositional.NaturalDeduction.Basic : defines the type of derivations and their basic properties, including weakening and substitution. Also develops equivalence of propositions.
• Propositional.NaturalDeduction.Theorems : derives some elementary equivalences and implications, such as De Morgan's laws, multiple negations, and so forth.

Notes

We develop natural deduction for minimal logic, and define derivability relative to a theory (set of propositions). Then intuitionistic (resp. classical) derivability is obtained by adding the principle of explosion (resp. double-negation elimination).

There are some non-obvious design choices to be made here, specifically in the definition of Derivation. On the grounds of simplicity, I believe these are relatively optimal.

• I do not require anything of the type Atom apart from decidable equality, in particular it need not be inhabited. It then has a bottom element whenever Atom does, and a top element whenever Atom is inhabited. This will make the definitions of algebraic semantics more natural: for minimal logic the semantics are naturally defined for generalised Heyting algebras, which have a top but no bottom.
• I use Finset's of propositions as contexts — this avoids explicit contraction and exchange, and is very easy to work with using grind.
• I treat weakening as a derived rule, by allowing arbitrary contexts in axiom rules.
• I do not obey the "crude-discharge convention", that hypotheses are discharged at the earliest opportunity. This choice is more natural in the context we are in, where the collection of open hypotheses is tracked explicitly. To be specific, the implication introduction rule has the form implI {A B : Proposition Atom} (Γ : Ctx Atom) : Derivation ⟨insert A Γ, B⟩ → Derivation ⟨Γ, impl A B⟩, and our convention manifests as not forbidding A ∈ Γ (or, equivalently, a rule with type Derivation ⟨Γ, B⟩ → Derivation ⟨Γ \ {A}, impl A B⟩).

Less obvious, & something I am looking for feedback on is the way I have treated theories. An alternative, which might be cleaner once sufficient API is developed, would be to have two kinds of axiom rules, one for propositions A ∈ Γ (context) and a separate one for A ∈ T (theory). This would restore the simplicity of the definition of Derivable, to something like

def Theory.SDerivable {T : Theory} {S : Sequent} := Nonempty (T.Derivation S)

[thomaskwaring]

Closing this — the more I think about it, the more I want to do it differently (better). Sorry to anyone who spent time reviewing it, new (smaller) PRs on the way.