On a second order propositional operator in intuitionistic logic

Studia Logica ◽  
1981 ◽  
Vol 40 (2) ◽  
pp. 113-139 ◽  
Author(s):  
A. S. Troelstra
Keyword(s):  
Intuitionistic Logic ◽  
Second Order ◽  
Propositional Operator

scholarly journals COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS

2018 ◽  
Vol 11 (3) ◽  
pp. 507-518
Author(s):  
PHILIP KREMER
Keyword(s):  
Modal Logic ◽  
Intuitionistic Logic ◽  
Second Order ◽  
Topological Semantics ◽  
First Order ◽  
Propositional Modal Logic ◽  
Propositional Quantifiers ◽  
Modal Logic S4 ◽  
Natural Way

AbstractWe add propositional quantifiers to the propositional modal logic S4 and to the propositional intuitionistic logic H, introducing axiom schemes that are the natural analogs to axiom schemes typically used for first-order quantifiers in classical and intuitionistic logic. We show that the resulting logics are sound and complete for a topological semantics extending, in a natural way, the topological semantics for S4 and for H.

ON FLATTENING ELIMINATION RULES

2014 ◽  
Vol 7 (1) ◽  
pp. 60-72 ◽  
Author(s):  
GRIGORY K. OLKHOVIKOV ◽  
PETER SCHROEDER-HEISTER
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Second Order ◽  
Kripke Semantics ◽  
Elimination Rule

AbstractIn proof-theoretic semantics of intuitionistic logic it is well known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases, these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all—they can be flattened in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.

On storage operators

1998 ◽  
Author(s):  
Karim Nour
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Input Data ◽  
Type System ◽  
Second Order ◽  
Data Type ◽  
Simple Type ◽  
Output Data ◽  
Major Drawback ◽  
Proof Rules

λ-calculus as such is not a computational model. A reduction strategy is needed. In this paper, we consider λ-calculus with the left reduction. This strategy has many advantages: it always terminates when applied to a normalizable λ-term and it seems more economic since we compute λ-term only when we need it. But the major drawback of this strategy is that a function must compute its argument every time it uses it. This is the reason why this strategy is not really used. In 1990 Krivine (1990b) introduced the notion of storage operators in order to avoid this problem and to simulate call-by-value when necessary. The AF2 type system is a way of interpreting the proof rules for second-order intuitionistic logic plus equational reasoning as construction rules for terms. Krivine (1990b) has shown that, by using Gödel translation from classical to intuitionistic logic (denoted byg), we can find in system AF2 a very simple type for storage operators. Historically the type was discovered before the notion of storage operator itself. Krivine (1990a) proved that as far as totality of functions is concerned second-order classical logic is conservative over second-order intuitionistic logic. To prove this, Krivine introduced the following notions: A[x] is an input (resp. output) data type if one can prove intuitionistically A[x] → Ag[x] (resp. Ag[x] → ⇁⇁A[x]). Then if A[x] is an input data type and B[x] is an output data type, then if one can prove A[x] → B[x] classically one can prove it intuitionistically. The notion of storage operator was discovered by investigating the property of all λ-terms of type Ng[x] → ⇁⇁N[x] where N[x] is the type of integers. Parigot (1992) and Krivine (1994) have extended the AF2 system to classical logic. The method of Krivine is very simple: it consists of adding a new constant, denoted by C, with the declaration С: ∀X{⇁⇁ X → X} which axiomatizes classical logic over intuitionistic logic. For the constant C, he adds a new reduction rule which is a particular case of a rule given by Felleisen (1987) for control operator.

On a theory of weak implications

1988 ◽  
Vol 53 (1) ◽  
pp. 200-211 ◽  
Author(s):  
Mitsuhiro Okada
Keyword(s):  
Intuitionistic Logic ◽  
General Setting ◽  
Second Order ◽  
Inference Rules ◽  
Full Strength ◽  
Circular Argument ◽  
Logical Connectives ◽  
Points Of View ◽  
Weak Implications ◽  
Order Extension

The purpose of this paper is to study logical implications which are much weaker than the implication of intuitionistic logic.In §1 we define the system SI (system of Simple Implication) which is obtained from intuitionistic logic by restricting the inference rules of intuitionistic implication. The implication of the system SI is called the “simple implication” and denoted by ⊃, where the simple implication ⊃ has the following properties:(1) The simple implication ⊃ is much weaker than the usual intuitionistic implication.(2) The simple implication ⊃ can be interpreted by the notion of provability, i.e., we have a very simple semantics for SI so that a sentence A ⊃ B is interpreted as “there exists a proof of B from A”.(3) The full-strength intuitionistic implication ⇒ is definable in a weak second order extension of SI; in other words, it is definable by help of a variant of the weak comprehension schema and the simple implication ⊃. Therefore, though SI is much weaker than the intuitionistic logic, the second order extension of SI is equivalent to the second order extension of the intuitionistic logic.(4) The simple implication is definable in a weak modal logic MI by the use of the modal operator and the intuitionistic implication ⇒ with full strength. More precisely, A ⊃ B is defined as the strict implication of the form ◽(A ⇒ B).In §1, we show (3) and (4). (2) is shown in §2 in a more general setting.Semantics by introduction rules of logical connectives has been studied from various points of view by many authors (e.g. Gentzen [4], Lorentzen [5], Dummett [1], [2], Prawitz [8]. Martin-Löf [7], Maehara [6]). Among them Gentzen (in §§10 and 11 of [4]) introduced such a semantics in order to justify logical inferences and the mathematical induction rule. He observed that all of the inference rules of intuitionistic arithmetic, except for those on implication and negation, are justified by means of his semantics, but justification of the inference rules on implication and negation contains a circular argument for the interpretation by introduction rules, where the natural interpretation of A ⊃ B by ⊃-introduction rule is “there exists a proof of B from A ” (cf. §11 of Gentzen [4]).

