Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
From MaRDI portal
Publication:3278334
DOI10.2307/2964334zbMath0098.24201OpenAlexW1524655177MaRDI QIDQ3278334
Publication date: 1960
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2964334
Related Items (39)
A criterion for admissibility of rules in the modal system S4 and intuitionistic logic ⋮ Admissible inference rules and semantic property of modal logics ⋮ Multiple Conclusion Rules in Logics with the Disjunction Property ⋮ Rudimentary Kripke models for the intuitionistic propositional calculus ⋮ Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective) ⋮ Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics ⋮ A semantics for \(\lambda \)Prolog ⋮ A Tableau Method for Checking Rule Admissibility in S4 ⋮ Uniform proofs as a foundation for logic programming ⋮ The ``relevance of intersection and union types ⋮ Rules admissible in transitive temporal logic \(\mathrm{T}_{\mathrm{S}4}\), sufficient condition ⋮ On unification and admissible rules in Gabbay-de Jongh logics ⋮ ON NON-MONOTONOUS PROPERTIES OF SOME CLASSICAL AND NONCLASSICAL PROPOSITIONAL PROOF SYSTEMS ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ Metacompleteness of substructural logics ⋮ On two problems of Harvey Friedman ⋮ Admissibility in positive logics ⋮ Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic ⋮ METAVALUATIONS ⋮ Admissible inference rules of modal WCP-logics ⋮ An explicit basis for \textit{WCP}-globally admissible inference rules ⋮ HEREDITARILY STRUCTURALLY COMPLETE POSITIVE LOGICS ⋮ Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus ⋮ UNIFICATION IN SUPERINTUITIONISTIC PREDICATE LOGICS AND ITS APPLICATIONS ⋮ The semantics of entailment omega ⋮ Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations \textit{Until} and \textit{Since} based on bundles of integer numbers, logical consecutions, deciding algorithms ⋮ Admissibility and refutation: some characterisations of intermediate logics ⋮ The Story of $$\gamma $$ γ ⋮ Admissible inference rules in the linear logic of knowledge and time \(\mathrm{LTK}_r\) with intransitive time relation ⋮ Linear temporal logic with until and next, logical consecutions ⋮ On specifications, subset types and interpretation of proposition in type theory ⋮ PRESERVATION OF ADMISSIBLE RULES WHEN COMBINING LOGICS ⋮ On the rules of intermediate logics ⋮ The admissible rules of \(\mathsf{BD}_2\) and \(\mathsf{GSc}\) ⋮ Hereditarily structurally complete superintuitionistic deductive systems ⋮ Failure of completeness in proof-theoretic semantics ⋮ Some applications of Gentzens second consistency proof ⋮ Extraction and verification of programs by analysis of formal proofs ⋮ On maximal intermediate predicate constructive logics
Cites Work
This page was built for publication: Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems
