Call a (strictly increasing) sequence (rn) of natural numbers regular if it satisfies the following condition: rn+1/rn→θ∈R>1∪{∞} and, if θ is algebraic, then (rn) satisfies a linear recurrence relation whose characteristic polynomial is the minimal polynomial of θ. Our main result states that (Z,+,0,R) is superstable whenever R is enumerated by a regular sequence. We give two proofs of this result. One relies on a result of E. Casanovas and M. Ziegler and the other on a quantifier elimination result. We (...) also show that (Z,+,0,<,R) is NIP whenever R is enumerated by a regular sequence that is ultimately periodic modulo m for all m>1. (shrink)

The main issue André Porto raises in his paper concerns the use of dot notation to indicate an infinite set of hypotheses. Whereas I agree that one cannot extract a unique infinite expansion from a finite initial segment, in my response I argue that this holds for finite expansions as well. I further explain how my remarks on infinite proof structures are neither motivated by the impact of Gödel’s incompleteness theorems on Hilbert’s program, nor by a negative view (...) of strict finitism.O problema central que André Porto discute em seu artigo diz respeito ao uso da notação de pontos para indicar um conjunto infinito de hipóteses. Mesmo estando de acordo não ser possível extrair uma expansão infinita a partir de um segmento inicial finito, em minha réplica argumento que isto vale igualmente para expansões finitas. Explico também que minhas observações sobre estruturas de prova infinitas não são motivadas pelo impacto dos teoremas de incompletude de Gödel no programa de Hilbert, e tampouco por uma visão negativa do finitismo estrito. (shrink)

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that there should be a canonical function from sequent proofs to proof nets, it should be possible to check (...) the correctness of a net in polynomial time, every correct net should be obtainable from a sequent calculus proof, and there should be a cut-elimination procedure which preserves correctness.Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley [22], the author presented a calculus of proof nets satisfying and ; the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of . That sequent calculus, called LK⁎LK⁎ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper [22]), we give a full proof of for expansion nets with respect to LK⁎LK⁎, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria. (shrink)

Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in (...) a previous work we presented a sequent system for TML with the cut-elimination property. Besides, in this same work, it was also presented a sound and complete natural deduction system for this logic. In the present article we continue with the study of TML under a proof-theoretic perspective. In the first place, we show that the natural deduction system that we introduced before admits a normalization theorem. In the second place, taking advantage of the contrapositive implication for the tetravalent modal algebras introduced by A. V. Figallo and P. Landini, we define a decidable tableau system adequate to check validity in the logic TML. Finally, we provide a sound and complete tableau system for TML in the original language. These two tableau systems constitute new (proof-theoretic) decision procedures for checking validity in the variety of tetravalent modal algebras. (shrink)

In Prawitz’s semantics, the validity of an argument may be defined, either relatively to an atomic base which determines the meaning of the non-logical terminology, or relatively to the whole class of atomic bases, namely as logical validity. In the first case, which may be qualified as local, one has to choose whether validity of arguments is or not monotonic over expansions of bases, while in the second case, which may be qualified as global, one has to choose whether the (...) reduction functions which justify non-primitive inferences are or not base-depending. I claim that these oppositions enjoy some conceptual symmetries, and that these symmetries may be understood as putting restrictions on one’s choice both at the local and at the global level. This produces two different proof-theoretic semantics in line with Prawitz’s tenets. However, I also argue that the symmetries stem from a deeper interaction within Prawitz’s semantics, i.e. non-logical meanings vs interpretation of rules. This interaction is in turn based on some primitive ingredients which, when suitably combined, produce other two Prawitz-compatible readings. The four readings form a diagram where some order relations hold. I finally claim that this diagram is complete, namely that, if we combine the ingredients in ways other than those giving rise to the four readings above, we obtain nothing new, or nothing compatible with general semantic requirements. Thus, symmetries between the local and the global level, and interaction between non-logical meaning and interpretation of rules, produce a complete classification of potential Prawitzian semantics. (shrink)

We formulate Hilbert’s epsilon calculus in the context of expansion proofs. This leads to a simplified proof of the epsilon theorems by disposing of the need for prenexification, Skolemisation, and their respective inverse transformations. We observe that the natural notion of cut in the epsilon calculus is associative.

Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories: iterate adding consistency of some weak base theory until you “hit” the target theory. Turing progressions based on n-consistency give rise to a \ proof-theoretic ordinal \ also denoted \. As such, to each theory U we can assign the sequence of corresponding \ ordinals \. We call this sequence a Turing-Taylor expansion or spectrum of a theory. In this paper, we relate Turing-Taylor (...) expansions of sub-theories of Peano Arithmetic to Ignatiev’s universal model for the closed fragment of the polymodal provability logic \. In particular, we observe that each point in the Ignatiev model can be seen as Turing-Taylor expansions of formal mathematical theories. Moreover, each sub-theory of Peano Arithmetic that allows for a Turing-Taylor expansion will define a unique point in Ignatiev’s model. (shrink)

