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.