Glivenko sequent classes in the light of structural proof theory

In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.     

Two applications of Boolean models

Semantical arguments, based on the completeness theorem for first-order logic, give elegant proofs of purely syntactical results. For instance, for proving a conservativity theorem between two theories, one shows instead that any model of one theory can be extended to a model of the other theory. This method of proof, because of its use of the completeness theorem, is a priori not valid constructively. We show here how to give similar arguments, valid constructively, by using Boolean models. These models are a slight variation of ordinary first-order models, where truth values are now regular ideals of a given Boolean algebra. Two examples are presented: a simple conservativity result and Herbrand's theorem. Received December 5, 1995     

Real numbers and projective spaces: Intuitionistic reasoning with undecidable basic relations

Brouwer introduced in 1924 the notion of an apartness relation for real numbers, with the idea that whenever it holds, a finite computation verifies it in contrast to equality. The idea was followed in Heyting’s axiomatization of intuitionistic projective geometry. Brouwer in turn worked out an intuitionistic theory of “virtual order.” It is shown that Brouwer’s proof of the equivalence of virtual and maximal order goes only in one direction, and that Heyting’s axiomatization needs to be made a bit stronger.     

Lifting independence results in bounded arithmetic

We investigate the problem how to lift the non - - conservativity of over to the expected non - - conservativity of over , for . We give a non-trivial refinement of the “lifting method” developed in [4,8], and we prove a sufficient condition on a -consequence of to yield the non-conservation result. Further we prove that Ramsey's theorem, a - formula, is not provable in , and that - conservativity of over implies - conservativity of the whole over , for any . Received: 3 April 1997     

Product a‐frames and proximity

Continuing the study of apartness in lattices, begun in [8], this paper deals with axioms for a product a‐frame and with their consequences. This leads to a reasonable notion of proximity in an a‐frame, abstracted from its counterpart in the theory of set‐set apartness. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Proof-theoretical analysis of order relations

A proof-theoretical analysis of elementary theories of order relations is effected through the formulation of order axioms as mathematical rules added to contraction-free sequent calculus. Among the results obtained are proof-theoretical formulations of conservativity theorems corresponding to Szpilrajns theorem on the extension of a partial order into a linear one. Decidability of the theories of partial and linear order for quantifier-free sequents is shown by giving terminating methods of proof-search.Mathematics Subject Classification (2000): 03F05, 06A05, 06A06     

A generalization of a conservativity theorem for classical versus intuitionistic arithmetic

A basic result in intuitionism is Π⁰₂‐conservativity. Take any proof p in classical arithmetic of some Π⁰₂‐statement (some arithmetical statement ?x.?y.P(x, y), with P decidable). Then we may effectively turn p in some intuitionistic proof of the same statement. In a previous paper [1], we generalized this result: any classical proof p of an arithmetical statement ?x.?y.P(x, y), with P of degree k, may be effectively turned into some proof of the same statement, using Excluded Middle only over degree k formulas. When k = 0, we get the original conservativity result as particular case. This result was a by‐product of a semantical construction. J. Avigad of Carnegie Mellon University, found a short, direct syntactical derivation of the same result, using H. Friedman's A‐translation. His proof is included here with his permission. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

On proximal convergence in uniform spaces

The paper deals with proximal convergence and Leader's theorem, in the constructive theory of uniform apartness spaces. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

D ickson定理和H all定理的初等证明及二定理的等价性

论证了二定理的等价性,给出了H a ll定理的初等证明,展示出求得H a ll方程解的个数的可操作性.再利用二定理的等价性,又给出D ickson定理的初等证明.对求解D ickson方程解的个数,也有鲜明的可操作性.     

Arithmetic transfinite induction and recursive well-orderings

A uniform, algebraic proof that every number-theoretic assertion provable in any of the intuitionistic theories T listed below has a well-founded recursive proof tree (demonstraby in T) is given. Thus every such assertion is provable by transfinite induction over some primitive recursive well-ordering. T can be higher order number theory, set theory, or its extensions equiconsistent with large cardinals. It is shown that there is a number-theoretic assertion B(n) (independent of T) with a parameter n such that any primitive recursive linear ordering R on ω for which transfinite induction on R for B(n) is provable in T is in fact a well-ordering.     

Modules over motivic cohomology

For fields of characteristic zero, we show that the homotopy category of modules over the motivic ring spectrum representing motivic cohomology is equivalent to Voevodsky's big category of motives. The proof makes use of some highly structured models for motivic stable homotopy theory, motivic Spanier-Whitehead duality, the homotopy theories of motivic functors and of motivic spaces with transfers as introduced from ground up in this paper. Working with rational coefficients, we extend the equivalence for fields of characteristic zero to all perfect fields by employing the techniques of alterations and homotopy purity in motivic homotopy theory.     

An intuitionistic formula hierarchy based on high‐school identities