In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by Dummett. (...) As recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one. (shrink)

One of the most fundamental questions in the philosophy of mathematics concerns the relation between truth and formal proof. The position according to which the two concepts are the same is called deflationism, and the opposing viewpoint substantialism. In an important result of mathematical logic, Kurt Gödel proved in his first incompleteness theorem that all consistent formal systems containing arithmetic include sentences that can neither be proved nor disproved within that system. However, such undecidable Gödel sentences can be established (...) to be true once we expand the formal system with Alfred Tarski s semantical theory of truth, as shown by Stewart Shapiro and Jeffrey Ketland in their semantical arguments for the substantiality of truth. According to them, in Gödel sentences we have an explicit case of true but unprovable sentences, and hence deflationism is refuted. -/- Against that, Neil Tennant has shown that instead of Tarskian truth we can expand the formal system with a soundness principle, according to which all provable sentences are assertable, and the assertability of Gödel sentences follows. This way, the relevant question is not whether we can establish the truth of Gödel sentences, but whether Tarskian truth is a more plausible expansion than a soundness principle. In this work I will argue that this problem is best approached once we think of mathematics as the full human phenomenon, and not just consisting of formal systems. When pre-formal mathematical thinking is included in our account, we see that Tarskian truth is in fact not an expansion at all. I claim that what proof is to formal mathematics, truth is to pre-formal thinking, and the Tarskian account of semantical truth mirrors this relation accurately. -/- However, the introduction of pre-formal mathematics is vulnerable to the deflationist counterargument that while existing in practice, pre-formal thinking could still be philosophically superfluous if it does not refer to anything objective. Against this, I argue that all truly deflationist philosophical theories lead to arbitrariness of mathematics. In all other philosophical accounts of mathematics there is room for a reference of the pre-formal mathematics, and the expansion of Tarkian truth can be made naturally. Hence, if we reject the arbitrariness of mathematics, I argue in this work, we must accept the substantiality of truth. Related subjects such as neo-Fregeanism will also be covered, and shown not to change the need for Tarskian truth. -/- The only remaining route for the deflationist is to change the underlying logic so that our formal languages can include their own truth predicates, which Tarski showed to be impossible for classical first-order languages. With such logics we would have no need to expand the formal systems, and the above argument would fail. From the alternative approaches, in this work I focus mostly on the Independence Friendly (IF) logic of Jaakko Hintikka and Gabriel Sandu. Hintikka has claimed that an IF language can include its own adequate truth predicate. I argue that while this is indeed the case, we cannot recognize the truth predicate as such within the same IF language, and the need for Tarskian truth remains. In addition to IF logic, also second-order logic and Saul Kripke s approach using Kleenean logic will be shown to fail in a similar fashion. (shrink)

The classical Glivenko theorem asserts that a propositional formula admits a classical proof if and only if its double negation admits an intuitionistic proof. By a natural expansion of the BCK-logic with negation we understand an algebraizable logic whose language is an expansion of the language of BCK-logic with negation by a family of connectives implicitly defined by equations and compatible with BCK-congruences. Many of the logics in the current literature are natural expansions of BCK-logic with (...) negation. The validity of the analogous of Glivenko theorem in these logics is equivalent to the validity of a simple one-variable formula in the language of BCK-logic with negation. (shrink)

A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover (...) which represents proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed -calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions. (shrink)

This paper dwells upon formal models of changes of beliefs, or theories, which are expressed in languages containing a binary conditional connective. After defining the basic concept of a (non-trivial) belief revision model. I present a simple proof of Gärdenfors''s (1986) triviality theorem. I claim that on a proper understanding of this theorem we must give up the thesis that consistent revisions (additions) are to be equated with logical expansions. If negated or might conditionals are interpreted on the basis (...) of autoepistemic omniscience, or if autoepistemic modalities (Moore) are admitted, even more severe triviality results ensue. It is argued that additions cannot be philosophically construed as parasitic (Levi) on expansions. In conclusion I outline somed logical consequences of the fact that we must not expect monotonic revisions in languages including conditionals. (shrink)

