scholarly journals A note on Humberstone's constant Ω

2021 ◽  
Vol 56 ◽  
pp. 75-99
Author(s):  
Satoru Niki ◽  
Hitoshi Omori

We investigate an expansion of positive intuitionistic logic obtained by adding a constant Ω introduced by Lloyd Humberstone. Our main results include a sound and strongly complete axiomatization, some comparisons to other expansions of intuitionistic logic obtained by adding actuality and empirical negation, and an algebraic semantics. We also brie y discuss its connection to classical logic.

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 385
Author(s):  
Hyeonseung Im

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.


2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka

International audience In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment $\{ \to ,\vee ,\bot \}$ of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.


1970 ◽  
Vol 35 (4) ◽  
pp. 529-534 ◽  
Author(s):  
Melvin Fitting

There are well-known embeddings of intuitionistic logic into S4 and of classical logic into S5. In this paper we give a related embedding of (first order) classical logic directly into (first order) S4, with or without the Barcan formula. If one reads the necessity operator of S4 as ‘provable’, the translation may be roughly stated as: truth may be replaced by provable consistency. A proper statement will be found below. The proof is based ultimately on the notion of complete sequences used in Cohen's technique of forcing [1], and is given in terms of Kripke's model theory [3], [4].


Author(s):  
Walter Carnielli ◽  
Abilio Rodrigues

Abstract From the technical point of view, philosophically neutral, the duality between a paraconsistent and a paracomplete logic (for example intuitionistic logic) lies in the fact that explosion does not hold in the former and excluded middle does not hold in the latter. From the point of view of the motivations for rejecting explosion and excluded middle, this duality can be interpreted either ontologically or epistemically. An ontological interpretation of intuitionistic logic is Brouwer’s idealism; of paraconsistency is dialetheism. The epistemic interpretation of intuitionistic logic is in terms of preservation of constructive proof; of paraconsistency is in terms of preservation of evidence. In this paper, we explain and defend the epistemic approach to paraconsistency. We argue that it is more plausible than dialetheism and allows a peaceful and fruitful coexistence with classical logic.


Author(s):  
Peter Pagin

The law of excluded middle (LEM) says that every sentence of the form A∨¬A (‘A or not A’) is logically true. This law is accepted in classical logic, but not in intuitionistic logic. The reason for this difference over logical validity is a deeper difference about truth and meaning. In classical logic, the meanings of the logical connectives are explained by means of the truth tables, and these explanations justify LEM. However, the truth table explanations involve acceptance of the principle of bivalence, that is, the principle that every sentence is either true or false. The intuitionist does not accept bivalence, at least not in mathematics. The reason is the view that mathematical sentences are made true and false by proofs which mathematicians construct. On this view, bivalence can be assumed only if we have a guarantee that for each mathematical sentence, either there is a proof of the truth of the sentence, or a proof of its falsity. But we have no such guarantee. Therefore bivalence is not intuitionistically acceptable, and then neither is LEM. A realist about mathematics thinks that if a mathematical sentence is true, then it is rendered true by the obtaining of some particular state of affairs, whether or not we can know about it, and if that state of affairs does not obtain, then the sentence is false. The realist further thinks that mathematical reality is fully determinate, in that every mathematical state of affairs determinately either obtains or does not obtain. As a result, the principle of bivalence is taken to hold for mathematical sentences. The intuitionist is usually an antirealist about mathematics, rejecting the idea of a fully determinate, mind-independent mathematical reality. The intuitionist’s view about the truth-conditions of mathematical sentences is not obviously incompatible with realism about mathematical states of affairs. According to Michael Dummett, however, the view about truth-conditions implies antirealism. In Dummett’s view, a conflict over realism is fundamentally a conflict about what makes sentences true, and therefore about semantics, for there is no further question about, for example, the existence of a mathematical reality than as a truth ground for mathematical sentences. In this vein Dummett has proposed to take acceptance of bivalence as actually defining a realist position. If this is right, then both the choice between classical and intuitionistic logic and questions of realism are fundamentally questions of semantics, for whether or not bivalence holds depends on the proper semantics. The question of the proper semantics, in turn, belongs to the theory of meaning. Within the theory of meaning Dummett has laid down general principles, from which he argues that meaning cannot in general consist in bivalent truth-conditions. The principles concern the need for, and the possibility of, manifesting one’s knowledge of meaning to other speakers, and the nature of such manifestations. If Dummett’s argument is sound, then bivalence cannot be justified directly from semantics, and may not be justifiable at all.


