We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E1, a theory axiomatized by T → ⊥. The intersection CPC ∩ E1 is axiomatizable by the Principle of the Excluded Middle A V ∨ ⌝A. If B (...) is a formula such that → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula → B is derivable exactly when B is provably equivalent to a formula of the form → A) →. (shrink)

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 1, C 2 be formulas over ?, such that (...) A∧C 1⊢C 2. Then there exists a formula B over ℳ such that A⊢B and B∧C 1⊢C 2. (shrink)

The most basic laws and principles of the Predicate Calculus, also known as Quantification Theory, are stated, as clearly and concisely as possible.

We establish a completeness theorem for first-order basic predicate logic BQC, a proper subsystem of intuitionistic predicate logic IQC, using Kripke models with transitive underlying frames. We develop the notion of functional well-formed theory as the right notion of theory over BQC for which strong completeness theorems are possible. We also derive the undecidability of basic arithmetic, the basic logic equivalent of intuitionistic Heyting Arithmetic and classical Peano Arithmetic.

We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination (...) theorem isproved in a syntactic way by modifying Gentzen's method. Thisdual-context style system exemplifies the effectiveness of dual-contextformulation in formalizing various non-classical logics. (shrink)

The calculus of Natural Calculation is introduced as an extension of Natural Deduction by proper term rules. Such term rules provide the capacity of dealing directly with terms in the calculus instead of the usual reasoning based on equations, and therefore the capacity of a natural representation of informal mathematical calculations. Basic proof theoretic results are communicated, in particular completeness and soundness of the calculus; normalisation is briefly investigated. The philosophical impact on a proof theoretic account (...) of the notion of meaning is considered. (shrink)

The derivative is a basic concept of differential calculus. However, if we calculate the derivative as change in distance over change in time, the result at any instant is 0/0, which seems meaningless. Hence, Newton and Leibniz used the limit to determine the derivative. Their method is valid in practice, but it is not easy to intuitively accept. Thus, this article describes the novel method of differential calculus based on the double contradiction, which is easier to accept (...) intuitively. Next, the geometrical meaning of the double contradiction is considered as follows. A tangent at a point on a convex curve is iterated. Then, the slope of the tangent at the point is sandwiched by two kinds of lines. The first kind of line crosses the curve at the original point and a point to the right of it. The second kind of line crosses the curve at the original point and a point to the left of it. Then, the double contradiction can be applied, and the slope of the tangent is determined as a single value. Finally, the meaning of this method for the foundation of mathematics is considered. We reflect on Dehaene’s notion that the foundation of mathematics is based on the intuitions, which evolve independently. Hence, there may be gaps between intuitions. In fact, the Ancient Greeks identified inconsistency between arithmetic and geometry. However, Eudoxus developed the theory of proportion, which is equivalent to the Dedekind Cut. This allows the iteration of an irrational number by rational numbers as precisely as desired. Simultaneously, we can define the irrational number by the double contradiction, although its existence is not guaranteed. Further, an area of a curved figure is iterated and defined by rectilinear figures using the double contradiction. (shrink)

We introduce a Gentzen-style sequent calculus axiomatization for Basic Predicate Calculus. Our new axiomatization is an improvement of the previous axiomatizations, in the sense that it has the subformula property. In this system the cut rule is eliminated.

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.

This textbook for the undergraduate vector calculus course presents a unified treatment of vector and geometric calculus. It is a sequel to my Linear and Geometric Algebra. That text is a prerequisite for this one. -/- Linear algebra and vector calculus have provided the basic vocabulary of mathematics in dimensions greater than one for the past one hundred years. Just as geometric algebra generalizes linear algebra in powerful ways, geometric calculus generalizes vector calculus in (...) powerful ways. (shrink)