oris, 1986, 17-34, Seminarberichte 86, Humboldt University, Berlin, where, with G. Cherlin, we gave a detailed proof of a result of Alexei L. Semenov that the theory of (N, +, 2x) is decidable and admits quantifier elimination in an expansion of the language containing the Presburger..

Chapter 1 constitutes an introduction to Gentzen calculi from two perspectives, logical and philosophical. It introduces the notion of generalisations of Gentzen sequent calculus and the discussion on properties that characterize good inferential systems. Among the variety of Gentzen-style sequent calculi, I divide them in two groups: syntactic and semantic generalisations. In the context of such a discussion, the inferentialist philosophy of the meaning of logical constants is introduced, and some potential objections – mainly concerning the choice of working with (...) semantic generalizations – are addressed. Finally, I’ll introduce the case studies that I’ll be dealing with in part II. Chapter 2 is concerned with the origins and development of Jaśkowski’s discussive logic. The main idea of this chapter is to systematize the various stages of the development of discussive logic related researches from two different angles, i.e., its connections to modal logics and its proof theory, by highlighting virtues and vices. Chapter 3 focuses on the Gentzen-style proof theory of discussive logic, by providing a characterization of it in terms of labelled sequent calculi. Chapter 4 deals with the Gentzen-style proof theory of relevant logics, again by employing the methodology of labelled sequent calculi. This time, instead of working with a single logic, I’ll deal with a whole family of them. More precisely, I’ll study in terms of proof systems those relevant logics that can be characterised, at the semantic level, by reduced Routley-Meyer models, i.e., relational structures with a ternary relation between states and a unique base element. Chapter 5 investigates the proof theory of a modal expansion of intuitionistic propositional logic obtained by adding an ‘actuality’ operator to the connectives. This logic was introduced also using Gentzen sequents. Unfortunately, the original proof system is not cut-free. This chapter shows how to solve this problem by moving to hypersequents. Chapter 6 concludes the investigations and discusses the future of the research presented throughout the dissertation. (shrink)

In 1969, De Jongh proved the “maximality” of a fragment of intuitionistic predicate calculus forHA. Leivant strengthened the theorem in 1975, using proof-theoretical tools (normalisation of infinitary sequent calculi). By a refinement of De Jongh's original method (using Beth models instead of Kripke models and sheafs of partial combinatory algebras), a semantical proof is given of a result that is almost as good as Leivant's. Furthermore, it is shown thatHA can be extended to Higher Order Heyting Arithmetic+all trueΠ (...) 2 0 -sentences + transfinite induction over primitive recursive well-orderings. As a corollary of the proof, maximality of intuitionistic predicate calculus is established wrt. an abstract realisability notion defined over a suitable expansion ofHA. (shrink)

We investigate the substitution Frege () proof system and its relationship to extended Frege () in the context of modal and superintuitionistic propositional logics. We show that is p-equivalent to tree-like , and we develop a “normal form” for -proofs. We establish connections between for a logic L, and for certain bimodal expansions of L.We then turn attention to specific families of modal and si logics. We prove p-equivalence of and for all extensions of , all tabular logics, all (...) logics of finite depth and width, and typical examples of logics of finite width and infinite depth. In most cases, we actually show an equivalence with the usual system for classical logic with respect to a naturally defined translation.On the other hand, we establish exponential speed-up of over for all modal and si logics of infinite branching, extending recent lower bounds by P. Hrubeš. We develop a model-theoretical characterization of maximal logics of infinite branching to prove this result. (shrink)

This paper deals with some strengthenings of the non-directional product-free Lambek calculus by means of additional structural rules. In fact, the rules contraction and expansion are restricted to basic types. For each of the presented systems the usual proof-theoretic notions are discussed, some new concepts especially designed for these calculi are introduced reflecting their intermediate position between the weaker and the stronger sequent-systems.

Generalizing Cooper’s method of quantifier elimination for Presburger arithmetic, we give a new proof that all parametric Presburger families \ [as defined by Woods ] are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f for every polynomial \. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic by multiplication by scalars \: \alpha \in R, t \in X\}\) where R is any ring of functions from (...) X into \. (shrink)

