namespace http://cds.omdoc.org/examples❚
// @_title Propositional Logic in MMT❙
// @_author Florian Rabe❙
/T
Intuitionistic propositional logic with natural deduction rules and a few example proofs ❚
/T We use LF as the meta-theory for all theories in this file.❚
fixmeta http://cds.omdoc.org/urtheories?LF❚
/T
We start with the syntax of propositional logic.❚
theory PL =
# :types The Basic Concepts❙
/T the type of propositions ❙
prop : type ❙
/T Given [F:prop], the type $⊦ F$ holds the proofs of $F$.❙
ded : prop ⟶ type ❘ # ⊦ 1 prec -5❘role Judgment❙
## Abbreviations❙
/T The type $contra$ abbreviates the judgment of inconsistency.
If we can give an element of the type, then every proposition has a proof.❙
contra : type ❘ = {a} ⊦ a❘ # ↯ ❙
# Constructors❙
/T The constructors provide the expressions of the types above.❙
true : prop ❙
false : prop ❙
and : prop ⟶ prop ⟶ prop ❘ # 1 ∧ 2 prec 15❙
or : prop ⟶ prop ⟶ prop ❘ # 1 ∨ 2 prec 15❙
impl : prop ⟶ prop ⟶ prop ❘ # 1 ⇒ 2 prec 10❙
not : prop ⟶ prop ❘ # ¬ 1 prec 20❙
/T Equivalence is taken as a non-primitive here and defined such that for [F:prop,G:prop] we define $F⇔G$ as $(F ⇒ G) ∧ (G ⇒ F)$.❙
equiv : prop ⟶ prop ⟶ prop ❘ # 1 ⇔ 2 prec 10❘
= [x,y] (x ⇒ y) ∧ (y ⇒ x)❙
❚
/T Now we describe the proof theory.❚
theory PLNatDed =
include ?PL ❙
/T We use natural ⊦uction proof rules that construct expressions of type $⊦ F$ for some [F:prop].
{For example, assume two propositions [F: prop, G: prop].
{If [p:⊦ F, q: ⊦ G], then $andI p q$ is a proof of $F∧G$.}
{If [p:⊦ F∧G], then $andEl p$ is a proof of $F$.}
}
❙
trueI : ⊦ true❙
falseE : ⊦ false ⟶ ↯❙
andI : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ A ∧ B ❙
andEl : {A,B} ⊦ A ∧ B ⟶ ⊦ A ❘ role ForwardRule❙
andEr : {A,B} ⊦ A ∧ B ⟶ ⊦ B ❘ role ForwardRule❙
orIl : {A,B} ⊦ A ⟶ ⊦ A ∨ B ❙
orIr : {A,B} ⊦ B ⟶ ⊦ A ∨ B ❙
orE : {A,B,C} ⊦ A ∨ B ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C❙
impI : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⇒ B ❙
impE : {A,B} ⊦ A ⇒ B ⟶ ⊦ A ⟶ ⊦ B ❘ role ForwardRule❙
notI : {A} (⊦ A ⟶ ↯) ⟶ ⊦ ¬ A❘# notI 2❙
notE : {A} ⊦ ¬ A ⟶ ⊦ A ⟶ ↯ ❘# notE 2 3❘ role ForwardRule❙
equivI : {A,B} (⊦ A ⟶ ⊦ B) ⟶ (⊦ B ⟶ ⊦ A) ⟶ ⊦ A ⇔ B ❘
= [A,B,p,q] andI (impI [x] p x) (impI [x] q x) ❙
equivEl : {A,B} ⊦ A ⇔ B ⟶ ⊦ A ⟶ ⊦ B ❘ role ForwardRule❘
= [A,B,p,a] impE (andEl p) a ❙
equivEr : {A,B} ⊦ A ⇔ B ⟶ ⊦ B ⟶ ⊦ A ❘ role ForwardRule❘
= [A,B,p,b] impE (andEr p) b ❙
imp2I : {A,B,C} (⊦ A ⟶ (⊦ B ⟶ ⊦ C)) ⟶ ⊦ A ⇒ (B ⇒ C) ❘
= [A,B,C] [f] impI [p] (impI ([q] f p q)) ❙
imp2E : {A,B,C} ⊦ A ⇒ (B ⇒ C) ⟶ ⊦ A ⟶ ⊦ B ⟶ ⊦ C ❘
= [A,B,C] [p,q,r] impE (impE p q) r ❙
example : {A} ⊦ A ⇒ (A ∧ A) ❘
= [A]impI [p]andI p p❙
❚
theory DeclarativeProofs =
include ?PL❙
cut : {A,B} ⊦A ⟶ (⊦A ⟶ ⊦B) ⟶ ⊦B❘
= [A,B,p,q] q p❘ # PROVE 1 BY 3 4❙
have : {A} ⊦A ⟶ ⊦A❘ = [A,p] p❘ # HAVE 1 BY 2❙
❚
theory Declarative_PL =
include ?PLNatDed❙
include ?DeclarativeProofs❙
decl_trueI = trueI❘ # TRIVIAL❙
decl_falseE = falseE❘ # EXFALSO 1❙
decl_andE : {A,B,C} ⊦ A∧B ⟶ (⊦A ⟶ ⊦B ⟶ ⊦C) ⟶ ⊦C❘
= [A,B,C,p,q] q (andEl p) (andEr p)❘ # FROM 4 OBTAIN 5❙
decl_orE = orE❘ # SPLIT 4 CASE 5 CASE 6 prec -10050❙
decl_impI = impI ❘ # SUPPOSE 1 3 prec 500❙
example: {A,B,C} ⊦ A∧B ⇒ ((B⇒C)∨C ⇒ C) ❘ = [A,B,C]
SUPPOSE (A∧B) [ab]▪
SUPPOSE ((B⇒C)∨C) [bc]▪
PROVE B BY (
FROM ab OBTAIN [a,b]▪
HAVE B BY b
)[b]▪
SPLIT bc
CASE [r] HAVE C BY ≪⊦C≫
CASE [r] HAVE C BY r
❙
example2: {A,B,C} ⊦ A∧B ⇒ ((B⇒C)∨C ⇒ C)❘ = [A,B,C] impI[p]impI[q]orE q ([r] impE r (andEr p)) ([r]r)❙
❚
import rules scala://lf.mmt.kwarc.info❚
theory ProofIrrelevance =
include ?PL❙
/T a rule that makes all terms of type ded F equal❙
rule rules?TermIrrelevanceRule ded❙
❚