Email Gateway (Aug 19 2022 at 11:21): Email Gateway (Aug 19 2022 at 11:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
I'm trying to make some connections between logic vocabulary and Isar.
From https://en.wikipedia.org/wiki/Sequent, I get the sentence
On the other hand an empty antecedent is assumed to be true, i.e.,
|- Sigma means that Sigma follows without any assumptions...
I'm trying to determine the right connection between sequent assumptions
and the meta-logic operator "==>", and how to restate a proved theorem
with Isar, THM, to accurately represent the sequent ( |- THM).
Say I have a sequent (A, B |- C), then I'm wanting to say that the
following Isar is a correct translation of that sequent:
theorem
assumes A and B
shows C
For any theorem THM I've proved in Isar, I'm trying to trivially restate
it as a sequent, |- THM, but have the restatement have some meaning,
not be an exact restatement.
For example, say I prove this:
theorem iffIi_1:
assumes "A --> B" and "B --> A"
shows "A = B"
<proof>
I'd like to restate the theorem using the identifier iffIi_1, but as I
said above, I don't know how, so I restate it like this:
theorem iffIi_2:
"(A --> B) ==> (B --> A) ==> (A = B)"
by(rule iffIi)
Here, I want to say that this represents the sequent ( |- "(A --> B) ==>
(B --> A) ==> (A = B)" ).
I've been thinking that the statements of iffIi_1 and iffIi_2 must be
exactly the same, but now I try the following and it doesn't work:
theorem
assumes "A --> B" and "B --> A"
shows "A = B"
by(rule iffIi)
I had started thinking assumes "A --> B" and "B --> A" was synonymous
with "(A --> B) ==> (B --> A)".
Regards,
GB
Email Gateway (Aug 19 2022 at 11:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Basically, I'm trying to sync up sequents notation with equivalent Isar
syntax being used with Isabelle/HOL. I wouldn't care about sequents, but
sequents are something that's resorted to a lot in many logic textbooks.
This is where a textbook would come in handy: "Sequents as Implemented
in Isabelle/HOL using Isar Syntax, Along with Many Tedious Examples,
Both Trivial and Advanced, and Likewise for Natural Deduction as
Implemented in Isar, for the Working Unprofessional."
It would say, "Here's a sequent, and here's its equivalent form using
Isar in Isabelle/HOL. Here's another sequent, but this sequent is
difficult to state in Isar. Here's yet another sequent, and you really
can't express this sequent in Isar in Isabelle/HOL."
There's a 3 page section in isar-ref.pdf titled "The sequent caclulus",
page 201, which I guess will help me eventually figure it out.
It says,
For certain proofs in classical logic, it can not be called natural.
The sequent calculus, a generalization of natural deduction, is
easier to automate.
If Isabelle/HOL is completely formulated as natural deduction, then I
guess every Isar statement of Isabelle/HOL can be expressed as a sequent.
But then on page 203, there's a section titled "Simulating sequents by
natural deduction", and it says,
Isabelle can represent sequents directly, as in the object-logic LK.
But natural deduction is easier to work with, and most object-logics
employ it. Fortunately, we can simulate the sequent P1, ..., Pm |-
Q1, ..., Qn by the Isabelle formula P1 ==> ... ==> Pm ==> ~Q2 ==>
... ==> ~Qn ==> Q1 where the order of the assumptions and the choice
of Q1 are arbitrary.
Here, the fact that the word "simulating" is being used, and the use of
the phrase "Fortunately, we can simulate the sequent...", makes me think
that I can't simulate certain sequents in Isabelle/HOL using Isar.
Maybe the discussion on page 202 explaining the sequent analogue to the
(-->I) will help me figure it out. It gives the rule as
P, Lambda |- Delta, Q
--------------------------------- (-->R)
Lambda |- Delta, P --> Q
For any proved HOL theorem THM, I'm trying to figure out how to restate
THM as a sequent which requires no assumptions, and do it using Isar.
I start with something trivial:
theorem TrueTrue:
"True"
by(rule TrueI)
There doesn't appear to be any assumptions in TrueTrue, but there must
be some assumptions because TrueTrue has to be proved by TrueI, which is
not an exact restatement of TrueI, where TrueI resorts to using the
axiom refl:
lemma TrueI: "True"
unfolding True_def by (rule refl)
If TrueTrue is a theorem, then I say, "Surely I can express it as a
sequent. But what is the sequent, and what is it in Isar?"
I make an attempt to answer the question, but I use the sequent rule
(-->R) as a template.
I'm tempted to say the sequent is "|- True", but I say it's "|- True,
TrueI". In Isar I say the sequent is
theorem TrueTrue_Restate:
"True"
by(rule TrueTrue)
So I decide that TrueTrue_Restate is the sequent "|- True, TrueTrue",
with there being a subtle difference between "|- True, TrueTrue" and "|-
True, TrueI", with the difference being that TrueTrue_Restate is
TrueTrue proving itself, which means it's using no assumptions. Using
theorem names, it would be "|- TrueTrue, TrueI" versus "|- TrueTrue,
TrueTrue_Restate" == "|- TrueTrue".
But I'm jumping through hoops to try and fit sequent notation with Isar
syntax. I'm trying to use "theorem" along with "by" or "proof" to prove
that a theorem THM is a sequent of the form "|- P", meaning that it
doesn't require any assumptions to be true. If I can do that, it's
important. If I can't, it's not important.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:21):From: Gottfried Barrow <gottfried.barrow@gmx.com>
And saying things like that are best only said to one's self. Moving
sets of assumptions back and forth from the LHS and RHS of the
turnstile would indicate a fundamental misunderstanding of basic logic,
of which the remembering of former textbook quotes can sometimes help
correct. It might be better to modify the notation and say something like:
Please consider |- <i(conjI),a,a> => "[|A;B|] ==> A & B"...
But that's the basic idea. Trying to tie into standard notation without
abusing it any more than necessary. If it's still messed up, I should be
eventually figure out how to make it acceptable.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:26):From: Gottfried Barrow <gottfried.barrow@gmx.com>
The right search words are "sequent style natural deduction", or
something similar, and throw in an "isabelle" to find what's specific to
Isabelle, or ":
(Isabelle specific)
http://www.inf.ed.ac.uk/teaching/courses/ar/slides/index.html
(Rules of the Game link)
http://www.cogsys.wiai.uni-bamberg.de/teaching/ss07/hs_rc/
(Natural Deduction in ISABELLE: Single-step proofs based on Sequent
Notation link)
http://www.gdi.uni-bamberg.de/personnel/aguado/publications.htm
(Natural Deduction with Gentzen Sequents)
http://www.ling.ohio-state.edu/~scott/teaching/2012/winter/280/
(Section 2.2 A sequent calculus for natural deduction)
http://books.google.com/books/about/Logic_and_Computation.html?id=8cyTbKWDKqgC
I think HOL4 notation corrupted my mind with things like this: "|- !f g
x. (f o g) x = f(g x)"
And then from a 1990 Isabelle user's manual it says:
"Theorems and axioms can be regarded as rules with no premises, so
let us speak just of rules."
So if we can speak of theorems as things without premises, I should be
able to combine sequent notation with Isar syntax, like writing
|- "A ==> B ==> (A & B)", ConjI
and get away with it, so I can emphasize the things I want to emphasize,
where because by(intro conjI) is the single proof command needed, then
ConjI must be qualified to representative the premises needed to prove
"A ==> B ==> (A & B)".
You gotta have those basic logic books to keep you from going astray too
far, when you have to answer most of your own questions. I finally found
what must have been vaguely in my mind:
"Remark 1.12 Indeed, this example indicates that we may transform
any proof of /phi1, phi2, ..., phi_n |- psi/ in such a way into a
proof of the theorem
|- phi1 --> (phi2 -->..."
http://www.cs.bham.ac.uk/research/projects/lics/
I think I saw someone from the HOL4 group say something like that on
this list over a year ago, probably Ramana.
Regards,
GB
Email Gateway (Aug 19 2022 at 11:32):From: Makarius <makarius@sketis.net>
Isabelle/Pure has sequents in the manner of Natural Deduction (with single
conclusion) built-in, but they only serve foundational and implementation
purposes.
When you state
theorem
assumes A and B
show C
you are claiming A, B |- C. The proof may refer to A and B in that
context as local theorems.
Alternatively, you can play with local contexts and sequents derived
within them more directly (and without global goals getting in the way)
using Isar notepad:
notepad
begin
{
assume A and B
have C sorry
}
end
The following versions lets you peek at the internal sequent (using
postfix notation for the "antecedent" due to Larry); the slightly nested
proof fragment ensures that the hypothetical facts actually show up in the
result:
notepad
begin
note [[show_hyps]]
{
assume A and B
then have C apply - sorry
thm this -- "C [A, B]"
}
note A ⟹ B ⟹ C
end
After closing the block, the internal sequent is exported into the
enclosing context, discharging the assumptions and turning them into
visible Pure rule structure using ==>.
Likewise, the initial "theorem assumes A and B shows C" gives you the
exported rule "A ==> B ==> C", not its sequent.
As a user of Isabelle/Pure (and HOL as application within it), you should
never encounter the hypotheses of the internal sequents, only the exported
versions with explicit rule structure.
Makarius
Email Gateway (Aug 19 2022 at 11:33):From: Makarius <makarius@sketis.net>
That is a slightly different thing: "Sequent calculus" is meant here in
the classic sense, with multiple conclusions and rules that allow shifting
between assumptions and conclusions in the classic dual fashion. (Don't
show this to constructivists, they will find it unintuitive despite
Wikipedia saying "other intuitive explanations are possible, which are
classically equivalent".)
What Larry explains in that chapter is how to use Pure rules (with their
!! / ==> structure and single conclusion) to represent the idea behind
classical sequent calculus naturally. It all works out rather nicely in
the end, leading to proof tools like "fast" and "best" that where a big
thing in the early 1990-ies (with minimal implementation effort). A bit
later came "blast", with the same rule representation, but different
inferencing engine.
Nowadays people tend to appeal to more heavy gear: sledgehammer and metis
for reconstruction, but that is quite different technology and unrelated
to this thread.
Makarius
Email Gateway (Aug 19 2022 at 11:34):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Makarius,
Thanks for the explanation, and the tips. It sounds complicated, and
like we wouldn't want to be writing sequents that reflect accurately
what's happening at the low level.
I'll be using "using [[show_hyps]]" to look at what the assumptions are
for a given fact.
I'm interested in sequents notation as a means to add some concise,
high-level, more-explicit notation to natural deduction notation, one of
those notations being Fitch diagrams, but, in general, mixing sequent
notation with natural deduction notation as shown by the docs linked to
my last email.
So I start with the sequent conjunction introduction rule on page 38 of
Larry's "Logic and Computation":
The conjunction introduction rule becomes
Gamma |- A Delta |- B
-------------------------------
Gamma, Delta |- A & B
The conclusion depends upon every assumption of A and of B.
I try to stay as true as I can, but staying true becomes relative to the
Isar syntax available, and the fact that there are multiple ways to
state a theorem.
I define <i(conjI,a,a> to be a list in the manner of Gamma and Delta.
The onus is on the interested reader to figure out the details. After
all, Gamma and Delta aren't exactly loaded with details. It turns that
<i(conjI,a,a> also conveniently corresponds with the sequence of Isar
commands apply(intro conjI), apply(assumption), by(assumption).
At least to myself, I can now say things like, "Please consider |-
"[|A;B|] ==> A & B", <i(conjI,a,a>..."
Instead of, "Please consider the theorem "[|A;B|] ==> A & B" which is
proved by the sequence of commands apply(intro conjI),
apply(assumption), by(assumption).
That's the idea. The implementation will never be perfect, but it could
be useful as a part of other things, at least for a while. Backward
proofs are very concise, so this kind of things looks like it's matching
up very nicely with short backwards proofs. Forward, structured proofs
aren't that concise, so it wouldn't work for that. But it could work for
proof steps within a structured proof, and a backward proof also can
tell a person how to do a forward proof.
I attached a screen shot and a PDF showing my notation experiments.
Regards,
GB
130701_sequent_stuff.png
130701_sequent_stuff.pdf
Last updated: Nov 21 2024 at 12:39 UTC