The aesthetic techniques used in The Expanse are indicative of the infinite space that is an essential and ever‐present character in the show. The cinematography and set design of The Expanse make extensive use of chiaroscuro—a famous artistic technique in the history of painting. For some reason, the infinity of The Expanse attracts us. The look and design of the show indulges us in an experience of the sublime. The dynamically sublime is an experience of infinite power, but not where (...) our survival is threatened by it. The experience of the sublime is one proof of freedom. The absence of the ability to know the significance of what one does in the context of the infinite does not diminish the significance of what they do. The characters of The Expanse know this. They act because they know they must, and they have faith that what they do matters. (shrink)

We develop a combinatorial model to study the evolution of graphs underlying proofs during the process of cut elimination. Proofs are two-dimensional objects and differences in the behavior of their cut elimination can often be accounted for by differences in their two-dimensional structure. Our purpose is to determine geometrical conditions on the graphs of proofs to explain the expansion of the size of proofs after cut elimination. We will be concerned with exponential expansion and we give upper and (...) lower bounds which depend on the geometry of the graphs. The lower bound is computed passing through the notion of universal covering for directed graphs. In this paper we present ground material for the study of cut elimination and structure of proofs in purely combinatorial terms. We develop a theory of duplication for directed graphs and derive results on graphs of proofs as corollaries. (shrink)

Cholak, Goncharov, Khoussainov, and Shore [1] showed that for each k > 0 there is a computably categorical structure whose expansion by a constant has computable dimension k. We show that the same is true with k replaced by ω. Our proof uses a version of Goncharov's method of left and right operations.

We define the notion of a combinatorics of a first order structure, and a relation of covering between first order structures and propositional proof systems. Namely, a first order structure M combinatorially satisfies an L-sentence Φ iff Φ holds in all L-structures definable in M. The combinatorics Comb(M) of M is the set of all sentences combinatorially satisfied in M. Structure M covers a propositional proof system P iff M combinatorially satisfies all Φ for which the associated sequence (...) of propositional formulas 〈Φ〉 n , encoding that Φ holds in L-structures of size n, have polynomial size P-proofs. That is, Comb(M) contains all Φ feasibly verifiable in P. Finding M that covers P but does not combinatorially satisfy Φ thus gives a super polynomial lower bound for the size of P-proofs of 〈Φ〉 n . We show that any proof system admits a class of structures covering it; these structures are expansions of models of bounded arithmetic. We also give, using structures covering proof systems R * (log) and PC, new lower bounds for these systems that are not apparently amenable to other known methods. We define new type of propositional proof systems based on a combinatorics of (a class of) structures. (shrink)

“Black box argument” is a metaphor for modular components of argumentative discussion that are, within a particular discussion, not open to expansion. In public policy debate such as the controversy over abstinence-only sex education, scientific conclusions enter the discourse as black boxes consisting of a result returned from an external and largely impenetrable process. In one way of looking at black box arguments, there is nothing fundamentally new for the argumentation theorist: A black box argument is very like any (...) other appeal to authority, and what might be said about any particular form of black box will turn out to be a particularized version of what might be said about evaluating arguments based on authority. But in another way of looking at black box arguments, they are a constantly evolving technology for coming to conclusions and making these conclusions broadly acceptable. Black boxes are to argumentation what material inventions are to engineering and related sciences. They are anchored in and constrained by fundamental natural processes, but they are also new things that require theoretical explication and practical assessment. (shrink)

The paper studies the extension of harmony and stability, major themes in proof-theoretic semantics, from single-conclusion natural-deduction systems to multiple -conclusions natural-deduction, independently of classical logic. An extension of the method of obtaining harmoniously-induced general elimination rules from given introduction rules is suggested, taking into account sub-structurality. Finally, the reductions and expansions of the multiple -conclusions natural-deduction representation of classical logic are formulated.

In the proof-theoretic semantics approach to meaning, harmony , requiring a balance between introduction-rules (I-rules) and elimination rules (E-rules) within a meaning conferring natural-deduction proof-system, is a central notion. In this paper, we consider two notions of harmony that were proposed in the literature: 1. GE-harmony , requiring a certain form of the E-rules, given the form of the I-rules. 2. Local intrinsic harmony : imposes the existence of certain transformations of derivations, known as reduction and expansion (...) . We propose a construction of the E-rules (in GE-form) from given I-rules, and prove that the constructed rules satisfy also local intrinsic harmony. The construction is based on a classification of I-rules, and constitute an implementation to Gentzen’s (and Pawitz’) remark, that E-rules can be “read off” I-rules. (shrink)

Connexive expansions of relevant logics tend to prove every negated implication formula. In this paper I discuss why they tend to satisfy this unsavoury property, and discuss avenues by which it can be avoided, providing logics which stand as proofs of concept that these avenues can be made to work.

