Skip to content

Research at St Andrews

Analyticity, balance and non-admissibility of Cut in Stoic Logic

Research output: Contribution to journalArticle


This paper shows that, for the Hertz-Gentzen Systems of 1933 (without Thinning), extended by a classical rule T1 (from the Stoics) and using certain axioms (also from the Stoics), all derivations are analytic: every cut formula occurs as a subformula in the cut’s conclusion. Since the Stoic cut rules are instances of Gentzen’s Cut rule of 1933, from this we infer the decidability of the propositional logic of the Stoics. We infer the correctness for this logic of a “relevance criterion” and of two “balance criteria”, and hence (in contrast to one of Gentzen’s 1933 results) that a particular derivable sequent has no derivation that is “normal” in the sense that the first premiss of each cut is cut-free. We also infer that Cut is not admissible in the Stoic system, based on the standard Stoic axioms, the T1 rule and the instances of Cut with just two antecedent formulae in the first premiss.


Original languageEnglish
Pages (from-to)375–397
Number of pages23
JournalStudia Logica
Issue number2
Early online date20 Apr 2018
Publication statusPublished - Apr 2019

    Research areas

  • Sequent, Analyticity, Stoic logic, Proof theory, Decidability, Relevance, Balance, Cut-admissibility

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Indefinite proof and inversions of syllogisms

    Dyckhoff, R., 2019, In : Bulletin of Symbolic Logic. 25, 2, p. 196-207 12 p.

    Research output: Contribution to journalArticle

  2. Contraction-free sequent calculi in intuitionistic logic: a correction

    Dyckhoff, R., Dec 2018, In : Journal of Symbolic Logic. 83, 4, p. 1680-1682 3 p.

    Research output: Contribution to journalArticle

  3. Intuitionistic decision procedures since Gentzen

    Dyckhoff, R., 5 May 2016, Advances in Proof Theory. Kahle, R., Strahm, T. & Studer, T. (eds.). Birkhäuser Basel, p. 245-267 (Progress in Computer Science and Applied Logic; vol. 28).

    Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

  4. POSIX lexing with derivatives of regular expressions (proof pearl)

    Ausaf, F., Dyckhoff, R. & Urban, C., 2016, Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Springer, p. 69-86 18 p. (Lecture Notes in Computer Science; vol. 9807).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related by journal

  1. General-elimination stability

    Jacinto, B. M. & Read, S. L., Apr 2017, In : Studia Logica. 105, 2, p. 361-405

    Research output: Contribution to journalArticle

  2. De Morgan algebras with a quasi-Stone operator

    Blyth, T. S., Fang, J. & Wang, L., Feb 2015, In : Studia Logica. 103, 1, p. 75-90 16 p.

    Research output: Contribution to journalArticle

  3. Revising Carnap's Semantic Conception of Modality

    Meadows, T., Jun 2012, In : Studia Logica. 100, 3, p. 497-515 19 p.

    Research output: Contribution to journalArticle

  4. First-Order da Costa Logic

    Priest, G. G., Feb 2011, In : Studia Logica. 97, 1, p. 183-198

    Research output: Contribution to journalArticle

Related by journal

  1. Studia Logica (Journal)

    Roy Dyckhoff (Editor)
    2004 → …

    Activity: Publication peer-review and editorial work typesEditor of research journal

ID: 252715248