Email Gateway (Aug 18 2022 at 19:47): Email Gateway (Aug 18 2022 at 19:47):From: Oleksandr Gavenko <gavenkoa@gmail.com>
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:
theory mylogic
imports Pure
begin
typedecl o
judgment
Trueprop :: "o => prop" ("(_)" 5)
consts
Imp :: "o \<Rightarrow> o \<Rightarrow> o" ("_ --> _" 40)
axiomatization where
ax1: "A --> (B --> A)" and
ax2: "(A --> (B --> C)) --> ((A --> B) --> (A --> C))"
axiomatization where
mp: "\<lbrakk>P; P-->Q\<rbrakk> \<Longrightarrow> Q"
lemma imp_refl: "A --> A"
apply(rule_tac P = "A-->(B-->A)" in mp)
apply(rule ax1)
apply(rule_tac P = "A-->((B-->A)-->A)" in mp)
apply(rule ax1)
apply(rule ax2)
done
lemma impI_from_assumption: "P ==> (Q --> P)"
apply(rule_tac P = "P" in mp)
apply(assumption)
apply(rule ax1)
done
lemma anything_imp_true: "B --> (A --> A)"
apply(rule impI_from_assumption)
apply(rule imp_refl)
done
lemma deduction_thm: "(P \<Longrightarrow> Q) \<Longrightarrow> (P --> Q)"
oops
end
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
'deduction_thm').
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?
Email Gateway (Aug 18 2022 at 19:48):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle is not a “meta-logical-framework". So you cannot perform induction over an inference system you introduce to it.
Larry Paulson
Email Gateway (Aug 18 2022 at 19:48):From: Randy Pollack <rpollack@inf.ed.ac.uk>
You can do meta logic of "deeply embedded" formal systems. Define the
syntax and derivations of your object system as datatypes and
inductive relations in (for example) isabelle HOL. Then you have the
power of induction over these representations.
However reasoning _within_ such deeply embedded systems is not vey
convenient unless you put effort into building tools.
Propositional logic should be simple. If your object system has
binding, look into using nominal isabelle. There are many examples of
reasoning about formalized object systems.
Randy
Email Gateway (Aug 18 2022 at 19:48):From: Oleksandr Gavenko <gavenkoa@gmail.com>
On 2012-05-20, Randy Pollack wrote:
You can do meta logic of "deeply embedded" formal systems. Define the
syntax and derivations of your object system as datatypes and
inductive relations in (for example) isabelle HOL. Then you have the
power of induction over these representations.Firstly thanks to Larry Paulson and Randy Pollack for answer...
I understand idea about "induction over these representations", and will try
to learn more on Isabelle to realise this idea...
However reasoning _within_ such deeply embedded systems is not vey
convenient unless you put effort into building tools.I want to notice that proofs in 'Pure' also is not convenient.
For example without deduction theorem I need make a lot of rut work...
I as say that I am newbie for Isabelle and so I do not understand what you
mean by saying "building tools"... Can you explain more? Is this mean to write
some SML support code?
Propositional logic should be simple. If your object system has
binding, look into using nominal isabelle. There are many examples of
reasoning about formalized object systems.By saying "nominal isabelle" do you mean:
http://isabelle.in.tum.de/nominal/ ??
I would glad if someone point me for examples of "reasoning about formalized
object systems" as I new to this field and don't know from what to start...
Email Gateway (Aug 18 2022 at 19:49):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
We have a paper in LPAR 2010 (Dawson & Gore) which gives a couple of
pages on deep embeddings, what (we think) that means, etc. Email me if
you want me to send you a copy.
The comment that
reasoning _within_ such deeply embedded systems is not vey
convenient unless you put effort into building tools
reflects the fact that instead of proving something, you are proving that it is provable. Fortunately the extra effort is just repetitive grunt work for which Isabelle's SML user interface is ideally suited. Unfortunately you will no doubt have been led to believe that the SML user interface is not the way to go in using Isabelle.
Cheers,
Jeremy
Oleksandr Gavenko wrote:
Email Gateway (Aug 18 2022 at 19:50):From: Lawrence Paulson <lp15@cam.ac.uk>
Normally, if you want to perform deductions that involve a set of assumptions, as the deduction theorem allows, you formalise a sequent calculus or alternatively a natural deduction system, of which several examples are already distributed with Isabelle.
Most of our recent documentation focuses on how to use Isabelle/HOL, which is possibly not relevant to your application. What sort of calculus do you want to formalise, And with what application in mind?
Larry Paulson
Email Gateway (Aug 18 2022 at 19:50):From: Makarius <makarius@sketis.net>
Why? Isabelle/ML and Isabelle/Isar are both the main Isabelle "user
interface", independently of the number of users who have ever writting
their own proof tools in ML. See also the command 'method_setup' in the
isar-ref manual to get started, and maybe search for some of its uses in
the Isabelle library.
Also note that in Isabelle/jEdit you get IDE functionality for both ML and
Isar source language, but of course you have to put your ML into the
proper formal context within a theory.
Makarius
Email Gateway (Aug 18 2022 at 19:53):From: Oleksandr Gavenko <gavenkoa@gmail.com>
On 2012-05-21, Lawrence Paulson wrote:
Normally, if you want to perform deductions that involve a set of
assumptions, as the deduction theorem allows, you formalise a sequent
calculus or alternatively a natural deduction system, of which several
examples are already distributed with Isabelle.Most of our recent documentation focuses on how to use Isabelle/HOL, which
is possibly not relevant to your application. What sort of calculus do you
want to formalise,
Sequent calculus.
And with what application in mind?
There are many propositional logic axiom sets (and most uses Modus Ponens as
deduction rule) for which stated that they lie in specified type of logic but
proofs are lost or unaccessible. For example (if I am correct) this paper
Łukasiewicz, Jan; Tarski, Alfred, "Untersuchungen über den Aussagenkalkül"
(I read English translation in "Logic, Semantics, Metamathematics: Papers from
1923 to 1938" by Alfred Tarski) state that these axioms:
CCpqCCqrCpr
CCNppp
CpCNpq
with MP allow to proof any true propositional sentence (without presenting
proof). This was shown during seminars at 1920-1930.
My goal is to prove theorems in this system which have well known properties.
That shown that original axiom set have same properties...
I decide use 'Pure' logic to record proofs in propositional logic by using MP
and substitution rules. This may be wrong decision but this solution is easy
to find in Isabelle sources (I use 'src/FOL/IFOL.thy' as start point).
After some time of work I explore that I make many routine work. For example
if I prove this statement:
A --> (B --> A)
A --> (B --> C)) --> ((A --> B) --> (A --> C))
I can use deduction theorem in human proofs to simplify my work. But how tell
to Isabelle that if I prove:
A ==> B
then it is possible to prove "A --> B" by modifying "A ==> B" proof?
Email Gateway (Aug 18 2022 at 19:54):From: Lawrence Paulson <lp15@cam.ac.uk>
Almost certainly, you should be formalising these deductive formalisms inductively in Isabelle/HOL, not in Pure. Then you will be able to prove their meta-theoretic properties (their proof theory) straightforwardly.
The deduction theorem inspires the sequent calculus, but it doesn't give you the sequent calculus. The sequent calculus is a formalism in its own right and should be formalised as such directly.
Larry Paulson
Email Gateway (Aug 18 2022 at 19:58):From: Joao Marcos <botocudo@gmail.com>
The question seems not to be without interest. Has anyone in the list
ever proved in Isabelle the meta-deduction theorem for, say, the
implicational fragment of intuitionistic Hilbert calculus?
JM
Last updated: Nov 21 2024 at 12:39 UTC