Algebraic semantics for the ‐fragment of and its properties

We study the variety of equivalential algebras with zero and its subquasivariety that gives the equivalent algebraic semantics for the ‐fragment of intuitionistic propositional logic. We prove that this fragment is hereditarily structurally complete. Moreover, we effectively construct the finitely generated free equivalential algebras with zero.     

A note on the independence of premiss rule

In this note, we prove that certain theories of (many‐sorted) intuitionistic predicate logic are closed under the independence of premiss rule (IPR). As corollaries, we show that and extended by some non‐classical axioms and non‐constructive axioms are closed under IPR.     

Singly generated quasivarieties and residuated structures

A quasivariety $\mathsf{K}$ of algebras has the joint embedding property (JEP) if and only if it is generated by a single algebra A . It is structurally complete if and only if the free ℵ₀-generated algebra in $\mathsf{K}$ can serve as A . A consequence of this demand, called ‘passive structural completeness’ (PSC), is that the nontrivial members of $\mathsf{K}$ all satisfy the same existential positive sentences. We prove that if $\mathsf{K}$ is PSC then it still has the JEP, and if it has the JEP and its nontrivial members lack trivial subalgebras, then its relatively simple members all belong to the universal class generated by one of them. Under these conditions, if $\mathsf{K}$ is relatively semisimple then it is generated by one $\mathsf{K}$-simple algebra. We also prove that a quasivariety of finite type, with a finite nontrivial member, is PSC if and only if its nontrivial members have a common retract. The theory is then applied to the variety of De Morgan monoids, where we isolate the sub(quasi)varieties that are PSC and those that have the JEP, while throwing fresh light on those that are structurally complete. The results illuminate the extension lattices of intuitionistic and relevance logics.     

Paraconsistent double negation as a modal operator

A paraconsistent modal‐like logic, , is defined as a Gentzen‐type sequent calculus. The modal operator in the modal logic can be simulated by the paraconsistent double negation in . Some theorems for embedding into a Gentzen‐type sequent calculus for and vice versa are proved. The cut‐elimination and completeness theorems for are also proved.     

The eal truth

We study a real valued propositional logic with unbounded positive and negative truth values that we call ‐valued logic. Such a logic is semantically equivalent to continuous propositional logic, with a different choice of connectives. After presenting the deduction machinery and the semantics of ‐valued logic, we prove a completeness theorem for finite theories. Then we define unital and Archimedean theories, in accordance with the theory of Riesz spaces. In the unital setting, we prove the equivalence of consistency and satisfiability and an approximated completeness theorem similar to the one that holds for continuous propositional logic. Eventually, among unital theories, we characterize Archimedean theories as those for which strong completeness holds. We also point out that ‐valued logic provides alternative calculi for ?ukasiewicz logic and for propositional continuous logic.     

On the definition and the representability of quasi‐polyadic equality algebras

We show that the usual axiom system of quasi polyadic equality algebras is strongly redundant. Then, so called non‐commutative quasi‐polyadic equality algebras are introduced (), in which, among others, the commutativity of cylindrifications is dropped. As is known, quasi‐polyadic equality algebras are not representable in the classical sense, but we prove that algebras in are representable by quasi‐polyadic relativized set algebras, or more exactly by algebras in .     

The simplest protoalgebraic logic

The logic is the sentential logic defined in the language with just implication → by the axiom of reflexivity or identity “” and the rule of Modus Ponens “from φ and to infer ψ”. The theorems of this logic are exactly all formulas of the form . We argue that this is the simplest protoalgebraic logic, and that in it every set of assumptions encodes in itself not only all its consequences but also their proofs. In this paper we study this logic from the point of view of abstract algebraic logic, and in particular we use it as a relatively natural counterexample to settle some open problems in this theory. It appears that this logic has almost no properties: it is neither equivalential nor weakly algebraizable; it does not have an algebraic semantics; it does not satisfy any form of the Deduction Theorem, other than the most general parameterized and local one that all protoalgebraic logics satisfy; it is not filter‐distributive; and so on. It satisfies some forms of the interpolation property but in a rather trivial way. Very few things are known about its algebraic counterpart, save that its intrinsic variety is the class of all algebras of the similarity type.     

An alternative Gentzenisation of

In this paper, we give a sequent calculus for the positive contraction‐less relevant logic and we give a proof that it is cut‐free without the use of the truth constant t. Based on , we re‐prove the decidability of the logic .     

Classical provability of uniform versions and intuitionistic provability

Along the line of Hirst‐Mummert 9 and Dorais 4 , we analyze the relationship between the classical provability of uniform versions Uni(S) of Π₂‐statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π₂‐statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi‐intuitionistic systems including bar induction in all finite types but also nonconstructive principles such as K?nig's lemma and uniform weak K?nig's lemma . Our result is applicable to many mathematical principles whose sequential versions imply .     

On notions of representability for cylindric‐polyadic algebras,and a solution to the finitizability problem for quantifier logics with equality

We consider countable so‐called rich subsemigroups of ; each such semigroup T gives a variety CPEA_T that is axiomatizable by a finite schema of equations taken in a countable subsignature of that of ω‐dimensional cylindric‐polyadic algebras with equality where substitutions are restricted to maps in T. It is shown that for any such T, if and only if is representable as a concrete set algebra of ω‐ary relations. The operations in the signature are set‐theoretically interpreted like in polyadic equality set algebras, but such operations are relativized to a union of cartesian spaces that are not necessarily disjoint. This is a form of guarding semantics. We show that CPEA_T is canonical and atom‐canonical. Imposing an extra condition on T, we prove that atomic algebras in CPEA_T are completely representable and that CPEA_T has the super amalgamation property. If T is rich and finitely represented, it is shown that CPEA_T is term definitionally equivalent to a finitely axiomatizable Sahlqvist variety. Such semigroups exist. This can be regarded as a solution to the central finitizability problem in algebraic logic for first order logic with equality if we do not insist on full fledged commutativity of quantifiers. The finite dimensional case is approached from the view point of guarded and clique guarded (relativized) semantics of fragments of first order logic using finitely many variables. Both positive and negative results are presented.     