1973 ◽  
Vol 38 (2) ◽  
pp. 315-319 ◽  
Author(s):  
Harvey Friedman

Let ZF be the usual Zermelo-Fraenkel set theory formulated without identity, and with the collection axiom scheme. Let ZF−-extensionality be obtained from ZF by using intuitionistic logic instead of classical logic, and dropping the axiom of extensionality. We give a syntactic transformation of ZF into ZF−-extensionality.Let CPC, HPC respectively be classical, intuitionistic predicate calculus without identity, whose only homological symbol is ∈. We use the ~ ~-translation, a basic tool in the metatheory of intuitionistic systems, which is defined byThe two fundamental lemmas about this ~ ~ -translation we will use areFor proofs, see Kleene [3, Lemma 43a, Theorem 60d].This - would provide the desired syntactic transformation at least for ZF into ZF− with extensionality, if A− were provable in ZF− for each axiom A of ZF. Unfortunately, the ~ ~-translations of extensionality and power set appear not to be provable in ZF−. We therefore form an auxiliary classical theory S which has no extensionality and has a weakened power set axiom, and show in §2 that the ~ ~-translation of each axiom of Sis provable in ZF−-extensionality. §1 is devoted to the translation of ZF in S.


1973 ◽  
Vol 38 (4) ◽  
pp. 613-627 ◽  
Author(s):  
Melvin Fitting

In classical logic a collection of sets of statements (or equivalently, a property of sets of statements) is called a consistency property if it meets certain simple closure conditions (a definition is given in §2). The simplest example of a consistency property is the collection of all consistent sets in some formal system for classical logic. The Model Existence Theorem then says that any member of a consistency property is satisfiable in a countable domain. From this theorem many basic results of classical logic follow rather simply: completeness theorems, the compactness theorem, the Lowenheim-Skolem theorem, and the Craig interpolation lemma among others. The central position of the theorem in classical logic is obvious. For the infinitary logic the Model Existence Theorem is even more basic as the compactness theorem is not available; [8] is largely based on it.In this paper we define appropriate notions of consistency properties for the first-order modal logics S4, T and K (without the Barcan formula) and for intuitionistic logic. Indeed we define two versions for intuitionistic logic, one deriving from the work of Gentzen, one from Beth; both have their uses. Model Existence Theorems are proved, from which the usual known basic results follow. We remark that Craig interpolation lemmas have been proved model theoretically for these logics by Gabbay ([5], [6]) using ultraproducts. The existence of both ultra-product and consistency property proofs of the same result is a common phenomena in classical and infinitary logic. We also present extremely simple tableau proof systems for S4, T, K and intuitionistic logics, systems whose completeness is an easy consequence of the Model Existence Theorems.


2014 ◽  
Vol 25 (1) ◽  
pp. 83-134 ◽  
Author(s):  
NORIHIRO KAMIDE

In this paper, we prove some embedding theorems for LTL (linear-time temporal logic) and its variants:viz. some generalisations, extensions and fragments of LTL. Using these embedding theorems, we give uniform proofs of the completeness, cut-elimination and/or decidability theorems for LTL and its variants. The proposed embedding theorems clarify the relationships between some LTL-variations (for example, LTL, a dynamic topological logic, a fixpoint logic, a spatial logic, Prior's logic, Davies' logic and an NP-complete LTL) and some traditional logics (for example, classical logic, intuitionistic logic and infinitary logic).


Author(s):  
Ravikumar Bandaru ◽  
Arsham Borumand Saeid ◽  
Young Bae Jun

Hilbert algebras are important tools for certain investigations in intuitionistic logic and other non-classical logic and as a generalization of Hilbert algebra a new algebraic structure, called a GE-algebra (generalized exchange algebra), is introduced and studied its properties. We consider filters, upper sets and congruence kernels in a GE-algebra. We also characterize congruence kernels of transitive GE-algebras.


Sign in / Sign up

Export Citation Format

Share Document