Switch to: References

Citations of:

Fragments of HA based on b-induction

Kai F. Wehmeier

Archive for Mathematical Logic 37 (1):37-50 (1998)

Add citations

You must login to add citations.

Theoremizing Yablo's Paradox.Ahmad Karimi & Saeed Salehi - manuscriptdetails To counter a general belief that all the paradoxes stem from a kind of circularity (or involve some self--reference, or use a diagonal argument) Stephen Yablo designed a paradox in 1993 that seemingly avoided self--reference. We turn Yablo's paradox, the most challenging paradox in the recent years, into a genuine mathematical theorem in Linear Temporal Logic (LTL). Indeed, Yablo's paradox comes in several varieties; and he showed in 2004 that there are other versions that are equally paradoxical. Formalizing these versions (...) Download Export citation Bookmark
Partially-Elementary Extension Kripke Models: A Characterization and Applications.Tomasz Połacik - 2006 - Logic Journal of the IGPL 14 (1):73-86.details A Kripke model for a first order language is called a partially-elementary extension model if its accessibility relation is not merely a submodel relation but a stronger relation of being an elementary submodel with respect to some class of fromulae. As a main result of the paper, we give a characterization of partially-elementary extension Kripke models. Throughout the paper we exploit a generalized version of the hierarchy of first order formulae introduced by W. Burr. We present some applications of partially-elementary (...) Download Export citation Bookmark 3 citations
Extracting Algorithms from Intuitionistic Proofs.Fernando Ferreira & António Marques - 1998 - Mathematical Logic Quarterly 44 (2):143-160.details This paper presents a new method - which does not rely on the cut-elimination theorem - for characterizing the provably total functions of certain intuitionistic subsystems of arithmetic. The new method hinges on a realizability argument within an infinitary language. We illustrate the method for the intuitionistic counterpart of Buss's theory Smath image, and we briefly sketch it for the other levels of bounded arithmetic and for the theory IΣ1. Download Export citation Bookmark 1 citation
Homomorphisms and chains of Kripke models.Morteza Moniri & Mostafa Zaare - 2011 - Archive for Mathematical Logic 50 (3-4):431-443.details In this paper we define a suitable version of the notion of homomorphism for Kripke models of intuitionistic first-order logic and characterize theories that are preserved under images and also those that are preserved under inverse images of homomorphisms. Moreover, we define a notion of union of chain for Kripke models and define a class of formulas that is preserved in unions of chains. We also define similar classes of formulas and investigate their behavior in Kripke models. An application to (...) Download Export citation Bookmark
Quick cut-elimination for strictly positive cuts.Toshiyasu Arai - 2011 - Annals of Pure and Applied Logic 162 (10):807-815.details In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic. Download Export citation Bookmark 3 citations

1