[isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- From: Oleksandr Gavenko <gavenkoa at gmail.com>
- Date: Sat, 19 May 2012 22:40:50 +0300
- Cancel-lock: sha1:b4B/KMx+EIQ4aRzNYRvGQNLgI80=
- Organization: At home.
- User-agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux)
I am newbie to Isabelle and I have hobby interest to make proofs in different
propositional deduction systems (sorry if my English too bad).
I start from 'src/FOL/IFOL.thy' and make such code:
Trueprop :: "o => prop" ("(_)" 5)
Imp :: "o \<Rightarrow> o \<Rightarrow> o" ("_ --> _" 40)
ax1: "A --> (B --> A)" and
ax2: "(A --> (B --> C)) --> ((A --> B) --> (A --> C))"
mp: "\<lbrakk>P; P-->Q\<rbrakk> \<Longrightarrow> Q"
lemma imp_refl: "A --> A"
apply(rule_tac P = "A-->(B-->A)" in mp)
apply(rule_tac P = "A-->((B-->A)-->A)" in mp)
lemma impI_from_assumption: "P ==> (Q --> P)"
apply(rule_tac P = "P" in mp)
lemma anything_imp_true: "B --> (A --> A)"
lemma deduction_thm: "(P \<Longrightarrow> Q) \<Longrightarrow> (P --> Q)"
Set of axioms take straight possibility to prove deduction theorem like this
done in any textbook for math logic and it can be formalised in Isabelle (see
Lemma 'impI_from_assumption' shown that simple meta-theorem can be proved and
can be used in next proofs.
Is it possible to prove 'deduction_thm' and how to do this?
This archive was generated by a fusion of
Pipermail (Mailman edition) and