Commit 74e50ed9 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Basic support for classical reasoning

parent c4b8ac15
#NAME classical.
(; We take the law of excluded middle as axiom. ;)
excluded_middle : P : fol.prop -> fol.proof (fol.or P (fol.not P)).
(; From this we can derive equivalent and weaker classical principles
but it will be either do so once we have a tactic language.
See ../meta/classical_cert.dk for some certificate combinators and
classical theorems. ;)
#NAME classical_cert.
(; Customization of Emacs mode for Dedukti: this file is not linear
and requires a path extended with "../fol".
(setq-local dedukti-check-options '("-nc" "-nl" "-I" "../fol"))
(setq-local dedukti-compile-options '("-nc" "-e" "-nl" "-I" "../fol"))
;)
(; Classical theorems and certificate combinators ;)
(; Reason by case on a the truth of a formula (using excluded middle) ;)
def prop_case (P : fol.prop) :
cert.certificate -> cert.certificate -> cert.certificate
:=
cert.destruct_or P (fol.not P)
(cert.exact
(fol.or P (fol.not P))
(classical.excluded_middle P)).
(; Double-negation elimination ;)
(; Remark: in first-order logic, this is a theorem scheme since we
cannot quantify over formulae ;)
def nnpp (P : fol.prop) : fol.proof (fol.imp (fol.not (fol.not P)) P)
:=
cert.cert_run (fol.imp (fol.not (fol.not P)) P)
(cert.intro
(; ¬¬P ⊢ P ;)
(prop_case P
(; ¬¬P, P ⊢ P ;)
cert.assumption
(; ¬¬P, ¬P ⊢ P ;)
cert.absurd)).
(; Use double-negation elimination to do a proof by contradiction.
(contradict c) proves Γ ⊢ P if c proves Γ, ¬P ⊢ ⊥ ;)
def contradict (c : cert.certificate) : cert.certificate :=
cert.with_goal (P => cert.refine (fol.not (fol.not P)) P (nnpp P) (cert.intro c)).
(; De Morgan laws ;)
def not_and_is_or_not (A : fol.prop) (B : fol.prop) :
fol.proof (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))
:=
cert.cert_run (fol.imp (fol.not (fol.and A B)) (fol.or (fol.not A) (fol.not B)))
(cert.intro
(; ¬∧ ⊢ ∨¬ ;)
(contradict
(; ¬∧, ¬∨¬ ⊢ ⊥;)
(cert.destruct_imp
(fol.and A B)
fol.false
(; ¬∧, ¬∨¬ ⊢ ¬∧ ;)
cert.assumption
(; ¬∧, ¬∨¬ ⊢ ∧ ;)
(cert.split
(; ¬∧, ¬∨¬ ⊢ A ;)
(contradict
(; ¬∧, ¬∨¬, ¬A ⊢ ⊥ ;)
(cert.destruct_imp
(fol.or (fol.not A) (fol.not B))
fol.false
(; ¬∧, ¬∨¬, ¬A ⊢ ¬∨¬ ;)
cert.assumption
(; ¬∧, ¬∨¬, ¬A ⊢ ∨¬ ;)
(cert.left cert.assumption)
(; ¬∧, ¬∨¬, ¬A, ⊥ ⊢ ⊥ ;)
cert.assumption))
(; ¬∧, ¬∨¬ ⊢ B ;)
(contradict
(cert.destruct_imp
(fol.or (fol.not A) (fol.not B))
fol.false
cert.assumption
(cert.right cert.assumption)
cert.assumption)))
(; ¬∧, ¬∨¬, ⊥ ⊢ ⊥ ;)
cert.assumption))).
(; Same for quantifiers ;)
def not_all_is_ex_not (A : fol.type) (P : fol.term A -> fol.prop) :
fol.proof (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
:=
tac.run (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
(cert.run (fol.imp (fol.not (fol.all A (x => P x)))
(fol.ex A (x : fol.term A => fol.not (P x))))
cert.nil_ctx
(cert.intro
(; ¬∀ ⊢ ∃¬ ;)
(contradict
(; ¬∀, ¬∃¬ ⊢ ⊥ ;)
(cert.destruct_imp (fol.all A (x => P x)) fol.false
cert.assumption
(cert.intro
(; ¬∀, ¬∃¬, x ⊢ P x ;)
(contradict
(; ¬∀, ¬∃¬, x, ¬P x ⊢ ⊥ ;)
(cert.destruct_imp
(fol.ex A (x => fol.not (P x)))
fol.false
cert.assumption
(; ¬∀, ¬∃¬, x, ¬P x ⊢ ∃¬ ;)
(cert.with_variable
(A => a => cert.exists A a cert.assumption))
cert.assumption)))
cert.assumption)))).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment