Minimal readability of intuitionistic arithmetic and elementary analysis

1995 ◽  
Vol 60 (4) ◽  
pp. 1208-1241 ◽  
Author(s):  
Zlatan Damnjanovic
Keyword(s):  
Finite Type ◽  
Peano Arithmetic ◽  
New Method ◽  
Recursive Functions ◽  
Heyting Arithmetic ◽  
Elementary Analysis ◽  
Skolem Functions ◽  
Definable Functions ◽  
Intuitionistic Arithmetic

AbstractA new method of “minimal” readability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)—functions f such that HA ⊢ ∀x∃!yA(x, y) ⇒ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of ℒ(HA) with only x,y free—are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the < ε0-recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be < ε0-recursive. The method is extended to intuitionistic finite-type arithmetic, , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived.

Lifschitz' realizability

1990 ◽  
Vol 55 (2) ◽  
pp. 805-821 ◽  
Author(s):  
Jaap van Oosten
Keyword(s):  
Axiomatic Characterization ◽  
Uniqueness Condition ◽  
Church’S Thesis ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Continuous Application ◽  
Church's Thesis ◽  
Order Arithmetic ◽  
Intuitionistic Arithmetic

AbstractV. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a “q-variant” we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe an analogous development for elementary analysis, with partial continuous application replacing partial recursive application.

Fragments of Heyting arithmetic

2000 ◽  
Vol 65 (3) ◽  
pp. 1223-1240 ◽  
Author(s):  
Wolfgang Burr
Keyword(s):  
First Order ◽  
Recursive Functions ◽  
Heyting Arithmetic ◽  
Universal Quantification ◽  
Law Of Excluded Middle ◽  
The Law ◽  
Order Arithmetic ◽  
Excluded Middle ◽  
Intuitionistic Arithmetic