This paper reports on the integration of the higher-order theorem proving environment TPS [Andrews96] into the mathematical assistant OMEGA [Omega97]. TPS can be called from OMEGA either as a black box or as an interactive system. In black box mode, the user has control over the parameters which control proof search in TPS; in interactive mode, all features of the TPS-system are available to the user. If the subproblem which is passed to TPS contains concepts defined in OMEGA’s database (...) of mathematical theories, these definitions are not instantiated but are also passed to TPS. Using a special theory which contains proof tactics that model the ND-calculus variant of TPS within OMEGA, any complete or partial proof generated in TPS can be translated one to one into an OMEGA proof plan. Proof transformation is realised by proof plan expansion in OMEGA’s 3-dimensional proof data structure, and remains transparent to the user. (shrink)

A heuristic proof is given that the divergent QCD perturbation series is, asymptotic. By treating it as an asymptotic expansion we show that it makes sense to keep only the first few terms. The example of e+e− annihilation is considered. It is shown that by keeping only the first few terms one can get within a per cent (or smaller) of the complete sum of the series even at very low momenta where the coupling is large. More generally, (...) this affords an explanation of the phenomena of precocious scaling and why keeping only leading order corrections generally works so well. (shrink)

Three years of work with more than twenty scientists and high-level specialists: here are revealed the modern proofs of the existence of God. For almost four centuries, from Copernicus to Freud via Galileo and Darwin, scientific discoveries have accumulated in a spectacular way, giving the impression that it was possible to explain the Universe without the need to resort to a god. Creator. And so it was that at the beginning of the 20th century, materialism triumphed intellectually. In a way (...) as unexpected as it is surprising, the pendulum of science has swung back in the other direction, with incredible force. The discoveries of Relativity, quantum mechanics, the expansion of the Universe, its thermal death, the Big Bang, the fine tuning of the Universe or the complexity of living things, have followed one another. This new knowledge came to dynamite the certainties anchored in the collective spirit of the 20th century, to the point that we can say today that materialism, which has never been just a belief like any other, is on the way to become an irrational belief. In a language accessible to all, the authors of this book retrace the history of these advances in a fascinating way and offer a rigorous overview of the new proofs of the existence of God. At the dawn of the 20th century, believing in a creator god seemed to oppose science. Today, wouldn't it be the opposite? An invitation to reflection and debate. (shrink)

The article presents proofs of the context freeness of a family of typelogical grammars, namely all grammars that are based on a uni- ormultimodal logic of pure residuation, possibly enriched with thestructural rules of Permutation and Expansion for binary modes.

We give a new proof of the subanalyticity of the regular locus of a p-adic subanalytic set, replacing use of an approximation theorem by a more natural argument based on the flatness of certain homomorphisms given by Taylor expansions of strictly convergent power series at a non-standard point of Zmp.

We study an expansion of the Distributive Non-associative Lambek Calculus with conjugates of the Lambek product operator and residuals of those conjugates. The resulting logic is well-motivated, under-investigated and difficult to tackle. We prove completeness for some of its fragments and establish that it is decidable. Completeness of the logic is an open problem; some difficulties with applying the usual proof method are discussed.

We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in the (...) given signature; if instead of adding Reiteration, one adds the rule of Reductio ad Absurdum, one obtains a proof system for orthologic; by adding both Reiteration and Reductio, one obtains a proof system for classical logic. Arguably neither Reiteration nor Reductio is as intimately related to the meaning of the connectives as the introduction and elimination rules are, so the base logic we identify serves as a more fundamental starting point and common ground between proponents of intuitionistic logic, orthologic, and classical logic. The algebraic semantics for the logic we motivate proof-theoretically is based on bounded lattices equipped with what has been called a weak pseudocomplementation. We show that such lattice expansions are representable using a set together with a reflexive binary relation satisfying a simple first-order condition, which yields an elegant relational semantics for the logic. This builds on our previous study of representations of lattices with negations, which we extend and specialize for several types of negation in addition to weak pseudocomplementation; in an appendix, we further extend this representation to lattices with implications. Finally, we discuss adding to our logic a conditional obeying only introduction and elimination rules, interpreted as a modality using a family of accessibility relations. (shrink)