We introduce a two-valued and a three-valued truth-valuational substitutional semantics for the Quantified Argument Calculus (Quarc). We then prove that the 2-valid arguments are identical to the 3-valid ones with strict-to-tolerant validity. Next, we introduce a Lemmon-style Natural Deduction system and prove the completeness of Quarc on both two- and three-valued versions, adapting Lindenbaum’s Lemma to truth-valuational semantics. We proceed to investigate the relations of three-valued Quarc and the Predicate Calculus (PC). Adding a logical predicate T to Quarc, (...) true of all singular arguments, allows us to represent PC quantification in Quarc and translate PC into Quarc, preserving validity. Introducing a weak existential quantifier into PC allows us to translate Quarc into PC, also preserving validity. However, unlike the translated systems, neither extended system can have a sound and complete proof system with Cut, supporting the claim that these are basically different calculi. (shrink)

Cirquent calculus is a proof system with inherent ability to account for sharing subcomponents in logical expressions. Within its framework, this article constructs an axiomatization $$\text{ CL18 }$$ CL18 of the basic propositional fragment of computability logic—the game-semantically conceived logic of computational resources and tasks. The nonlogical atoms of this fragment represent arbitrary so called static games, and the connectives of its logical vocabulary are negation and the parallel and choice versions of conjunction and disjunction. The main technical (...) result of the article is a proof of the soundness and completeness of $$\text{ CL18 }$$ CL18 with respect to the semantics of computability logic. (shrink)

To sentential language we add an operator C to be read as ‘it changes that…’ and present an axiomatic system in the frame of classical logic to catch some meaning of the term ‘change’. A typical axiom is e.g.: CA implies, a basic rule is: from A it may be inferred (theorems do not change). So this system is not regular. On the semantic level we introduce stages (of the development of some world, of some agents’ convictions or of (...) some argumentation) at which a sentence may be true or false. It turns out that with the help of C, an operator N can be defined whose intuitive meaning is ‘on the next occasion…’ and which behaves like A.N. Prior’s F (and also like the T operator of G.H. von Wright’s read ‘… and next…’). In a book by Świetorzecka (2008) cited below, the philosophical background is described which is the Aristotelian theory of substantial change. The author of this book shows also some metalogical properties of this logic. The aim of this text now is to present a formal extraction of Świetorzecka (2008) with a shortened axiomatisation and to describe some metalogical results. (shrink)

The present introduction to the Fluent Calculus is intended as an ETAI reference article. It summarizes basic definitions and concepts in the Fluent Calculus, and is intended as a reference for future articles where the calculus is used.

The purpose of the paper is to show that by cleaning Classical Logic (CL) from redundancies (irrelevances) and uninformative complexities in the consequence class and from too strong assumptions (of CL) one can avoid most of the paradoxes coming up when CL is applied to empirical sciences including physics. This kind of cleaning of CL has been done successfully by distinguishing two types of theorems of CL by two criteria. One criterion (RC) forbids such theorems in which parts of the (...) consequent (conclusion) can be replaced by arbitrary parts salva validitate of the theorem. The other (RD) reduces the consequences to simplest conjunctive consequence elements. Since the application of RC and RD to CL leads to a logic without the usual closure conditions, an approximation to RC and RD has been constructed by a basic logic with the help of finite (6-valued) matrices. This basic logic called RMQ (relevance, matrix, Quantum Physics) is consistent and decidable. It distinguishes two types of validity (strict validity) and classical or material validity. All theorems of CL (here: classical propositional calculus CPC) are classically or materially valid in RMQ. But those theorems of CPC which obey RC and RD and avoid the difficulties in the application to empirical sciences and to Quantum Physics are separated as strictly valid in RMQ. In the application to empirical sciences in general the proposed logic avoids the well known paradoxes in the area of explanation, confirmation, versimilitude and Deontic Logic. Concerning the application to physics it avoids also the difficulties with distributivity, commensurability and with Bell's inequalities. (shrink)

PREFACE. We present a variety of basic theories involving fundamental concepts of naive thinking, of the sort that were common in "natural philosophy" before the dawn of physical science. The most extreme forms of infinity ever formulated are embodied in the branch of mathematics known as abstract set theory, which forms the accepted foundation for all of mathematics. Each of these theories embodies the most extreme forms of infinity ever formulated, in the following sense. ZFC, and even extensions of (...) ZFC with the so called large cardinal axioms, are mutually interpretable with these theories. This is an extended abstract. Proofs of the claims will appear elsewhere. (shrink)