AbstractWe define classes Φn of formulae of first-order arithmetic with the following properties:(i) Every φ ϵ Φn is classically equivalent to a Πn-formula (n ≠ 1, Φ1 := Σ1).(ii) (iii) IΠn and iΦn (i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φn both under existential and universal quantification (we call these classes Θn) the corresponding theories iΘn still prove the same Π2-formulae. In a second part we consider iΔ0 plus collection-principles. We show that both the provably recursive functions and the provably total functions of are polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence .

Grzegorcyk's hierarchy and IepΣ1

1994 ◽  
Vol 59 (4) ◽  
pp. 1274-1284 ◽  
Author(s):  
Gaisi Takeuti
Keyword(s):  
Computational Complexity ◽  
Weak Form ◽  
Complexity Class ◽  
Conservative Extension ◽  
Recursive Functions ◽  
Theoretic Characterization ◽  
Definable Functions ◽  
Primitive Recursive

A proof-theoretic characterization of the primitive recursive functions is the Σ1-definable functions in IΣ1 as is shown in Mints [4], Parsons [5], and [8].Then what is a proof-theoretic characterization of Grzegorzyk's hierarchy? First we discuss a related previous work. In Clote and Takeuti [2], we introduced a theory TAC that corresponds to the computational complexity class AC. TAC has a very weak form of induction. We assign a rank to a proof in TAC in the following way. The rank of a proof P in TAC is the nesting number of inductions used in P. Then TACi is defined to be the subtheory of TAC whose proof has a rank ≤ i. We proved that TACi corresponds to the class ACi.In this paper we introduce a theory IepΣ1 which is equivalent to IΣ1. Then we define the rank of a proof in IepΣ1 as the nesting number of inductions in the proof and prove that the proofs with rank ≤ i correspond to Grzegorcyk's hierarchy for i > 0.We also prove that the system that has proofs with rank 0 is actually equivalent to I Δ0. These facts are interesting since it is proved in [10] that the theory isomorphic to TAC∘ by RSUV isomorphism is a conservative extension of I Δo. Therefore there is some analogy between the class AC and the primitive recursive functions.

Forcing and satisfaction in Kripke models of intuitionistic arithmetic

2018 ◽  
Vol 27 (5) ◽  
pp. 659-670
Author(s):  
Maryam Abiri ◽  
Morteza Moniri ◽  
Mostafa Zaare
Keyword(s):  
Predicate Logic ◽  
Kripke Model ◽  
Peano Arithmetic ◽  
Kripke Models ◽  
Classical Structure ◽  
First Order ◽  
Heyting Arithmetic ◽  
Intuitionistic Arithmetic

Abstract We define a class of first-order formulas $\mathsf{P}^{\ast }$ which exactly contains formulas $\varphi$ such that satisfaction of $\varphi$ in any classical structure attached to a node of a Kripke model of intuitionistic predicate logic deciding atomic formulas implies its forcing in that node. We also define a class of $\mathsf{E}$-formulas with the property that their forcing coincides with their classical satisfiability in Kripke models which decide atomic formulas. We also prove that any formula with this property is an $\mathsf{E}$-formula. Kripke models of intuitionistic arithmetical theories usually have this property. As a consequence, we prove a new conservativity result for Peano arithmetic over Heyting arithmetic.

A new method for approximation of closed convex subsets of B(H)

Filomat ◽  
2017 ◽  
Vol 31 (19) ◽  
pp. 6005-6013
Author(s):  
Mahdi Iranmanesh ◽  
Fatemeh Soleimany
Keyword(s):  
Best Approximation ◽  
Numerical Range ◽  
New Method ◽  
C Algebra ◽  
Convex Subsets

In this paper we use the concept of numerical range to characterize best approximation points in closed convex subsets of B(H): Finally by using this method we give also a useful characterization of best approximation in closed convex subsets of a C*-algebra A.

On a generalization of the Rényi–Srivastava characterization of the Poisson law

2021 ◽  
Vol 58 (1) ◽  
pp. 68-82
Author(s):  
Jean-Renaud Pycke
Keyword(s):  
Life Insurance ◽  
Collective Model ◽  
New Method ◽  
Bell Polynomials ◽  
Explicit Formulas ◽  
Compound Distributions ◽  
Poisson Law ◽  
Pierre Loti

AbstractWe give a new method of proof for a result of D. Pierre-Loti-Viaud and P. Boulongne which can be seen as a generalization of a characterization of Poisson law due to Rényi and Srivastava. We also provide explicit formulas, in terms of Bell polynomials, for the moments of the compound distributions occurring in the extended collective model in non-life insurance.

scholarly journals Spectroscopic characterization of a thermodynamically stable doubly charged diatomic molecule: MgAr2+

2021 ◽  
Author(s):  
Dominik Wehrli ◽  
Matthieu Génévriez ◽  
Frédéric Merkt
Keyword(s):  
High Resolution ◽  
Diatomic Molecule ◽  
Spectroscopic Characterization ◽  
New Method ◽  
High Resolution Spectroscopy ◽  
Singly Charged ◽  
Doubly Charged

We present a new method to study doubly charged molecules relying on high-resolution spectroscopy of the singly charged parent cation, and report on the first spectroscopic characterization of a thermodynamically stable diatomic dication, MgAr2+.

scholarly journals A New Ultrasensitive Bioluminescence-Based Method for Assaying Monoacylglycerol Lipase

2021 ◽  
Vol 22 (11) ◽  
pp. 6148
Author(s):  
Matteo Miceli ◽  
Silvana Casati ◽  
Pietro Allevi ◽  
Silvia Berra ◽  
Roberta Ottria ◽  
...  
Keyword(s):  
Arachidonic Acid ◽  
Kinetic Constants ◽  
New Method ◽  
Monoacylglycerol Lipase ◽  
Enzymatic Cleavage ◽  
Highly Sensitive ◽  
Bioluminescence Assay ◽  
Identification And Characterization ◽  
In Cells

A novel bioluminescent Monoacylglycerol lipase (MAGL) substrate 6-O-arachidonoylluciferin, a D-luciferin derivative, was synthesized, physico-chemically characterized, and used as highly sensitive substrate for MAGL in an assay developed for this purpose. We present here a new method based on the enzymatic cleavage of arachidonic acid with luciferin release using human Monoacylglycerol lipase (hMAGL) followed by its reaction with a chimeric luciferase, PLG2, to produce bioluminescence. Enzymatic cleavage of the new substrate by MAGL was demonstrated, and kinetic constants Km and Vmax were determined. 6-O-arachidonoylluciferin has proved to be a highly sensitive substrate for MAGL. The bioluminescence assay (LOD 90 pM, LOQ 300 pM) is much more sensitive and should suffer fewer biological interferences in cells lysate applications than typical fluorometric methods. The assay was validated for the identification and characterization of MAGL modulators using the well-known MAGL inhibitor JZL184. The use of PLG2 displaying distinct bioluminescence color and kinetics may offer a highly desirable opportunity to extend the range of applications to cell-based assays.

Sign in / Sign up

Export Citation Format

Share Document