Philosophers are divided on whether the proof- or truth-theoretic approach to logic is more fruitful. The paper demonstrates the considerable explanatory power of a truth-based approach to logic by showing that and how it can provide (i) an explanatory characterization —both semantic and proof-theoretical—of logical inference, (ii) an explanatory criterion for logical constants and operators, (iii) an explanatory account of logic’s role (function) in knowledge, as well as explanations of (iv) the characteristic features of logic —formality, strong modal (...) force, generality, topic neutrality, basicness, and (quasi-)apriority, (v) the veridicality of logic and its applicability to science, (v) the normativity of logic, (vi) error, revision, and expansion in/of logic, and (vii) the relation between logic and mathematics. The high explanatory power of the truth-theoretic approach does not rule out an equal or even higher explanatory power of the proof-theoretic approach. But to the extent that the truth-theoretic approach is shown to be highly explanatory, it sets a standard for other approaches to logic, including the proof-theoretic approach. (shrink)

We consider first-order infinite-valued Łukasiewicz logic and its expansion, first-order rational Pavelka logic RPL∀. From the viewpoint of provability, we compare several Gentzen-type hypersequent calculi for these logics with each other and with Hájek’s Hilbert-type calculi for the same logics. To facilitate comparing previously known calculi for the logics, we define two new analytic calculi for RPL∀ and include them in our comparison. The key part of the comparison is a density elimination proof that introduces no cuts for (...) one of the hypersequent calculi considered. (shrink)

The spectrum of a relation on a computable structure is the set of Turing degrees of the image of R under all isomorphisms between and any other computable structure . The relation is intrinsically computably enumerable if its image under all such isomorphisms is c.e. We prove that any computable partially ordered set is isomorphic to the spectrum of an intrinsically c.e. relation on a computable structure. Moreover, the isomorphism can be constructed in such a way that the image of (...) the minimum element of the partially ordered set is computable. This solves the spectrum problem. The theorem and modifications of its proof produce computably categorical structures whose expansions by finite number of constants are not computably categorical and, indeed, ones whose expansions can have any finite number of computable isomorphism types. They also provide examples of computably categorical structures that remain computably categorical under expansions by constants but have no Scott family. (shrink)

Developing a suggestion by Russell, Prawitz showed how the usual natural deduction inference rules for disjunction, conjunction and absurdity can be derived using those for implication and the second order quantifier in propositional intuitionistic second order logic NI\. It is however well known that the translation does not preserve the relations of identity among derivations induced by the permutative conversions and immediate expansions for the definable connectives, at least when the equational theory of NI\ is assumed to consist only of (...) \- and \-equations. On the basis of the categorial interpretation of NI\, we introduce a new class of equations expressing what in categorial terms is a naturality condition satisfied by the transformations interpreting NI\-derivations. We show that the Russell–Prawitz translation does preserve identity of proof with respect to the enriched system by highlighting the fact that naturality corresponds to a generalized permutation principle. Finally we sketch how these results could be used to investigate the properties of connectives definable in the framework of higher-level rules. (shrink)

Consider a definably complete uniformly locally o-minimal expansion of the second kind of a densely linearly ordered abelian group. Let $f:X \rightarrow R^n$ be a definable map, where X is a definable set and R is the universe of the structure. We demonstrate the inequality $\dim ) \leq \dim $ in this paper. As a corollary, we get that the set of the points at which f is discontinuous is of dimension smaller than $\dim $. We also show that (...) the structure is definably Baire in the course of the proof of the inequality. (shrink)

The paper discusses tools for teaching logic used in Logic & Proofs, a web-based introduction to modern logic that has been taken by more than 1,300 students since the fall of 2003. The tools include a wide array of interactive learning environments or cognitive mini-tutors; most important among them is the Carnegie Proof Lab. The Proof Lab is a sophisticated interface for constructing natural deduction proofs and is central, as strategically guided discovery of proofs is the distinctive focus (...) of the course. My discussion makes explicit the broader intellectual context, but also the pursuit of pedagogical goals and their experimental examination. The intellectual context includes i) the theoretical background for the proof search algorithm AProS and its use for a dynamic Proof Tutor, and ii) the programmatic expansion of the course to Computational Logic. 1. (shrink)

We show that, assuming the Axiom of Determinacy, every non-selfdual Wadge class can be constructed by starting with those of level $\omega _1$ and iteratively applying the operations of expansion and separated differences. The proof is essentially due to Louveau, and it yields at the same time a new proof of a theorem of Van Wesep. The exposition is self-contained, except for facts from classical descriptive set theory.

We give a short proof of the Marker–Steinhorn theorem for o-minimal expansions of ordered groups. The key tool is Ramakrishnan’s classification of definable linear orders in such structures.