The Fluent Calculus belongs to the established predicate calculus formalisms for reasoning about actions. Its underlying concept of state update axioms provides a solution to the basic representational and inferential Frame Problems in pure first-order logic. Extending a recent research result, we present a Fluent Calculus to reason about domains involving continuous change and where actions occur concurrently.

It is shown that all the provably total functions of Basic Arithmetic BA, a theory introduced by Ruitenburg based on Predicate Basic Calculus, are primitive recursive. Along the proof a new kind of primitive recursive realizability to which BA is sound, is introduced. This realizability is similar to Kleene's recursive realizability, except that recursive functions are restricted to primitive recursives.

The modal -calculus extends basic modal logic with second-order quantification in terms of arbitrarily nested fixpoint operators. Its satisfiability problem is EXPTIME-complete. Decision procedures for the modal -calculus are not easy to obtain though since the arbitrary nesting of fixpoint constructs requires some combinatorial arguments for showing the well-foundedness of least fixpoint unfoldings. The tableau-based decision procedures so far also make assumptions on the unfoldings of fixpoint formulas, e.g., explicitly require formulas to be in guarded normal form. (...) In this paper we present a tableau calculus for deciding satisfiability of arbitrary, i.e., not necessarily guarded -calculus formulas. It is based on a new unfolding rule for greatest fixpoint formulas which allows unguarded formulas to be handled without an explicit transformation into guarded form, thus avoiding a exponential blow-up in formula size. We prove soundness and completeness of the calculus, and compare it empirically to using guarded transformation instead. The new unfolding rule can also be used to handle nested star operators in PDL formulas correctly. (shrink)

Combinatory logic and lambda-conversion were originally devised in the 1920s for investigating the foundations of mathematics using the basic concept of 'operation' instead of 'set'. They have now developed into linguistic tools, useful in several branches of logic and computer science, especially in the study of programming languages. These notes form a simple introduction to the two topics, suitable for a reader who has no previous knowledge of combinatory logic, but has taken an undergraduate course in predicate calculus (...) and recursive functions. The key ideas and basic results are presented, as well as a number of more specialised topics, and man), exercises are included to provide manipulative practice. (shrink)

This book presents not only the mathematical concept of probability, but also its philosophical aspects, the relativity of probability and its applications and even the psychology of probability. All explanations are made in a comprehensible manner and are supported with suggestive examples from nature and daily life, and even with challenging math paradoxes.

We study the problem of minimizing $\int _\Omega F)\, dx \;$ over the functions $u\in W^{1,1}$ that assume given boundary values $\phi $ on $\Gamma := \partial \Omega $. The lagrangian $F$ and the domain $\Omega $ are assumed convex. A new type of hypothesis on the boundary function $\phi $ is introduced: the lower bounded slope condition. This condition, which is less restrictive than the familiar bounded slope condition of Hartman, Nirenberg and Stampacchia, allows us to extend the classical (...) Hilbert-Haar regularity theory to the case of semiconvex boundary data. We prove in particular that the solution is locally Lipschitz in $\Omega $. In certain cases, as when $\Gamma $ is a polyhedron or else of class $C^{1,1}$, we obtain in addition a global Hölder condition on $\,\overline{\!\,\Omega }$. (shrink)

As with mathematics, logic is easier to do if its symbols and their rules are better. In a graphic way, the logic symbols introduced in thís paper show their truth-table values, their composite truth-functions, and how to say them as either ?or? or ?if ? then? propositions. Simple rules make the converse, add or remove negations, and resolve propositions.

