Email Gateway (Aug 19 2022 at 08:31): Email Gateway (Aug 19 2022 at 08:31):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all,
Please, someone can help to understand some words in
http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.pdf ?
Page 27 (printed 12), these words:
“For example, existing formalizations of linear and modal
logics simulate sequent-calculus rules within the pure
natural deduction framework, which would result in slightly
impractical Isar proof texts.”
Well, I simply don't understand what I quoted above.
What does it mean? An example?
If I ever have other questions from the same document, I will post it in
this thread.
Email Gateway (Aug 19 2022 at 08:32):From: Elsa L Gunter <egunter@illinois.edu>
In Natural Deduction, one has a system of proof rules for constructing
proof trees for provable propositions. These trees are associated with
a "discharge" function labeling where in the proofs assumptions (open
leaves of the tree) are used. The rule for implication introduction is
usually written
A
:
:
B
-------
A --> B
meaning that in the construction of the proof tree of B, there are zero
or more occurrences of the assumption A (as leaves of the tree) that may
be assigned to be discharged at this node of the proof tree.
the discharge function may only discharge in accordance with rules
allowing it. Thus, among other things, an assumption can only be
discharged at a node that has the assumption as the end of a branch from
that node. Assumptions
The rules come in two forms: introduction and elimination. The rule
above is the introduction rule for implication. The elimination rule
for implication is
Q
:
:
P -> Q P R
R
A proof tree is incomplete unless all assumptions are discharged
somewhere in the tree. For example, from these we may build the
following (incomplete) proof tree:
------- ---
A --> B A B
--------------------(Imp elim, discharging B to prove B)
B
--------------------(Imp intro, discharging (A --> B)
( A --> B) --> B
This proof is incomplete because nowhere have we discharged A. It can
be understood as saying "if we know A, then we know (A --> B) --> B.
It can be completed as follows:
------- --- ---
A --> B A B
--------------------(Imp elim, discharging B to prove B)
B
---------------(Imp intro, discharging (A --> B)
(A --> B) --> B
---------------------(Imp intro, discharging A)
A --> ((A --> B) --> B)
A bit more infrastructure is needed to deal with variables if your logic
has quantifiers.
Sequent calculi are a different style of describing provability.
Instead of proving propositions, one proves sequents. A sequent is a
pair of collections of propositions, and may be thought of a asserting
"if everything on the right is true, then something on the left is true".
The rules for a sequent calculus usually include a collection of rules
for introducing operations on the left collection, a set of rules for
introducing operations on the right collection, a rule (often called
axiom) for introducing assumptions, and the "cut" rule. The "axiom" rule is
A |- A
The cut rule is frequently given as
Gamma |- Delta, A Sigma, A |- D1, ..., Dj
B1,..., Bm, C1, ..., Ca, Cb, ..., Ck |- A1 ,...Aa, Ab,..., An, D1,
..., Dj
Sample Left and RIght rules are
Gamma |- A, Delta Sigma, B, |- Pi
-------------------------------- (Left Implication)
Gamma, Sigma, A --> B |- Delta, Pi
Gamma, A |- Delta, B
---------------------- (Right Implication)
Gamma |- Delta, A --> B
In the above, A and B are propositions, while Gamma, Delta, Sigma, and
Pi are collections of propositions.
Various flavours arise depending upon whether the collection is a set,
list or multiset. For example, intuitionistic logic restricts the
collection on the right to having just one element. On can encode
sequent calculi in a natural deduction system by introducing an explicit
predicate "provable" taking a pair of collections, with an inductive
relation definition following the sequent rules.
Linear logic is a variant of logic having "linear" connectives,
restricting the "use" of propositions in proofs (linear implication can
only discharge a single instance of an assumption, for example).
Modal logics introduce "modality" operators including Box and Diamond.
Box may be read as "it is necessarily the case that" and Diamond may be
read as "it is possible that". Temporal logics can by and large be
viewed as an outgrowth of modal logic.
I hope this gives you a little better idea of what is being said in the
section of Wenzel's thesis you were trying to read. For a little more
in depth discussion, you might try the Wikipedia entries; they're not
too bad.
---Elsa
PS. I apologize for any and all typos and other gaffs in the above
description. I have not proofread it carefully. If you find anything
confusing, please ask for clarification.
Last updated: Apr 23 2024 at 08:19 UTC