Epsilon substitution method for [Π0 1, Π0 1]-FIX

We formulate epsilon substitution method for a theory [Π⁰₁, Π⁰₁]-FIX for two steps non-monotonic Π⁰₁ inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].     

A note on theΠ 2 0 -induction rule

It is well-known (due to C. Parsons) that the extension of primitive recursive arithmeticPRA by first-order predicate logic and the rule of ₂ ⁰ -induction ₂ ⁰ -IR is ₂ ⁰ -conservative overPRA. We show that this is no longer true in the presence of function quantifiers and quantifier-free choice for numbersAC ^0,0-qf. More precisely we show that :=PRA ² + ₂ ⁰ -IR+AC ^0,0-qf proves the totality of the Ackermann function, wherePRA ² is the extension ofPRA by number and function quantifiers and ₂ ⁰ -IR may contain function parameters.This is true even forPRA ² + ₁ ⁰ -IR+ ₂ ⁰ -IR ^–+AC ^0,0-qf, where ₂ ⁰ -IR ^– is the restriction of ₂ ⁰ -IR without function parameters.I am grateful to an anonymous referee whose suggestions led to an improved discussion of our results     

Explaining the Gentzen–Takeuti reduction steps: a second-order system

Using the concept of notations for infinitary derivations we give an explanation of Takeuti's reduction steps on finite derivations (used in his consistency proof for Π¹ ₁-CA) in terms of the more perspicious infinitary approach from [BS88]. Received: 27 April 1999 / Published online: 21 March 2001     

Epsilon substitution method for elementary analysis

We formulate epsilon substitution method for elementary analysisEA (second order arithmetic with comprehension for arithmetical formulas with predicate parameters). Two proofs of its termination are presented. One uses embedding into ramified system of level one and cutelimination for this system. The second proof uses non-effective continuity argument.     

Reverse Mathematics and parameter-free Transfer

Recently, conservative extensions of Peano and Heyting arithmetic in the spirit of Nelson's axiomatic approach to Nonstandard Analysis, have been proposed. In this paper, we study the Transfer axiom of Nonstandard Analysis restricted to formulas without parameters. Based on this axiom, we formulate a base theory for the Reverse Mathematics of Nonstandard Analysis and prove some natural reversals, and show that most of these equivalences do not hold in the absence of parameter-free Transfer.     

On Two Questions About Topological (and Nonstandard) Extensions

We construct, under MA, a non-Hausdorff (T₁-)topological extension ^*ω of ω, such that every function from ω to ω extends uniquely to a continuous function from ^*ω to ^*ω. We also show (in ZFC) that for every nontrivial topological extension ^*X of a countable set X there exists a topology τ_f on ^*X, strictly finer than the Star topology, and such that (^*X, τ_f) is still a topological extension of X with the same function extensions ^*f. This solves two questions raised by M. Di Nasso and M. Forti.     

A note on sharply bounded arithmetic

Summary We prove some independence results for the bounded arithmetic theoryR ₂ ⁰ , and we define a class of functions that is shown to be an upper bound for the class of functions definable by a certain restricted class of ₁ ^b in extensions ofR ₂ ⁰ .Mathematics subject classification: 03F30This article was processed by the author using the LATEX style filepljour1 from Spinger-Verlag.     

Basic Propositional Calculus II. Interpolation

Let ℒ and ? be propositional languages over Basic Propositional Calculus, and ℳ = ℒ∩?. Weprove two different but interrelated interpolation theorems. First, suppose that Π is a sequent theory over ℒ, and Σ∪ {C⇒C′} is a set of sequents over ?, such that Π,Σ⊢C⇒C′. Then there is a sequent theory Φ over ℳ such that Π⊢Φ and Φ, Σ⊢C⇒C′. Second, let A be a formula over ℒ, and C ₁, C ₂ be formulas over ?, such that A∧C ₁⊢C ₂. Then there exists a formula B over ℳ such that A⊢B and B∧C ₁⊢C ₂. Received: 7 January 1998 / Published online: 18 May 2001     

Universality of Embeddability Relations for Coloured Total Orders

Some examples of Σ₁ ¹-universal preorders are presented, in the form of various relations of embeddability between countable coloured total orders. As an application, strengthening a theorem of (Marcone, A. and Rosendal, C.: The Complexity of Continuous Embeddability between Dendrites, J. Symb. Log. 69 (2004), 663–673), the Σ₁ ¹-universality of continuous embeddability for dendrites whose branch points have order 3 is obtained.     

Density results in the Δ20 e-degrees

We show that the Δ⁰ ₂ enumeration degrees are dense. We also show that for every nonzero n-c. e. e-degree a, with n≥ 3, one can always find a nonzero 3-c. e. e-degree b such that b < a on the other hand there is a nonzero ωc. e. e-degree which bounds no nonzero n-c. e. e-degree. Received: 13 June 2000 / Published online: 3 October 2001     

Algebraic proof theory for substructural logics: Cut-elimination and completions

