|Speaker:||Prof Jan von PLATO, University of Helsinki, Finland|
|Place:||Room B 101, Institute of Cybernetics, Akadeemia tee 21, Tallinn, Estonia|
|Time:||Friday, May 7, 2004, 11:00|
In sequent calculus in natural deduction style, any multiplicities of active formulas can appear in the premisses of logical rules. No structural rules are needed, because multiplicity zero corresponds to weakening and greater than one to contraction.
Sequent calculus in natural deduction style is applied to simplify and complete Gentzen's third (1938) consistency proof of arithmetic.