A1 is not a conservative extension of S4 but of S5

1989 ◽  
Vol 18 (3) ◽  
pp. 321-323
Author(s):  
Michiro Kondo
Keyword(s):  
Conservative Extension

Relativized realizability in intuitionistic arithmetic of all finite types

1978 ◽  
Vol 43 (1) ◽  
pp. 23-44 ◽  
Author(s):  
Nicolas D. Goodman
Keyword(s):  
Extension Theorem ◽  
General Notion ◽  
Conservative Extension ◽  
First Order ◽  
New Information ◽  
Reflection Theorem ◽  
Order Arithmetic ◽  
Special Case ◽  
Dependent Choice ◽  
Intuitionistic Arithmetic

In this paper we introduce a new notion of realizability for intuitionistic arithmetic in all finite types. The notion seems to us to capture some of the intuition underlying both the recursive realizability of Kjeene [5] and the semantics of Kripke [7]. After some preliminaries of a syntactic and recursion-theoretic character in §1, we motivate and define our notion of realizability in §2. In §3 we prove a soundness theorem, and in §4 we apply that theorem to obtain new information about provability in some extensions of intuitionistic arithmetic in all finite types. In §5 we consider a special case of our general notion and prove a kind of reflection theorem for it. Finally, in §6, we consider a formalized version of our realizability notion and use it to give a new proof of the conservative extension theorem discussed in Goodman and Myhill [4] and proved in our [3]. (Apparently, a form of this result is also proved in Mine [13]. We have not seen this paper, but are relying on [12].) As a corollary, we obtain the following somewhat strengthened result: Let Σ be any extension of first-order intuitionistic arithmetic (HA) formalized in the language of HA. Let Σω be the theory obtained from Σ by adding functionals of finite type with intuitionistic logic, intensional identity, and axioms of choice and dependent choice at all types. Then Σω is a conservative extension of Σ. An interesting example of this theorem is obtained by taking Σ to be classical first-order arithmetic.

A linear conservative extension of Zermelo-Fraenkel set theory

Studia Logica ◽  
1996 ◽  
Vol 56 (3) ◽  
pp. 361-392 ◽  
Author(s):  
Masaru Shirahata
Keyword(s):  
Set Theory ◽  
Conservative Extension

scholarly journals Polymorphic Subtyping for Effect Analysis: The Integration

1996 ◽  
Vol 25 (501) ◽  
Author(s):  
Hanne Riis Nielson ◽  
Flemming Nielson ◽  
Torben Amtoft
Keyword(s):  
Type System ◽  
Common Type ◽  
Inference Algorithm ◽  
Conservative Extension ◽  
Effect Analysis

The integration of polymorphism (in style of the ML <kbd>let</kbd>-construct), subtyping, and effects (modelling assignment or communication) into one common type system has proved remarkably difficult. One line of research has succeeded in integrating polymorphism and subtyping; adding effects in a straightforward way results in a semantically unsound system. Another line of research has succeeded in integrating polymorphism, effects, and subeffecting; adding sybtyping in a straightforward way invalidaters the construction of the inference algorithm. This paper integrates all op polymorphism, effects, and sybtyping into an annotated type and effect system for Concurrent ML and shows that the resulting system is a conservative extension of the ML type system.

Designing Document SQL (DSQL)

2009 ◽  
Vol 20 (4) ◽  
pp. 26-53 ◽  
Author(s):  
Arijit Sengupta ◽  
V. Ramesh
Keyword(s):  
Ad Hoc ◽  
Query Language ◽  
Optimization Techniques ◽  
Order Logic ◽  
Conservative Extension ◽  
Tree Structures ◽  
First Order ◽  
Easy Integration ◽  
Query Semantics ◽  
Theoretical Foundations

This article presents DSQL, a conservative extension of SQL, as an ad-hoc query language for XML. The development of DSQL follows the theoretical foundations of first order logic, and uses common query semantics already accepted for SQL. DSQL represents a core subset of XQuery that lends well to optimization techniques, while at the same time allows easy integration into current databases and applications that useSQL. The intent of DSQL is not to replace XQuery, the current W3C recommended XML query language, but to serve as an ad-hoc querying frontend to XQuery. Further, the authors present proofs for important query language properties such as complexity and closure. An empirical study comparing DSQL and XQuery for the purpose of ad-hoc querying demonstrates that users perform better with DSQL for both flat and tree structures, in terms of both accuracy and efficiency.

Epistemic set theory is a conservative extension of intuitionistic set theory

1985 ◽  
Vol 50 (4) ◽  
pp. 895-902 ◽  
Author(s):  
R. C. Flagg
Keyword(s):  
Set Theory ◽  
Affirmative Answer ◽  
Conservative Extension ◽  
Successful Program ◽  
Power Set ◽  
Epistemic Notion ◽  
Intuitionistic Mathematics ◽  
Topological Boolean Algebra ◽  
Faithful Interpretation ◽  
Intuitionistic Set Theory

In [6] Gödel observed that intuitionistic propositional logic can be interpreted in Lewis's modal logic (S4). The idea behind this interpretation is to regard the modal operator □ as expressing the epistemic notion of “informal provability”. With the work of Shapiro [12], Myhill [10], Goodman [7], [8], and Ščedrov [11] this simple idea has developed into a successful program of integrating classical and intuitionistic mathematics.There is one question quite central to the above program that has remained open. Namely:Does Ščedrov's extension of the Gödel translation to set theory provide a faithful interpretation of intuitionistic set theory into epistemic set theory?In the present paper we give an affirmative answer to this question.The main ingredient in our proof is the construction of an interpretation of epistemic set theory into intuitionistic set theory which is inverse to the Gödel translation. This is accomplished in two steps. First we observe that Funayama's theorem is constructively provable and apply it to the power set of 1. This provides an embedding of the set of propositions into a complete topological Boolean algebra . Second, in a fashion completely analogous to the construction of Boolean-valued models of classical set theory, we define the -valued universe V(). V() gives a model of epistemic set theory and, since we use a constructive metatheory, this provides an interpretation of epistemic set theory into intuitionistic set theory.

Sign in / Sign up

Export Citation Format

Share Document