A decidable paraconsistent relevant logic: Gentzen system and Routley‐Meyer semantics

In this paper, the positive fragment of the logic of contraction‐less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four‐valued logic . This extended relevant logic is called , and it has the property of constructible falsity which is known to be a characteristic property of . A Gentzen‐type sequent calculus for is introduced, and the cut‐elimination and decidability theorems for are proved. Two extended Routley‐Meyer semantics are introduced for , and the completeness theorems with respect to these semantics are proved.     

Concrete barriers to quantifier elimination in finite dimensional C*‐algebras

Work of Eagle, Farah, Goldbring, Kirchberg, and Vignati shows that the only separable C*‐algebras that admit quantifier elimination in continuous logic are $\mathbb{C}$, ${\mathbb{C}}^2$, $M_2(\mathbb{C})$, and the continuous functions on the Cantor set. We show that, among finite dimensional C*‐algebras, quantifier elimination does hold if the language is expanded to include two new predicate symbols: One for minimal projections, and one for pairs of unitarily conjugate elements. Both of these predicates are definable, but not quantifier‐free definable, in the usual language of C*‐algebras. We also show that adding just the predicate for minimal projections is sufficient in the case of full matrix algebras, but that in general both new predicate symbols are required.     

Embedding classical in minimal implicational logic

Consider the problem which set V of propositional variables suffices for whenever , where , and ?_c and ?_i denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula . It is an easy consequence of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving ⊥, which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary.     

Incomparable ω1‐like models of set theory

We show that the analogues of the embedding theorems of [3], proved for the countable models of set theory, do not hold when extended to the uncountable realm of ω₁‐like models of set theory. Specifically, under the ⋄ hypothesis and suitable consistency assumptions, we show that there is a family of many ω₁‐like models of , all with the same ordinals, that are pairwise incomparable under embeddability; there can be a transitive ω₁‐like model of that does not embed into its own constructible universe; and there can be an ω₁‐like model of whose structure of hereditarily finite sets is not universal for the ω₁‐like models of set theory.     

Clubs on quasi measurable cardinals

We construct a model satisfying “κ is quasi measurable”. Here, we call κ quasi measurable if there is an ℵ₁‐saturated κ‐additive ideal on κ. We also show that, in this model, forcing with adds one but not κ Cohen reals. We introduce a weak club principle and use it to show that, consistently, for some ℵ₁‐saturated κ‐additive ideal on κ, forcing with adds one but not κ random reals.     

A model of intuitionistic analysis in which ‐definable discrete sets are subcountable

There is a model, for a system of intuitionistic analysis including Brouwer's principle for numbers and Kripke's schema, in which ‐definable discrete sets of choice sequences are subcountable.     

Neutrally expandable models of arithmetic

A subset of a model of is called neutral if it does not change the relation. A model with undefinable neutral classes is called neutrally expandable. We study the existence and non‐existence of neutral sets in various models of . We show that cofinal extensions of prime models are neutrally expandable, and ω₁‐like neutrally expandable models exist, while no recursively saturated model is neutrally expandable. We also show that neutrality is not a first‐order property. In the last section, we study a local version of neutral expandability.     

Peano Corto and Peano Basso: A Study of Local Induction in the Context of Weak Theories

In this paper we study local induction w.r.t. Σ₁‐formulas over the weak arithmetic . The local induction scheme, which was introduced in 7 , says roughly this: for any virtual class that is progressive, i.e., is closed under zero and successor, and for any non‐empty virtual class that is definable by a Σ₁‐formula without parameters, the intersection of and is non‐empty. In other words, we have, for all Σ₁‐sentences S, that S implies , whenever is progressive. Since, in the weak context, we have (at least) two definitions of Σ₁, we obtain two minimal theories of local induction w.r.t. Σ₁‐formulas, which we call Peano Corto and Peano Basso. In the paper we give careful definitions of Peano Corto and Peano Basso. We establish their naturalness both by giving a model theoretic characterization and by providing an equivalent formulation in terms of a sentential reflection scheme. The theories Peano Corto and Peano Basso occupy a salient place among the sequential theories on the boundary between weak and strong theories. They bring together a powerful collection of principles that is locally interpretable in . Moreover, they have an important role as examples of various phenomena in the metamathematics of arithmetical (and, more generally, sequential) theories. We illustrate this by studying their behavior w.r.t. interpretability, model interpretability and local interpretability. In many ways the theories are more like Peano arithmetic or Zermelo Fraenkel set theory, than like finitely axiomatized theories as Elementary Arithmetic, and . On the one hand, Peano Corto and Peano Basso are very weak: they are locally cut‐interpretable in . On the other hand, they behave as if they were strong: they are not contained in any consistent finitely axiomatized arithmetical theory, however strong. Moreover, they extend , the theory of parameter‐free Π₁‐induction.     

Algebraic functions in quasiprimal algebras

A function is algebraic on an algebra if it can be implicitly defined by a system of equations on . In this note we give a semantic characterization for algebraic functions on quasiprimal algebras. This characterization is applied to obtain necessary and sufficient conditions for a quasiprimal algebra to have every one of its algebraic functions be a term function. We also apply our results to particular algebras such as finite fields and monadic algebras.