Free ordered algebraic structures towards proof theory

Andreja Prijatelj

doi:10.2307/2695031

Free ordered algebraic structures towards proof theory

Journal of Symbolic Logic ◽

10.2307/2695031 ◽

2001 ◽

Vol 66 (2) ◽

pp. 597-608

Author(s):

Andreja Prijatelj

Keyword(s):

Classical Logic ◽

Proof Theory ◽

Algebraic Structures ◽

Ordered Algebras

AbstractIn this paper, constructions of free ordered algebras on one generator are given that correspond to some one-variable fragments of affine propositional classical logic and their extensions with n-contraction (n ≥ 2). Moreover, embeddings of the already known infinite free structures into the algebras introduced below are furnished with; thus, solving along the respective cardinality problems.

Download Full-text

Some Fixpoint Techniques in Algebraic Structures and Applications to Computer Science

Fundamenta Informaticae ◽

10.3233/fi-1987-10405 ◽

1987 ◽

Vol 10 (4) ◽

pp. 387-413

Author(s):

Irène Guessarian

Keyword(s):

Logic Programming ◽

Computer Science ◽

Proof Theory ◽

Algebraic Structures ◽

Data Bases

This paper recalls some fixpoint theorems in ordered algebraic structures and surveys some ways in which these theorems are applied in computer science. We describe via examples three main types of applications: in semantics and proof theory, in logic programming and in deductive data bases.

Download Full-text

Multiplicative conjunction and an algebraic meaning of contraction and weakening

Journal of Symbolic Logic ◽

10.2307/2586715 ◽

1998 ◽

Vol 63 (3) ◽

pp. 831-859 ◽

Cited By ~ 3

Author(s):

A. Avron

Keyword(s):

Classical Logic ◽

Linear Logic ◽

Substructural Logics ◽

Interesting Property ◽

Relevance Logic ◽

Proper Subset ◽

Algebraic Structures ◽

Elimination Rule ◽

First Case ◽

Soundness And Completeness

AbstractWe show that the elimination rule for the multiplicative (or intensional) conjunction Λ is admissible in many important multiplicative substructural logics. These include LLm (the multiplicative fragment of Linear Logic) and RMIm (the system obtained from LLm by adding the contraction axiom and its converse, the mingle axiom.) An exception is Rm (the intensional fragment of the relevance logic R, which is LLm together with the contraction axiom). Let SLLm and SRm be, respectively, the systems which are obtained from LLm and Rm by adding this rule as a new rule of inference. The set of theorems of SRm is a proper extension of that of Rm, but a proper subset of the set of theorems of RMIm. Hence it still has the variable-sharing property. SRm has also the interesting property that classical logic has a strong translation into it. We next introduce general algebraic structures, called strong multiplicative structures, and prove strong soundness and completeness of SLLm relative to them. We show that in the framework of these structures, the addition of the weakening axiom to SLLm corresponds to the condition that there will be exactly one designated element, while the addition of the contraction axiom corresponds to the condition that there will be exactly one nondesignated element (in the first case we get the system BCKm, in the second - the system SRm). Various other systems in which multiplicative conjunction functions as a true conjunction are studied, together with their algebraic counterparts.

Download Full-text

Logic and Philosophical Methodology

10.1093/oxfordhb/9780199668779.013.30 ◽

2016 ◽

Author(s):

John P. Burgess

Keyword(s):

Set Theory ◽

Model Theory ◽

Classical Logic ◽

Proof Theory ◽

Recursion Theory ◽

Theory Model ◽

Philosophical Methodology ◽

Paraconsistent Logics ◽

Philosophical Logic

This article explores the role of logic in philosophical methodology, as well as its application in philosophy. The discussion gives a roughly equal coverage to the seven branches of logic: elementary logic, set theory, model theory, recursion theory, proof theory, extraclassical logics, and anticlassical logics. Mathematical logic comprises set theory, model theory, recursion theory, and proof theory. Philosophical logic in the relevant sense is divided into the study of extensions of classical logic, such as modal or temporal or deontic or conditional logics, and the study of alternatives to classical logic, such as intuitionistic or quantum or partial or paraconsistent logics. The nonclassical consists of the extraclassical and the anticlassical, although the distinction is not clearcut.