We carry out a unified investigation of two prominent topics in proof theory and order algebra: cut-elimination and completion, in the setting of substructural logics and residuated lattices.We introduce the substructural hierarchy — a new classification of logical axioms (algebraic equations) over full Lambek calculus FL, and show that a stronger form of cut-elimination for extensions of FL and the MacNeille completion for subvarieties of pointed residuated lattices coincide up to the level N₂ in the hierarchy. Negative results, which indicate limitations of cut-elimination and the MacNeille completion, as well as of the expressive power of structural sequent calculus rules, are also provided.Our arguments interweave proof theory and algebra, leading to an integrated discipline which we call algebraic proof theory.     

Rigidity of critical circle mappings I

We prove that two C ³ critical circle maps with the same rotation number in a special set ? are C ^1+α conjugate for some α>0 provided their successive renormalizations converge together at an exponential rate in the C ⁰ sense. The set ? has full Lebesgue measure and contains all rotation numbers of bounded type. By contrast, we also give examples of C ^∞ critical circle maps with the same rotation number that are not C ^1+β conjugate for any β>0. The class of rotation numbers for which such examples exist contains Diophantine numbers. Received November 1, 1998 / final version received July 7, 1999     

Normal forms for stochastic differential equations

Summary.   We address the following problem from the intersection of dynamical systems and stochastic analysis: Two SDE dx _t = ∑ _{j =0} ^m f _j (x _t )∘dW _t ^j and dx _t =∑ _{j =0} ^m g _j (x _t )∘dW _t ^j in ℝ ^d with smooth coefficients satisfying f _j (0)=g _j (0)=0 are said to be smoothly equivalent if there is a smooth random diffeomorphism (coordinate transformation) h(ω) with h(ω,0)=0 and Dh(ω,0)=id which conjugates the corresponding local flows,

Virtual Eigenvalues of the High Order Schrödinger Operator I

We consider the Schr?dinger operator H_γ = ( − Δ)^l + γ V(x)· acting in the space $$L_2 (\mathbb{R}^d ),$$ where 2l ≥ d, V (x) ≥ 0, V (x) is continuous and is not identically zero, and $$\lim _{|{\mathbf{x}}| \to \infty } V({\mathbf{x}}) = 0.$$ We obtain an asymptotic expansion as $$\gamma \uparrow 0$$of the bottom negative eigenvalue of H_γ, which is born at the moment γ = 0 from the lower bound λ = 0 of the spectrum σ(H₀) of the unperturbed operator H₀ = ( − Δ)^l (a virtual eigenvalue). To this end we develop a supplement to the Birman-Schwinger theory on the process of the birth of eigenvalues in the gap of the spectrum of the unperturbed operator H₀. Furthermore, we extract a finite-rank portion Φ(λ) from the Birman- Schwinger operator $$X_V (\lambda ) = V^{\frac{1} {2}} R_\lambda (H_0 )V^{\frac{1}{2}} ,$$ which yields the leading terms for the desired asymptotic expansion.     

Index sets and parametric reductions

We investigate the index sets associated with the degree structures of computable sets under the parameterized reducibilities introduced by the authors. We solve a question of Peter Cholakand the first author by proving the fundamental index sets associated with a computable set A, {e : W _e ≤ _q ^u A} for q∈ {m, T} are Σ₄ ⁰ complete. We also show hat FPT(≤ _q ⁿ ), that is {e : W _e computable and ≡ _q ⁿ ?}, is Σ₄ ⁰ complete. We also look at computable presentability of these classes. Received: 13 July 1996 / Revised version: 14 April 2000 / Published online: 18 May 2001     

No Escape from Vardanyan's theorem

Vardanyan's theorem states that the set of PA-valid principles of Quantified Modal Logic, QML, is complete Π⁰₂. We generalize this result to a wide class of theories. The crucial step in the generalization is avoiding the use of Tennenbaum's Theorem.     

Positive provability logic for uniform reflection principles

We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ω   corresponds to the full uniform reflection schema, whereas n<ω$n<\omega$ corresponds to its restriction to arithmetical _Πn+1${\Pi }_{n+1}$-formulas. This calculus is shown to be complete w.r.t. a suitable class of finite Kripke models and to be decidable in polynomial time.     

Logical Extensions of Aristotle’s Square

We start from the geometrical-logical extension of Aristotle’s square in [6,15] and [14], and study them from both syntactic and semantic points of view. Recall that Aristotle’s square under its modal form has the following four vertices: A is □α, E is , I is and O is , where α is a logical formula and □ is a modality which can be defined axiomatically within a particular logic known as S5 (classical or intuitionistic, depending on whether is involutive or not) modal logic. [3] has proposed extensions which can be interpreted respectively within paraconsistent and paracomplete logical frameworks. [15] has shown that these extensions are subfigures of a tetraicosahedron whose vertices are actually obtained by closure of by the logical operations , under the assumption of classical S5 modal logic. We pursue these researches on the geometrical-logical extensions of Aristotle’s square: first we list all modal squares of opposition. We show that if the vertices of that geometrical figure are logical formulae and if the sub-alternation edges are interpreted as logical implication relations, then the underlying logic is none other than classical logic. Then we consider a higher-order extension introduced by [14], and we show that the same tetraicosahedron plays a key role when additional modal operators are introduced. Finally we discuss the relation between the logic underlying these extensions and the resulting geometrical-logical figures.