Propositional quantification in the monadic fragment of intuitionistic logic

1998 ◽  
Vol 63 (1) ◽  
pp. 269-300 ◽  
Author(s):  
Tomasz Połacik
Keyword(s):  
Intuitionistic Logic ◽  
Metric Space ◽  
Propositional Logic ◽  
Second Order ◽  
Intuitionistic Propositional Logic ◽  
Topological Interpretation ◽  
Propositional Quantifiers ◽  
Propositional Quantification

AbstractWe study the monadic fragment of second order intuitionistic propositional logic in the language containing the standard propositional connectives and propositional quantifiers. It is proved that under the topological interpretation over any dense-in-itself metric space, the considered fragment collapses to Heyting calculus. Moreover, we prove that the topological interpretation over any dense-in-itself metric space of fragment in question coincides with the so-called Pitts' interpretation. We also prove that all the nonstandard propositional operators of the form q ↦ ∃p (q ↔ F(p)), where F is an arbitrary monadic formula of the variable p, are definable in the language of Heyting calculus under the topological interpretation of intuitionistic logic over sufficiently regular spaces.

scholarly journals LOGICS FOR PROPOSITIONAL CONTINGENTISM

2017 ◽  
Vol 10 (2) ◽  
pp. 203-236 ◽  
Author(s):  
PETER FRITZ
Keyword(s):  
Model Theory ◽  
Possible Worlds ◽  
Second Order ◽  
Order Logic ◽  
Existential Quantifier ◽  
Philosophical Theory ◽  
Propositional Operator ◽  
Second Order Logic

AbstractRobert Stalnaker has recently advocated propositional contingentism, the claim that it is contingent what propositions there are. He has proposed a philosophical theory of contingency in what propositions there are and sketched a possible worlds model theory for it. In this paper, such models are used to interpret two propositional modal languages: one containing an existential propositional quantifier, and one containing an existential propositional operator. It is shown that the resulting logic containing an existential quantifier is not recursively axiomatizable, as it is recursively isomorphic to second-order logic, and a natural candidate axiomatization for the resulting logic containing an existential operator is shown to be incomplete.

The undecidability of second order linear logic without exponentials

1996 ◽  
Vol 61 (2) ◽  
pp. 541-548 ◽  
Author(s):  
Yves Lafont
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Linear Logic ◽  
Classical Case ◽  
Second Order ◽  
Order Linear ◽  
Phase Semantics ◽  
Counter Machines ◽  
Intuitionistic Linear Logic

AbstractRecently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment of second order intuitionistic linear logic is undecidable, using an encoding of second order intuitionistic logic. Their argument applies to the multiplicative-additive fragment, but it does not work in the classical case, because second order classical logic is decidable. Here we show that the multiplicative-additive fragment of second order classical linear logic is also undecidable, using an encoding of two-counter machines originally due to Kanovich. The faithfulness of this encoding is proved by means of the phase semantics.

How to glue analysis models

1984 ◽  
Vol 49 (4) ◽  
pp. 1339-1349 ◽  
Author(s):  
D. Van Dalen
Keyword(s):  
Intuitionistic Logic ◽  
Second Order ◽  
Kripke Semantics ◽  
Kripke Models ◽  
Closure Properties ◽  
Second Order Arithmetic ◽  
First Order ◽  
Order Arithmetic ◽  
Analysis Models

Among the more traditional semantics for intuitionistic logic the Beth and the Kripke semantics seem well-suited for direct manipulations required for the derivation of metamathematical results. In particular Smoryński demonstrated the usefulness of Kripke models for the purpose of obtaining closure properties for first-order arithmetic, [S], and second-order arithmetic, [J-S]. Weinstein used similar techniques to handle intuitionistic analysis, [W]. Since, however, Beth-models seem to lend themselves better for dealing with analysis, cf. [D], we have developed a somewhat more liberal semantics, that shares the features of both Kripke and Beth semantics, in order to obtain analogues of Smoryński's collecting operations, which we will call Smoryński-glueing, in line with the categorical tradition.

scholarly journals On the complexity of propositional quantification in intuitionistic logic

1997 ◽  
Vol 62 (2) ◽  
pp. 529-544 ◽  
Author(s):  
Philip Kremer
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Natural Extension ◽  
Second Order ◽  
Modal Systems ◽  
Propositional Quantification

AbstractWe define a propositionally quantified intuitionistic logic Hπ+ by a natural extension of Kripke's semantics for propositional intuitionistic logic. We then show that Hπ+ is recursively isomorphic to full second order classical logic. Hπ+ is the intuitionistic analogue of the modal systems S5π+, S4π+, S4.2π+, K4π+, Tπ+, Kπ+ and Bπ+, studied by Fine.

scholarly journals Interpreting classical theories in constructive ones

2000 ◽  
Vol 65 (4) ◽  
pp. 1785-1812 ◽  
Author(s):  
Jeremy Avigad
Keyword(s):  
Set Theory ◽  
Intuitionistic Logic ◽  
Second Order ◽  
Bounded Arithmetic ◽  
Admissible Set ◽  
Second Order Arithmetic ◽  
Order Arithmetic

AbstractA number of classical theories are interpreted in analogous theories that are based on intuitionistic logic. The classical theories considered include subsystems of first- and second-order arithmetic, bounded arithmetic, and admissible set theory.

Sign in / Sign up

Export Citation Format

Share Document