Download Full-text

Intuitionism and the Sorites Paradox

10.1093/oso/9780199277339.003.0015 ◽

2021 ◽

pp. 393-422

Author(s):

Crispin Wright

Keyword(s):

Subject Matter ◽

Classical Logic ◽

Proof Theory ◽

Philosophy Of Mathematics ◽

Sorites Paradox ◽

Major Premise ◽

Stable Boundary

This chapter revisits and further develops all the principle themes and concepts of the preceding chapters. Epistemicism about vagueness postulates a realm of distinctions drawn by basic vague concepts that transcend our capacity to know them. Its treatment of their subject matter is thus broadly comparable to the Platonist philosophy of mathematics. An intuitionist philosophy of vagueness, as do many philosophies of the semantics and metaphysics of vague expressions, finds this idea merely superstitious and rejects it. The vagueness-intuitionist, however, credits the epistemicist with a crucial insight: that vagueness is indeed a cognitive, rather than a semantic, phenomenon—something that is not a consequence of some kind of indeterminacy, or open-endedness in the semantics of vague expressions but rather resides in our brute inability to bring, for example, yellow and orange right up against one another, so to speak, so as to mark a sharp and stable boundary. A solution to the Sorites paradox is developed that is consonant with this basic idea but, by motivating a background logic that observes (broadly) intuitionistic restrictions on the proof theory for negation, allows us to treat the paradoxical reasoning as a simple reductio of its major premise, without the unwelcome implication, sustained by classical logic, of sharp cut-offs.

Download Full-text

The finite embeddability property for noncommutative knotted extensions of RL

International Journal of Algebra and Computation ◽

10.1142/s0218196715500010 ◽

2015 ◽

Vol 25 (03) ◽

pp. 349-379 ◽

Cited By ~ 1

Author(s):

R. Cardona ◽

N. Galatos

Keyword(s):

Classical Logic ◽

Proof Theory ◽

Mathematical Linguistics ◽

Residuated Lattices ◽

Automata Theory ◽

Finite Model ◽

Algebraic Proof ◽

Model Property ◽

Finite Model Property ◽

Finite Embeddability Property

The finite embeddability property (FEP) for knotted extensions of residuated lattices holds under the assumption of commutativity, but fails in the general case. We identify weaker forms of the commutativity identity which ensure that the FEP holds. The results have applications outside of order algebra to non-classical logic, establishing the strong finite model property (SFMP) and the decidability for deductions, as well as to mathematical linguistics and automata theory, providing new conditions for recognizability of languages. Our proofs make use of residuated frames, developed in the context of algebraic proof theory.

Download Full-text

Identity of Proofs Based on Normalization and Generality

Bulletin of Symbolic Logic ◽

10.2178/bsl/1067620091 ◽

2003 ◽

Vol 9 (4) ◽

pp. 477-503 ◽

Cited By ~ 19

Author(s):

Kosta Došen

Keyword(s):

Equivalence Relation ◽

Category Theory ◽

Classical Logic ◽

Proof Theory ◽

Natural Deduction ◽

Lambda Calculus ◽

Free Form ◽

Low Dimensional Topology ◽

Sequent Systems ◽

Low Dimensional

AbstractSome thirty years ago, two proposals were made concerning criteria for identity of proofs. Prawitz proposed to analyze identity of proofs in terms of the equivalence relation based on reduction to normal formin natural deduction. Lambek worked on a normalization proposal analogous to Prawitz's, based on reduction to cut-free form in sequent systems, but he also suggested understanding identity of proofs in terms of an equivalence relation based on generality, two derivations having the same generality if after generalizing maximally the rules involved in them they yield the same premises and conclusions up to a renaming of variables. These two proposals proved to be extensionally equivalent only for limited fragments of logic.The normalization proposal stands behind very successful applications of the typed lambda calculus and of category theory in the proof theory of intuitionistic logic. In classical logic, however, it did not fare well.The generality proposal was rather neglected in logic, though related matters were much studied in pure category theory in connection with coherence problems, and there are also links to low-dimensional topology and linear algebra. This proposal seems more promising than the other one for the general proof theory of classical logic.

Download Full-text