The logic DAI of demodalised analytic implication has been introduced by J.M. Dunn as a variation on a time-honoured logical system by C.I. Lewis’ student W.T. Parry. The main tenet underlying this logic is that no implication can be valid unless its consequent is “analytically contained” in its antecedent. DAI has been investigated both proof-theoretically and model-theoretically, but no study so far has focussed on DAI from the viewpoint of abstract algebraic logic. We provide several different algebraic semantics for (...) DAI, showing their equivalence with the known semantics by Dunn and Epstein. We also show that DAI is algebraisable and we identify its equivalent quasivariety semantics. This class turns out to be a linguistic and axiomatic expansion of involutive bisemilattices, a subquasivariety of which forms the algebraic counterpart of Paraconsistent Weak Kleene logic. This fact sheds further light on the relationship between containment logics and logics of nonsense. (shrink)

Using nonstandard methods we construct a model of an induction scheme called inside a "resource" of the form is a Turing machine of code is calculated in less than , where means the length of the binary expansion of and are nonstandard parameters in a model of . As a consequence we obtain a model theoretic proof of a witnessing theorem for this theory by functions computable in time , a result first obtained by Buss, Krajícek, and Takeuti (...) using proof theory. (shrink)

Kripke recently suggested viewing the intuitionistic continuum as an expansion in time of a definite classical continuum. We prove the classical consistency of a three-sorted intuitionistic formal system IC, simultaneously extending Kleene’s intuitionistic analysis I and a negative copy C° of the classically correct part of I, with an “end of time” axiom ET asserting that no choice sequence can be guaranteed not to be pointwise equal to a definite sequence. “Not every sequence is pointwise equal to a definite (...) sequence” is independent of IC. The proofs are by Crealizability interpretations based on classical ω-models ${\cal M}$ = $\left$ of C°. (shrink)

Ultralogic as Universal? is a seminal text in non-classcial logic. Richard Routley presents a hugely ambitious program: to use an 'ultramodal' logic as a universal key, which opens, if rightly operated, all locks. It provides a canon for reasoning in every situation, including illogical, inconsistent and paradoxical ones, realized or not, possible or not. A universal logic, Routley argues, enables us to go where no other logic—especially not classical logic—can. Routley provides an expansive and singular vision of how a universal (...) logic might one day solve major problems in set theory, arithmetic, linguistics, physics, and more. It circulated in typescript in the late 1970s before appearing as the Appendix to Exploring Meinong's Jungle and Beyond. With engaging, forceful prose, unsparing criticism of entrenched institutions, and many tantalizing proof sketches, Ultralogic? has had a major influence on the development of paraconsistent and relevant logic. This new edition makes this work available for a modern audience, newly typeset and corrected, along with extensive notes, and new commentary essays. (shrink)

The tetravalent modal logic is one of the two logics defined by Font and Rius :481–518, 2000) in connection with Monteiro’s tetravalent modal algebras. These logics are expansions of the well-known Belnap–Dunn’s four-valued logic that combine a many-valued character with a modal character. In fact, $${\mathcal {TML}}$$ TML is the logic that preserves degrees of truth with respect to tetravalent modal algebras. As Font and Rius observed, the connection between the logic $${\mathcal {TML}}$$ TML and the algebras is not so (...) good as in $${{\mathcal {TML}}}^N$$ TML N, but, as a compensation, it has a better proof-theoretic behavior, since it has a strongly adequate Gentzen calculus :481–518, 2000). In this work, we prove that the sequent calculus given by Font and Rius does not enjoy the cut-elimination property. Then, using a general method proposed by Avron et al., we provide a sequent calculus for $${\mathcal {TML}}$$ TML with the cut-elimination property. Finally, inspired by the latter, we present a natural deduction system, sound and complete with respect to the tetravalent modal logic. (shrink)

Let (M, ≤,...) denote a Boolean ordered o-minimal structure. We prove that a Boolean subalgebra of M determined by an algebraically closed subset contains no dense atoms. We show that Boolean algebras with finitely many atoms do not admit proper expansions with o-minimal theory. The proof involves decomposition of any definable set into finitely many pairwise disjoint cells, i.e., definable sets of an especially simple nature. This leads to the conclusion that Boolean ordered structures with o-minimal theories are essentially (...) bidefinable with Boolean algebras with finitely many atoms, expanded by naming constants. We also discuss the problem of existence of proper o-minimal expansions of Boolean algebras. (shrink)