We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the invertible proof rules of intuitionistic (minimal) propositional sequent calculi are formula (i.e., sequent) isomorphisms corresponding to the high‐school identities, we show that one can obtain a more compact variant of a proof system, consisting of non‐invertible proof rules only, and where the invertible proof rules have been replaced by a formula normalization procedure. Moreover, for certain proof systems such as the G4ip sequent calculus of Vorob'ev, Hudelmaier, and Dyckhoff, it is even possible to see all of the non‐invertible proof rules as strict inequalities between exponential polynomials; a careful combinatorial treatment is given in order to establish this fact. Finally, we extend the exponential polynomial analogy to the first‐order quantifiers, showing that it gives rise to an intuitionistic hierarchy of formulas, resembling the classical arithmetical hierarchy, and the first one that classifies formulas while preserving isomorphism.     

Conservativity Spectra and Joosten–Fernández Model

Doklady Mathematics - We study a generalization of the notion of conservativity spectrum of an arithmetical theory to a language with transfinitely many truth definitions. We establish a natural...     

Contraction-free sequent calculi for geometric theories with an application to Barr's theorem

 Geometric theories are presented as contraction- and cut-free systems of sequent calculi with mathematical rules following a prescribed rule-scheme that extends the scheme given in Negri and von Plato (1998). Examples include cut-free calculi for Robinson arithmetic and real closed fields. As an immediate consequence of cut elimination, it is shown that if a geometric implication is classically derivable from a geometric theory then it is intuitionistically derivable. Received: 18 April 2001 / Published online: 10 October 2002 Mathematics Subject Classification (2000): 03F05, 18C10, 18B15 Key words or phrases: Cut elimination – Geometric theories – Barr's theorem     

A weak variant of Hindman’s Theorem stronger than Hilbert’s Theorem

Hirst investigated a natural restriction of Hindman’s Finite Sums Theorem—called Hilbert’s Theorem—and proved it equivalent over \(\mathbf {RCA}_0\) to the Infinite Pigeonhole Principle for all colors. This gave the first example of a natural restriction of Hindman’s Theorem provably much weaker than Hindman’s Theorem itself. We here introduce another natural restriction of Hindman’s Theorem—which we name the Adjacent Hindman’s Theorem with apartness—and prove it to be provable from Ramsey’s Theorem for pairs and strictly stronger than Hirst’s Hilbert’s Theorem. The lower bound is obtained by a direct combinatorial implication from the Adjacent Hindman’s Theorem with apartness to the Increasing Polarized Ramsey’s Theorem for pairs introduced by Dzhafarov and Hirst. In the Adjacent Hindman’s Theorem homogeneity is required only for finite sums of adjacent elements.     

Pre-apartness structures on spaces of functions

Pre-apartness structures are defined on Y^X, where X is an inhabited set and Y a uniform space. These structures clarify the discussion of proximal and uniform convergence in the constructive theory of apartness spaces.     

Causal compositional models in valuation-based systems with examples in specific theories

We show that Pearl's causal networks can be described using causal compositional models (CCMs) in the valuation-based systems (VBS) framework. One major advantage of using the VBS framework is that as VBS is a generalization of several uncertainty theories (e.g., probability theory, a version of possibility theory where combination is the product t-norm, Spohn's epistemic belief theory, and Dempster–Shafer belief function theory), CCMs, initially described in probability theory, are now described in all uncertainty calculi that fit in the VBS framework. We describe conditioning and interventions in CCMs. Another advantage of using CCMs in the VBS framework is that both conditioning and intervention can be easily described in an elegant and unifying algebraic way for the same CCM without having to do any graphical manipulations of the causal network. We describe how conditioning and intervention can be computed for a simple example with a hidden (unobservable) variable. Also, we illustrate the algebraic results using numerical examples in some of the specific uncertainty calculi mentioned above.     

Transfer principles in nonstandard intuitionistic arithmetic

 Using a slight generalization, due to Palmgren, of sheaf semantics, we present a term-model construction that assigns a model to any first-order intuitionistic theory. A modification of this construction then assigns a nonstandard model to any theory of arithmetic, enabling us to reproduce conservation results of Moerdijk and Palmgren for nonstandard Heyting arithmetic. Internalizing the construction allows us to strengthen these results with additional transfer rules; we then show that even trivial transfer axioms or minor strengthenings of these rules destroy conservativity over HA. The analysis also shows that nonstandard HA has neither the disjunction property nor the explicit definability property. Finally, careful attention to the complexity of our definitions allows us to show that a certain weak fragment of intuitionistic nonstandard arithmetic is conservative over primitive recursive arithmetic. Received: 7 January 2000 / Revised version: 26 March 2001 / Published online: 12 July 2002     

Proof complexity of propositional default logic

Default logic is one of the most popular and successful formalisms for non-monotonic reasoning. In 2002, Bonatti and Olivetti introduced several sequent calculi for credulous and skeptical reasoning in propositional default logic. In this paper we examine these calculi from a proof-complexity perspective. In particular, we show that the calculus for credulous reasoning obeys almost the same bounds on the proof size as Gentzen??s system LK. Hence proving lower bounds for credulous reasoning will be as hard as proving lower bounds for LK. On the other hand, we show an exponential lower bound to the proof size in Bonatti and Olivetti??s enhanced calculus for skeptical default reasoning.