scientific article

Publication date: 1987

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

proof theory higher order logic second order functionals recursive ordinals no-counterexample interpretation applications of reflection principles omega-derivations strong normalizability proofs

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Proof theory and constructive mathematics (03Fxx)

Related Items

From axioms to synthetic inference rules via focusing, Provability algebras and proof-theoretic ordinals. I, Minimal bad sequences are necessary for a uniform Kruskal theorem, Proofs with monotone cuts, Cut elimination for the unified logic, Sharpened lower bounds for cut elimination, Is cut-free logic fit for unrestricted abstraction?, A note on the $\omega$-incompleteness formalization, A finite analog to the Löwenheim-Skolem theorem, MELL in the calculus of structures, A comparison of well-known ordinal notation systems for $\varepsilon _{0}$, Computational adequacy for recursive types in models of intuitionistic set theory, Open Questions in Reverse Mathematics, Totality in applicative theories, Normal functors, power series and $\lambda$-calculus, Herbrand analyses, The metamathematics of scattered linear orderings, Cut-elimination and interpolation for $\Omega$-logic, Derivatives of normal functions and $\omega $-models, On schematological equivalence of partially interpreted dataflow networks, A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations, A cut-free calculus for second-order Gödel logic, Strong normalization theorem for a constructive arithmetic with definition by transfinite recursion and bar induction, Les premiers recursivement inaccessible et Mahlo et la theorie des dilatateurs, Cut elimination, identity elimination, and interpolation in super-Belnap logics, One step is enough, Higher-level inferences in the strong-Kleene setting: a proof-theoretic approach, On the strong normalisation of intuitionistic natural deduction with permutation-conversions, Proof theory of paraconsistent weak Kleene logic, Languages of logic and their applications, The omega-rule interpretation of transfinite provability logic, A proof-theoretic investigation of a logic of positions, The maximal linear extension theorem in second order arithmetic, The provably terminating operations of the subsystem PETJ of explicit mathematics, Neutral free logic: motivation, proof theory and models, Some uses of dilators in combinatorial problems. III: Independence results by means of decreasing F-sequences (F weakly finite dilator), Alpha conversion, conditions on variables and categorical logic, The Church-Fitch knowability paradox in the light of structural proof theory, Theories with self-application and computational complexity., Hypersequent Calculi for S5: The Methods of Cut Elimination, The Reverse Mathematics of wqos and bqos, Finite presentability of strongly finite dilators, Extraction of expansion trees, What is a Paraconsistent Logic?, On Feferman's operational set theory \textsf{OST}, Higman’s Lemma and Its Computational Content, CERES: An analysis of Fürstenberg's proof of the infinity of primes, Tarskian and Kripkean truth, One-step modal logics, intuitionistic and classical. I, The Veblen functions for computability theorists, Bounded arithmetic for NC, ALogTIME, L and NL, Proof systems for infinite behaviours, An order-theoretic characterization of the Howard-Bachmann-hierarchy, Existential instantiation and normalization in sequent natural deduction, Cut as Consequence, Preface to the special volume, 2-sequent calculus: A proof theory of modalities, Constructive logics. I: A tutorial on proof systems and typed $\lambda$- calculi, An approach to infinitary temporal proof theory, Fixed points in Peano arithmetic with ordinals, Cut-elimination: syntax and semantics, A proof-theoretic characterization of the basic feasible functionals, Singularities, expanders and topology of maps. II: From combinatorics to topology via algebraic isoperimetry, Paraconsistent informational logic, On the form of witness terms, $\Pi_1^1$-comprehension as a well-ordering principle, CERES in higher-order logic, Common knowledge does not have the Beth property, Proof theory and ordinal analysis, Abstract deduction and inferential models for type theory, Notation systems for infinitary derivations, Valuations: bi, tri, and tetra, Deduction chains for common knowledge, The metamathematics of ergodic theory, Generating plans in linear logic. I: Actions as proofs, On the non-confluence of cut-elimination, The implicit commitment of arithmetical theories and its semantic core, A hierarchy of classical and paraconsistent logics, $\Pi_ 2^ 1$-logic and uniformization in the analytical hierarchy, A logic for quantum register measurements, Proof-theoretic strengths of the well-ordering principles, Full operational set theory with unbounded existential quantification and power set, Reverse mathematics and well-ordering principles: a pilot study, Paraconsistency and the need for infinite semantics, Validities, antivalidities and contingencies: a multi-standard approach, Truth and the philosophy of mathematics, Completeness of the primitive recursive $\omega $-rule, Strong normalization property for second order linear logic, Well-ordering proofs for Martin-Löf type theory, Some results on cut-elimination, provable well-orderings, induction and reflection, Streams and strings in formal proofs., Gentzen-type systems, resolution and tableaux, Applicative theories for logarithmic complexity classes, Combinatory reduction systems: Introduction and survey, Systems of explicit mathematics with non-constructive $\mu$-operator. I, On the proof theory of infinitary modal logic, The complexity of predicate default logic over a countable domain, Reverse mathematics and ordinal exponentiation, Towards a semantic characterization of cut-elimination, Sequent-calculi for metainferential logics, Linear Logic Properly Displayed, Basic logic: reflection, symmetry, visibility, The cost of a cycle is a square, Ordinal inequalities, transfinite induction, and reverse mathematics, Well-Ordering Principles in Proof Theory and Reverse Mathematics, The role of parameters in bar rule and bar induction, Intuitionistic three-valued logic and logic programming, About some symmetries of negation, Derived sequences and reverse mathematics, Reducing ω-model reflection to iterated syntactic reflection, The (Greatest) Fragment of Classical Logic that Respects the Variable-Sharing Principle (in the FMLA-FMLA Framework), Well ordering principles for iterated $\Pi^1_1$-comprehension, (I can't get no) antisatisfaction, (Meta)inferential levels of entailment beyond the Tarskian paradigm, Substructural logics, pluralism and collapse, A note on ordinal exponentiation and derivatives of normal functions, PREDICATIVE COLLAPSING PRINCIPLES, A FULLY CLASSICAL TRUTH THEORY CHARACTERIZED BY SUBSTRUCTURAL MEANS, On the logical strength of the better quasi order with three elements, Functorial Fast-Growing Hierarchies, On the metainferential solution to the semantic paradoxes, The conservation theorem for differential nets, A two‐dimensional metric temporal logic, Natural deduction calculi for classical and intuitionistic S5, Anti-exceptionalism, truth and the BA-plan, Cut Elimination for Extended Sequent Calculi, Computable aspects of the Bachmann–Howard principle, Unnamed Item, TWO (OR THREE) NOTIONS OF FINITISM, HOW STRONG ARE SINGLE FIXED POINTS OF NORMAL FUNCTIONS?, ST, LP and Tolerant Metainferences, Minimal invariant spaces in formal topology, Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken, WELL ORDERING PRINCIPLES AND -STATEMENTS: A PILOT STUDY, Cut-elimination and redundancy-elimination by resolution, Elementary patterns of resemblance, A family of metainferential logics, Asymptotic cyclic expansion and bridge groups of formal proofs, Cycling in proofs and feasibility, On the No-Counterexample Interpretation, A categorical construction of Bachmann–Howard fixed points, 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent, Paraconsistent conjectural deduction based on logical entropy measures I: C-systems as non-standard inference framework, A practical implementation of simple consequence relations using inductive definitions, Well-ordering Principles, ω-models and $$ \varPi_{1}^{1} $$-comprehension, Effectively dense Boolean algebras and their applications