# Re: [isabelle] Words in Markus document's, I don't understand

`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.
`
On 8/5/12 4:38 PM, Yannick Duchêne (Hibou57) wrote:

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.
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*