The paper presents the diagrammatic calculus CL, which combines features of tree, Euler-type, Venn-type diagrams and squares of opposition. In its basic form, `CL' (= Cubus Logicus) organizes terms in the form of a square or cube. By applying the arrows of the square of opposition to CL, judgments and inferences can be displayed. Thus CL offers on the one hand an intuitive method to display ontologies and on the other hand a diagrammatic tool to check inferences. The (...) paper focuses mainly on the adaptation of the square of opposition in CL and offers an algebraic notation, which corresponds to the diagrammatic representation. (shrink)

The situation calculus is one of the most established formalisms for reasoning about action and change. In this paper we will review the basics of Reiter’s version of the situation calculus, show how knowledge and time have been addressed in this framework, and point to some of the weaknesses of the situation calculus with respect to time. We then present a modal version of the situation calculus where these problems can be overcome with relative ease and (...) without sacrificing the advantages of the original. (shrink)

We introduce a sequent calculus B for a new logic, named basic logic. The aim of basic logic is to find a structure in the space of logics. Classical, intuitionistic, quantum and non-modal linear logics, are all obtained as extensions in a uniform way and in a single framework. We isolate three properties, which characterize B positively: reflection, symmetry and visibility. A logical constant obeys to the principle of reflection if it is characterized semantically by an equation (...) binding it with a metalinguistic link between assertions, and if its syntactic inference rules are obtained by solving that equation. All connectives of basic logic satisfy reflection. To the control of weakening and contraction of linear logic, basic logic adds a strict control of contexts, by requiring that all active formulae in all rules are isolated, that is visible. From visibility, cut-elimination follows. The full, geometric symmetry of basic logic induces known symmetries of its extensions, and adds a symmetry among them, producing the structure of a cube. (shrink)

In this paper we give relational semantics and an accompanying relational proof theory for full Lambek calculus (a sequent calculus which we denote by FL). We start with the Kripke semantics for FL as discussed in [11] and develop a second Kripke-style semantics, RelKripke semantics, as a bridge to relational semantics. The RelKripke semantics consists of a set with two distinguished elements, two ternary relations and a list of conditions on the relations. It is accompanied by a Kripke-style (...) valuation system analogous to that in [11]. Soundness and completeness theorems with respect to FL hold for RelKripke models. Then, in the spirit of the work of Orlowska [14], [15], and Buszkowski and Orlowska [3], we develop relational logic RFL. The adjective relational is used to emphasize the fact that RFL has a semantics wherein formulas are interpreted as relations. We prove that a sequent Γ → α in FL is provable if and only if a translation, t( $\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ , has a cut-complete fundamental proof tree. This result is constructive: that is, if a cut-complete proof tree for $t(\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ is not fundamental, we can use the failed proof search to build a relational countermodel for $t(\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha)\varepsilon \upsilon u$ and from this, build a RelKripke countermodel for $\gamma_1 \bullet \cdots \bullet \gamma_n \supset \alpha$ . These results allow us to add FL, the basic substructural logic, to the list of those logies of importance in computer science with a relational proof theory. (shrink)

In 1960–1962, E. Kähler enriched É. Cartan’s exterior calculus, making it suitable for quantum mechanics (QM) and not only classical physics. His “Kähler-Dirac” (KD) equation reproduces the fine structure of the hydrogen atom. Its positron solutions correspond to the same sign of the energy as electrons.The Cartan-Kähler view of some basic concepts of differential geometry is presented, as it explains why the components of Kähler’s tensor-valued differential forms have three series of indices. We demonstrate the power of his (...) calculus by developing for the electron’s and positron’s large components their standard Hamiltonian beyond the Pauli approximation, but without resort to Foldy-Wouthuysen transformations or ad hoc alternatives (positrons are not identified with small components in K ähler’s work). The emergence of negative energies for positrons in the Dirac theory is interpreted from the perspective of the KD equation. Hamiltonians in closed form (i.e. exact through a finite number of terms) are obtained for both large and small components when the potential is time-independent.A new but as yet modest new interpretation of QM starts to emerge from that calculus’ peculiarities, which are present even when the input differential form in the Kähler equation is scalar-valued. Examples are the presence of an extra spin term, the greater number of components of “wave functions” and the non-association of small components with antiparticles. Contact with geometry is made through a Kähler type equation pertaining to Clifford-valued differential forms. (shrink)

Epsilon terms indexed by contexts were used by K. von Heusinger to represent definite and indefinite noun phrases as well as some other constructs of natural language. We provide a language and a complete first order system allowing to formalize basic aspects of this representation. The main axiom says that for any finite collection S 1,…,S k of distinct definable sets and elements a 1,…,a k of these sets there exists a choice function assigning a i to S i (...) for all i≤k. We prove soundness and completeness theorems for this system S ε i fin. (shrink)

The interpretation of implications as rules motivates a different left-introduction schema for implication in the sequent calculus, which is conceptually more basic than the implication-left schema proposed by Gentzen. Corresponding to results obtained for systems with higher-level rules, it enjoys the subformula property and cut elimination in a weak form.

We present a novel way of using proof nets for the multimodal Lambek calculus, which provides a general treatment of both the unary and binary connectives. We also introduce a correctness criterion which is valid for a large class of structural rules and prove basic soundness, completeness and cut elimination results. Finally, we will present a correctness criterion for the original Lambek calculus Las an instance of our general correctness criterion.

The issue of the emergence of formal axiomatic logical systems due to the emergence of logical antinomies in formal axiomatic systems, specifically the issue of developing formal logical axiomatics in the calculus of considerations was investigated in the considered research. At the same time, in order to determine the characteristics of the implementation of the logical-methodological principles and provisions of the deductive reasoning obviously, conceptual-logical foundations of the calculus of considerations was studied and the main propositions of the (...) calculus of considerations and the analysis of the initial logical operations on them were given in the study. The basic laws of logic and the expression of one logical act with another one were also explained in the research work by giving the concepst of proportional form and tautology in the calculus of considerations. At the same time, main properties and the procedure of setting of the formal deductive theory in the calculus of considerations were studied in the article. In order to provide an adequate characterization of the conceptual and methodological bases of the calculus of considerations in the research work, the basic logical laws of the calculus of considerations developed by the German mathematician and thinker P. Hilbert were also given. In addition, the main principles and methodological provisions of the deductive method were investigated, and the rules of deriving new conclusions from the axioms were interpreted. At the end of the reviewed article, the main principles and methods of the formal axiomatic mathematical systems built on a deductive basis, specifically the calculus of considerations, were studied and a logical-methodological analysis of the calculus of considerations was carried out on this basis. In this framework, the syntactic and semantic analysis of formalized language in formal axiomatic logical systems was carried out separately, the constituent parts of those systems, including the construction scheme, were given. (shrink)

In A New Form of Agent-Based Virtue Ethics , Daniel Doviak develops a novel agent-based theory of right action that treats the rightness (or deontic status) of an action as a matter of the action’s net intrinsic virtue value (net-IVV)—that is, its balance of virtue over vice. This view is designed to accommodate three basic tenets of commonsense morality: (i) the maxim that “ought” implies “can,” (ii) the idea that a person can do the right thing for the wrong (...) reason, and (iii) the idea that a virtuous person can have “mixed motives.” In this paper, I argue that Doviak’s account makes an important contribution to agent-based virtue ethics, but it needs to be supplemented with a consequentialist account of the efficacy of well-motivated actions—that is, it should be transformed into a mixed (motives-consequences) account, while retaining its net-IVV calculus. This is because I believe that there are right-making properties external to an agent’s psychology which it is important to take into account, especially when an agent’s actions negatively affect other people. To incorporate this intuition, I add to Doviak’s net-IVV calculus a scale for outcomes . The result is a mixed view which accommodates tenets (ii) and (iii) above, but allows for (i) to fail in certain cases. I argue that, rather than being a defect, this allowance is an asset because our intuitions about ought-implies-can break down in cases where an agent is grossly misguided, and our theory should track these intuitions. (shrink)

We present a complete axiomatisation of the operator of projection onto state in the Duration Calculus relative to validity in DC without extending constructs. Projection onto state was introduced and studied extensively in our earlier works. We first establish the completeness of a system of axioms and proof rules for the operator relative to validity in the extension of DC by neighbourhood formulas, which express the neighbourhood values of boolean DC state expressions. By establishing a relatively complete axiomatisation for (...) the neighbourhood formulas in DC, we then achieve completeness of our system relative to basic DC. (shrink)

I offer a novel solution to Zeno’s paradox of The Arrow by introducing nilpotent infinitesimal lengths of time. Nilpotents are nonzero numbers that yield zero when multiplied by themselves a certain number of times. Zeno’s Arrow goes like this: during the present, a flying arrow is moving in virtue of its being in flight. However, if the present is a single point in time, then the arrow is frozen in place during that time. Therefore, the arrow is both moving and (...) at rest. In “Zeno’s Arrow, Divisible Infinitesimals, and Chrysippus,” White suggests using an infinitesimal value as the length of the present. Contra Zeno, this allows the arrow to be moving in the present, rather than frozen in place. In this paper, I follow the basic outline of White’s solution but argue that his solution suffers from arbitrariness and a related theoretical artificiality in relation to the system of infinitesimals he invokes, viz. in relation to the hyperreal infinitesimals of nonstandard analysis. After arguing that any solution to the paradox must satisfy certain theoretical requirements, I examine White’s solution alongside two nilpotent solutions. One of these solutions is inspired by F.W. Lawvere’s Smooth Infinitesimal Analysis and the other is inspired by Paolo Giordano’s ring of Fermat Reals. I argue that Giordano’s nilpotents supply the best answer to Zeno’s paradox. (shrink)

We study the linear Lindenbaum algebra of Basic Propositional Calculus, called linear basic algebra.

We study Basic algebra, the algebraic structure associated with basic propositional calculus, and some of its natural extensions. Among other things, we prove the amalgamation property for the class of Basic algebras, faithful Basic algebras and linear faithful Basic algebras. We also show that a faithful theory has the interpolation property if and only if its correspondence class of algebras has the amalgamation property.

In the present paper we give the first proof-theoretical example of an embedding of classical logic into a quantum-like logic. This is performed in the framework of basic logic, where a proof-theoretical approach to quantum logic is convenient. We consider basic orthologic, that corresponds to a sequential formulation of paraconsistent quantum logic, and which is given by basic orthologic added with weakening and contraction, in a language with Girard's negation. In the paper we first consider a convenient (...) cut-free calculus for classical logic, in the same language; then, in a language enriched with a new kind of literals, we introduce basic orthologic with a primitive modality, where classical logic is embeddable. Similarly to Girard's negation, our modality is not a connective but conceivable as an operator defined inductively on the set of formulae. This allows us to obtain a calculus which enjoys cut-elimination. (shrink)

In this research work, we formulate the phenomena of the financial system in the fractional framework to describe the complex nature of finance. The basic definitions and ideas of the Caputo-Fabrizio fractional operator are listed. We introduce a novel numerical technique for the dynamical behaviour of our fractional model. The oscillatory and chaotic behaviour of the model is studied with the variation of various input parameters on the model. We have shown that there exists strong oscillatory and chaotic behaviour (...) in the system; moreover, we highlighted the impact of fractional-order parameter on the model. The conditions for the local complex behaviour of the system are analyzed with the impact of certain parameters on the macroeconomic. Our findings suggest that the values of initial conditions, fractional order, and input parameters can lessen the chaos of the proposed financial system. (shrink)

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.

Pentus (1992) proves the equivalence of LCG's and CFG's, and CFG's are equivalent to BCG's by the Gaifman theorem (Bar-Hillel et al., 1960). This paper provides a procedure to extend any LCG to an equivalent BCG by affixing new types to the lexicon; a procedure of that kind was proposed as early, as Cohen (1967), but it was deficient (Buszkowski, 1985). We use a modification of Pentus' proof and a new proof of the Gaifman theorem on the basis of the (...) Lambek calculus. (shrink)

We present a geometrical analysis of the principles that lay at the basis of Categorial Grammar and of the Lambek Calculus. In Abrusci it is shown that the basic properties known as Residuation laws can be characterized in the framework of Cyclic Multiplicative Linear Logic, a purely non-commutative fragment of Linear Logic. We present a summary of this result and, pursuing this line of investigation, we analyze a well-known set of categorial grammar laws: Monotonicity, Application, Expansion, Type-raising, Composition, (...) Geach laws and Switching laws. (shrink)

Hypersequent calculus, developed by A. Avron, is one of the most interesting proof systems suitable for nonclassical logics. Although HC has rather simple form, it increases significantly the expressive power of standard sequent calculi. In particular, HC proved to be very useful in the field of proof theory of various nonclassical logics. It may seem surprising that it was not applied to temporal logics so far. In what follows, we discuss different approaches to formalization of logics of linear frames (...) and provide a cut-free HC formalization ofKt4.3, the minimal temporal logic of linear frames, and some of its extensions. The novelty of our approach is that hypersequents are defined not as finite sets but as finite lists of ordinary sequents. Such a solution allows both linearity of time flow, and symmetry of past and future, to be incorporated by means of six temporal rules. Extensions of the basic calculus with simple structural rules cover logics of serial and dense frames. Completeness is proved by Schütte/Hintikka-style argument using models built from saturated hypersequents. (shrink)

This article concerns the treatment of propositional quantification in a framework of labelled natural deduction for modal logic developed by Basin, Matthews and Viganò. We provide a detailed analysis of a basic calculus that can be used for a proof-theoretic rendering of minimal normal multimodal systems with quantification over stable domains of propositions. Furthermore, we consider variations of the basic calculus obtained via relational theories and domain theories allowing for quantification over possibly unstable domains of propositions. (...) The main result of the article is that fragments of the labelled calculi not exploiting reductio ad absurdum enjoy the Church–Rosser property and the strong normalization property; such result is obtained by combining Girard’s method of reducibility candidates and labelled languages of lambda calculus codifying the structure of modal proofs. (shrink)

This book seeks to offer original answers to all the major open questions in epistemology—as indicated by the book’s title. These questions and answers arise organically in the course of a validation of the entire corpus of human knowledge. The book explains how we know what we know, and how well we know it. The author presents a positive theory, motivated and directed at every step not by a need to reply to skeptics or subjectivists, but by the need of (...) a rational individual to know the world. -/- The author draws heavily from Ayn Rand’s theory of concepts as presented in her book, Introduction to Objectivist Epistemology, but departs from her epistemology—especially as explicated by leading exponents of her philosophy—in important ways. Areas of departure include the perception of entities and the role of probability theory in epistemology. -/- A main idea in the book is to begin the validation of the law of causality by identifying that existence causes our consciousness of it. Another key idea is this: The very fact that we perceive entities is the most basic and most extensive evidence that causal forces and causal interactions are regular. -/- Applying Ayn Rand’s principle that characteristics are ranges of measurement, the book offers a philosophical validation of “nonparametric predictive inference,” in turn providing an objective basis for prior probabilities in Bayesian analysis. -/- This book is primarily for a specialized readership—familiar with epistemological ideas and with Ayn Rand’s theory of concepts in particular. The last third of the book uses probability theory and mathematics somewhat beyond basic calculus, but less mathematical explanations are also included to make the general ideas accessible to lay readers. (shrink)

The lambda-calculus lies at the very foundation of computer science. Besides its historical role in computability theory it has had significant influence on programming language design and implementation, denotational semantics and domain theory. The book emphasizes the proof theory for the type-free lambda-calculus. The first six chapters concern this calculus and cover the basic theory, reduction, models, computability, and the relationship between the lambda-calculus and combinatory logic. Chapter 7 presents a variety of typed calculi; first (...) the simply typed lambda-calculus, then Milner-style polymorphism and, finally the polymporphic lambda-calculus. Chapter 8 concerns three variants of the type-free lambda-calculus that have recently appeared in the research literature: the lazy lambda-calculus, the concurrent y-calculus and the lamdba omega-calculus. The final chapter contains references and a guide to further reading. There are exercises throughout. In contrast to earlier books on these topics, which were written by logicians, the book is written from a computer science perspective and emphasizes the practical relevance of many of the key theoretical ideas. The book is intended as a course text for final year undergraduates or first year graduate students in computer science. Research students should find it a useful introduction to more specialist literature. (shrink)

We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.