An intuitionistic formula hierarchy based on high‐school identities
From MaRDI portal
Publication:5108846
DOI10.1002/malq.201700047OpenAlexW3105111019MaRDI QIDQ5108846
Danko Ilik, Taus Brock-Nannestad
Publication date: 6 May 2020
Published in: Mathematical Logic Quarterly (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1601.04876
Constructive and recursive analysis (03F60) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03) Subsystems of classical logic (including intuitionistic logic) (03B20)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Delimited control operators prove double-negation shift
- Syntactic preservation theorems for intuitionistic predicate logic
- Bounds for cut elimination in intuitionistic propositional logic
- Remarks on isomorphisms in typed lambda calculi with empty and sum types
- Sovability of the problem of deducibility in LJ for a class of formulas not containing negative occurrences of quantifiers
- The saga of the high school identities
- Admissibility of structural rules for contraction-free systems of intuitionistic logic
- Proofs and Computations
- Focusing and Polarization in Intuitionistic Logic
- On formulas of one variable in intuitionistic propositional calculus
- Implicational complexity in intuitionistic arithmetic
- Logic Programming with Focusing Proofs in Linear Logic
- Contraction-free sequent calculi for intuitionistic logic
- Fragments of Heyting arithmetic
- Symmetric normalisation for intuitionistic logic
- Axioms and decidability for type isomorphism in the presence of sums
- Identity of Proofs Based on Normalization and Generality
- A system of interaction and structure
- The exp-log normal form of types: decomposing extensional equality and representing terms compactly
- Automating Coherent Logic
- A new algorithm for derivability in the constructive propositional calculus
- On the Mints Hierarchy in First-Order Intuitionistic Logic