Elizabeth Anderson exalts the transition from the aristocratic to the modern ethic of debt as one of the most significant cultural achievements of capitalism. Whereas the debitor was once forced to compromise his liberty, dignity, and equality, today the rights and freedoms of insolvents are legally protected, and disadvantaged members of the community can readily obtain credit without personal supplication. Anderson’s intuition was, until recently, widely shared. Then came the financial crisis of 2007-08 and the ensuing global recession, triggered by (...) mass defaults among “sub-prime” borrowers. Many had entered the mortgage market with no proof of income, no assets behind them, no down-payment, a chequered credit history, and a generally reduced repayment capacity. Suddenly a flurry of criticism was unleashed against the lowering of credit standards and the government programs which pressured lenders to service the poor. My aim in this paper is not to assess the democratization of credit from the point of view of economic efficiency or political prudence, but rather to provide a much needed ethical appraisal. Any number of reasons might be advanced for why a particular government policy is morally objectionable. I will concentrate on the least controversial reason conceivable: the policy violates the rights of citizens. Whether this is true of government-driven credit-democratization - specifically, whether it violates the rights of the lenders compelled to act as agents of the policy, the rights of the third parties exposed to the risks associated with the expansion of credit markets, or both – is the question that I take up here. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:Journal of the History of Ideas 63.2 (2002) 261-282 [Access article in PDF] The "Progress of Ambition": Character, Narrative, and Philosophy in the Works of William Robertson Neil Hargraves In his biography of William Robertson, Dugald Stewart claimed that by "few writers of the present age has [the] combination of philosophy with history been more often attempted than by Dr. Robertson; and by none have the inconveniences which it (...) threatens been more successfully avoided." 1 At first sight Stewart's assertion seems puzzling. Arnaldo Momigliano considered Robertson to be less successful than Edward Gibbon in his integration of the three elements of eighteenth-century historical writing, philosophy, narrative, and erudition. 2 Despite Robertson's stated belief that "arrangement" was the principal task of the historian, his organizational framework appeared to foster separation rather than integration. 3 Thus, his central work, The History of the Reign of Charles V (1769), is divided into three discrete parts. An apparently conventional narrative of high politics and diplomacy is prefaced by an essay on medieval Europe, A View of the Progress of Society in Europe, which was regarded by his contemporaries as a classic of "philosophical" history, 4 while [End Page 261] Robertson appended to both copious "Proofs and Illustrations." The structure of The History of America (1777) is even less integrated, despite criticalpraise of its "regular plan... complete narration and perfect whole." 5 To other critics his interpolation of dissertations upon the "condition and character" of the Americans, Mexicans, and Peruvians, seemed to sever the thread of the narrative and consequently to break up the unity of the work. 6 Yet as this paper will seek to demonstrate, there was a vital connection between the narrative and "philosophical" components of Robertson's major histories: the theoretical dissertations served recognizably narrative purposes. The bridge between them lies in the complex notion of character created by the expansion of historical forms in the eighteenth century."Philosophical" history defined itself in opposition to the vacuities and muddles of conventional political-diplomatic historical narrative. Its advantages over narrative were various: the revelation of general rather than particular causes, grounding the history on more certain and less random principles: 7 the penetration of causes "insensible" and invisible to the eyes of a careless observer, obscured by the "great theatre of the world"; 8 a broadening of the subject-matter, away from the mere rehearsal of the struggles between crown and nobility or fixation with constitution and government, towards a more inclusive and heterogeneous history of "manners, including arts, sciences, society" and what today would be termed "mentalities," and, related to the last point, a principle of organization that would reduce the apparent chaos and multiplicity of the past to a simple and luminous plan of arrangement. 9 This was the most exacting requirement for the philosophical historian. As a critic wrote of Robertson's View, its value lay most in its "vast and magnificent plan... that profound and easy art of classing [facts], in such a manner that... the accumulated multiplicity of events is gradually reduced to a small number." It [End Page 262] required a more "elevated view... above all discussions and disputes." 10 Philosophic history aimed to strip away the illusion of appearances and substitute an unseen but more regular and systematic history. In its more ambitious formulations it aimed not simply at a universal history of mankind but at no less than a "history of the human mind": an attempt to explain through historical description the enormous gulf that separated modern man from his savage ancestor. As Robertson himself famously declared in Book IV of America, In order to complete the history of the human mind, and attain to a perfect knowledge of its nature and operations, we must contemplate man in all those various situations wherein he has been placed. We must follow him in his progress through the different stages of society, as he gradually advances from the infant state of civil life towards its maturity and decline. (VIII, 49-50) This was a history of progress... (shrink)