ABSTRACT. In the first half of my talk, I will introduce five "unorthodox" algebras, four of which have 3-element chain as a lattice-reduct and the fifth one has a 4-element Boolean lattice as a lattice-reduct. These algebras are anti-Boolean and yet have some amazing similarities with Boolean algebras. I develop an algebraic theory of these algebras that leads to an equational axiomatization of the variety UNO1 generated by the five unorthodox algebras. I, then, look at the structure of the lattice of subvarieties of the variety UNO1 and provide bases for all 32 subvarieties of UNO1. I also indicate why these algebras collectively generate a discriminator variety and individually are primal algebras. In the second half, I will introduce an algebraizable logic (in the sense of Blok and Pigozzi) called "UNO1" whose equivalent algebraic semantics is the variety UNO1. Here I rely on the well-known results of Rasiowa on implicative logics and of Blok and Pigozzi on algebraizability. I will then present axiomatizations for all the axiomatic extensions of UNO1 and discuss decidability of these logics.

References

[1] H.P. Sankappanavar, Semi-De Morgan algebras, J. Symbolic. Logic, 52 (1987), pp. 712–724.

[2] H.P. Sankappanavar, Semi-Heyting algebras: An abstraction from Heyting algebras. In: Proceedings of the 9th “Dr. Antonio A. R. Monteiro” Congress (Spanish: Actas del IX Congresso Dr. Antonio A. R. Monteiro, held in Bahá Blanca, May 30-June 1, 2007), edited by M. Abadand I. Viglizzo (Universidad Nacional del Sur), 2008, pp. 33–66.

[3] H.P. Sankappanavar, Expansions of Semi-Heyting algebras I: Discriminator varieties, Studia Logica, 98, no.1-2, (2011), pp. 27–81.

[4] H.P. Sankappanavar, Dually quasi-De Morgan Stone semi-Heyting algebras I. Regularity, Categories, General Algebraic Structures and Applications, 2, no. 1, (2014), pp. 47–64

[5] J. M. Cornejo and H.P. Sankappanavar, A logic for dually hemimorphic semi-Heyting algebras and its axiomatic expansions, Bulletin of the Section of Logic, 51 (2022), pp. 555–645.

ABSTRACT. In the 1669 manuscript De Analysi, Newton derives three theorems, now cornerstones of modern calculus: the power series for arcsine, the power series for sine, and the area under the curve y(x)=x^m/n=n/m+n∙x^m+n/n (Rule I). He also sets the rule stating the area under finitely or infinitely many curves equals the sum of areas under each curve (Rule II) and shows how to expand into a power series then-standard functions such as a²/b+x or √(a²+x²) based on some algebraic laws (Rule III).

Generally, Newton's approach in Rule I hinges on an odd procedure of summing up infinitesimal area moments; for the series of arcsine, he combines Rule II applied to infinitesimal arc moments with the same peculiar sum operation, dealing with area and arc moments, he employs the concept of the infinitely small unit segment (indivisible); deriving the sine series, he adopts an approach other than Rules I to III.

Specifically, proving Rule I, Newton shows that if z(x)= n/m+n∙x^m+n/n is a function of an area under a curve, then the curve is y(x)=x^m/n. At the end, he writes ``Conversely therefore if a∙x^m/n=y, then will be (n/m+n)∙a∙x^m+n/n=z."

We interpret Newton's Rule I with techniques of nonstandard analysis and represent his arguments on a hyperfinite grid, essentially a discrete domain instead of a continuous one. Bridging the gap between finite and infinite, we mimic Newton's approach, define the area under a curve as a hyperfinite sum, and prove the unproved part of Rule I using 17th-century techniques.

References

[1] Błaszczyk, P., Petiurenko, A.: Euler's Series for Sine and Cosine. An Interpretation in Nonstandard Analysis. In: Waszek, D., Zack, M. (eds.), Annals of the CSHPM, Birkhauser 2023, 73--102.

[2] Newton, I.: The `De Analysis per Aequationes Infinitas'. On analysis by infinite equations. In: Whiteside, D. T. (ed): The Mathematical Papers of Isaac Newton. Vol II. 1667--1670. Cambridge Univ. Press, Cambridge 1968, 206--247.

ABSTRACT. This paper bridges the classical and modern approaches to Thales' theorem. We start with commensurable lines and then introduce the general version. While the commensurable version relies on elementary techniques, the general one requires the arithmetic of line segments or real numbers. We reference Euclid's proof of Thales' theorem (Elements, VI.2) and consider its implications for automatic theorem proving.

Thales' theorem, also known as the intercept or fundamental theorem of proportionality, is a crucial topic that distinguishes Euclid's methodology from modern axiomatic systems. In the Elements, it is a part of Book VI and builds on proportion developed in Book V ­- a technique replaced in the 20th century by the arithmetic of real numbers (Błaszczyk 2021). Its proof relies on proposition VI.1 and refers to the definition of proportion (V.def.5). Euclidean proportion relates pairs of figures of the same kind, such as line segments, triangles, and angles. At the same time, modern systems define proportion only for line segments.

We review the proofs of Thales' theorem throughout the 20th-century geometric systems, significantly those developed by Hilbert (1899), Hartshorne (2000), Birkhoff (1932), Millman & Parker (1991), Borsuk & Szmielew (1960), and Schwabhäuser, Szmielew & Tarski (1983). These systems highlight the challenge of proving Thales' theorem, with two main strategies identified: segment arithmetic (Hilbert, Hartshorne, Schwabhäuser, Szmielew, Tarski) and the implementation of real numbers into geometric systems (Borsuk & Szmielew, Millman & Parker). The latter includes either axioms guaranteeing the existence of a bijection between real numbers and a straight line (Birkhoff) or deriving this bijection from Hilbert-style axioms (Borsuk & Szmielew). We examine proofs using segment arithmetic and discuss Borsuk and Szmielew's measure theorem and Millman and Parker's proof. Additionally, we consider Birkhoff's axiom on the relationship between real numbers and a straight line.

Modern systems that bypass Euclid's proof of Thales' theorem introduce real numbers or segment arithmetic, resulting in complex proofs. Euclid's proof is straightforward but uses techniques abandoned by modern mathematics. We propose an intermediary solution: an axiomatic theory, making proposition VI.1 an axiom, enabling the recovery of the original proof. We present an approach to Thales' theorem based on the axioms of the area method and automatic theorem proving in the GCLC system developed by Chou, Gao, Zhang (1994) and Janicic, Narboux, Quaresma (2012).

References

[1] Birkhoff, G. D.: A Set of Postulates for Plane Geometry (Based on Scale and Protractors), Annals of Mathematics, 33(2), 329–345, 1932.

[2] Błaszczyk, P.: Descartes' Transformation of Greek Notion of Proportionality. In B. Sriraman (ed.) Handbook of the History and Philosophy of Mathematical Practice. Springer, Cham, 2021; https://link.springer.com/referenceworkentry/10.1007/ 978-3-030-19071-2_16-1

[3] Borsuk, K., Szmielew, W.: Foundations of Geometry, North-Holland, Amsterdam 1960.

[4] Hartshorne, R.: Geometry: Euclid and Beyond. Springer, New York 2000.

[5] Chou, S., Gao, X., Zhang, J.: Machine Proofs in Geometry, World Scientific, Singapore 1994.

[6] Hilbert, D.: Grundlagen der Geometrie. Festschrift zur Feier der Enthüllung des Gauss-Weber-Denkmals in Göttingen. Teubner, Leipzig 1899, 1–92. In: K. Volkert (Hrsg.), David Hilbert, Grundlagen der Geometrie (Festschrift 1899), Springer, Berlin 2015.

[7] Janičić, P., Narboux, J., Quaresma, P.: The area method: a recapitulation, Journal of Automated Reasoning, Springer Verlag 48(4), 489–532, 2012.

[8] Millman, R., Parker, G.: Geometry A Metric Approach with Models, Springer, Berlin 1991.

[9] Schwabhäuser, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie, Springer, Berlin 1983.

ABSTRACT. In the philosophical literature on the foundations of logic, various principles of classical logic have been questioned and weaker systems have been proposed. In paraconsistent logics, the law of explosion fails: a theory may contain a sentence together with its negation without exploding into triviality. In intuitionistic logic, the law of excluded middle fails: it may be that a sentence does not hold, but neither does its negation. As noted by Tedder and Shapiro, these two non-classical systems correspond to largely disjoint areas of research.

We aim to contribute to bridging this gap by introducing a paraconsistent intuitionistic logic, in which both laws fail. Building on the bachelor's thesis under supervision of Robert Passmann, we take as a starting point Priest's paraconsistent logic propositional logic of paradox (LP) and combine it with the Kripke semantics for intuitionistic logic. The result is a natural extension of both logics, which we call intuitionistic logic of paradox (ILP). We introduce two versions of this logic; one that obeys modus ponens, and one that does not (remaining faithful to LP).

Whenever a logic is weakened, this raises the question of recapture: can the original logic be recovered from its weakening by adding certain assumptions? We raise this question for ILP with respect to LP and intuitionistic logic. By its very definition, ILP allows for a primitive kind of recapture of both these logics: restricting the consequence relation to a certain class of models allows us to recover the consequence relation of LP or intuitionistic logic.

However, such recapture is not necessarily expressible within the logic. We might hope for something stronger -- in particular, we ask the question: does ILP stand to LP as intuitionistic logic stands to classical logic? Classical logic can be recovered from intuitionistic logic by adding the law of excluded middle; do we obtain LP when we strengthen ILP by adding this law? The question turns out not to be straightforward, and its answer depends on the formulation of the law of excluded middle -- intuitionistically equivalent formulations are no longer equivalent in ILP -- and on the version of ILP that is used.

ABSTRACT. We introduce a natural deduction system with a general collapse rule for intuitionistic propositional logic. The general collapse rule is a generalization of the collapse rule that replaces the falsity rule also known as the ex falso quodlibet rule. We provide a computational variant of the system in the style of the Curry-Howard correspondence and show that it is strongly normalizing.

ABSTRACT. The logic IK is the intuitionistic variant of normal modal logic K, introduced by Fischer Servi , Plotkin and Stirling , and studied by Simpson . This logic is considered a fundamental intuitionstic modal system as it corresponds, modulo the standard translation, to a fragment of intuitionstic first-order logic. The language of is generated from constants ⊤, ⊥ and a set At of propositional variables and by means of the operators ∧, ∨, ⊃, □ and ◇. The semantics of IK is defined in terms of bi-relational models, consisting of a pre-order relation ≤ from intuitionistic models and a binary relation R corresponding to the accessibility relation of modal Kripke frames. Bi-relational models additionally satisfy the frame conditions of forward and backward confluence, governing the interaction between the two relations.

Various proof systems for IK have been proposed in the literature, among which nested and labelledsequent calculi [2,3,6]. We introduce an innovative labelled-free bi-nested sequent calculus for IK, whichis called C_IK. This proof system comprises two kinds of nesting structures: ⟨·⟩, corresponding to thepre-order relation of bi-relational models for IK, and [·], corresponding to the accessibility relation. Theframe conditions of bi-relational models are modularly captured in the proof system by the ‘interactionrules’, (inter_fc) and (inter_bc), operating on the two nestings.

Theorem 1 (Soundness). If a sequent is provable in C_IK, then it is valid.

Then we introduce a decision algorithm for IK, that is, an algorithm that for any formula decideswhether it is valid or not. The algorithm implements a terminating proof search strategy in a cumulativeand set-based version of C_IK which is called CC_IK.

Proposition 2. Let S be a sequent. S is provable in CIK if and only if it is provable in CC_IK.

Theorem 3 (Termination). Let A be a formula. Proof-search for the sequent ⇒ A terminates and ityields either a proof of A or a finite derivation where all the non-axiomatic leaves are global-saturated.

Next, we show that C_IK allows for direct counter-model extraction: from a single failed derivation,it is possible to construct a finite countermodel for the formula at the root. This can be seen as themain advantage of our calculus over other labelled-free calculi. In order to extract a model from aglobal-saturated sequent, however, we need to additionally keep track of specific components occurringin set-based sequents. To this aim, we shall define an annotated version of CC_IK, called CC_IKⁿ, whichoperates on sequents whose components are decorated by natural numbers, the annotations, and areequipped with an additional structure to keep in memory a binary relation on such annotations.The finite countermodel extraction from failed proof search entails completeness.

Theorem 4 (Completeness). If A is valid in IK, it is provable in CC_IKⁿ, and thus in CC_IK.Lastly, we compare C_IK with a fully labelled sequent calculus labIK_≤ (cf. [2]). We simulate anyderivation (rooted by a formula) in labIK_≤ into one in C_IK. The whole procedure is divided into threesteps, (i) llabIK_≤ to CC_IKⁿ; (ii) CC_IKⁿ to CC_IK; and lastly (iii) CC_IK to C_IK. Steps (ii) and (iii) aretrivial; for (i) we prove the following result:

Proposition 5. For each formula, a derivation in labIK_≤ can be simulated by one in CC_IK.

References

[1] Gisèle Fischer Servi. Axiomatizations for some intuitionistic modal logics. Rendiconti del SeminarioMatematico Università e Politecnico di Torino, 42, 1984.

[2] Sonia Marin, Marianela Morales, and Lutz Straßburger. A fully labelled proof system for intuitionisticmodal logics. J. Log. Comput., 31(3):998–1022, 2021.

[3] Sonia Marin and Lutz Straßburger. Label-free modular systems for classical and intuitionistic modallogics. In Advances in Modal Logic 10, 2014.

[4] Gordon Plotkin and Colin Stirling. A framework for intuitionistic modal logics. In Proceedings of the1st Conference on Theoretical Aspects of Reasoning about Knowledge (TARK), pages 399–406, 1986.

[5] Alex K. Simpson. The proof theory and semantics of intuitionistic modal logic. 1994.

[6] Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Foundationsof Software Science and Computation Structures, pages 209–224. Springer, 2013.

ABSTRACT. In this paper, we analyse the effects of the principle of explosion (PE) and inference rules related to PE within the context of subminimal logics which were introduced by Dimiter Vakarelov [1]. Since we have two backgrounds, we will first describe the backgrounds, and then clarify the aims of the paper.

References

[1] Dimiter Vakarelov (2005): Nelson’s negation on the base of weaker versions of intuitionistic negation. Studia Logica 80, pp. 393–430, doi:10.1007/s11225-005-8476-5.

ABSTRACT. This talk explores global proof transformations within sequent and hypersequent calculi. These transformations result in:

(a) restricting cuts to analytic cuts,

(b) replacing hypersequent structures with bounded cuts, and

(c) eliminating the density rule from hypersequent calculi (thus determining whether a given logic qualifies as a fuzzy logic).

ABSTRACT. We observe in Mathematics statements formulated with respect to a small domain of discourse, but using notions only available in a proper extensions. Paradigmatic example for such weak extensions is the statement that the sum of the first n natural numbers can be given in terms of fractions (belonging to the rationals). We propose a positive free logic, the logic of virtual extensions, capable of representing adequately this phenomenon. The grammar of this logic permits virtual function symbols (for non-denoting terms), the calculus is a variation of Natural Deduction and the semantics is given in terms of term structures in which equality is evaluated by a suitable congruence relation. Besides being capable of representing weak extensions, this logic seems suitable to provide a formal underpinning to philosophical stances, where the real existence of newly introduced objects (as the square root of -1) was doubted.

ABSTRACT. Normalisation theorems establish that certain detours, to use Gentzen's phrase, in proofs in systems of natural deduction are unnecessary and can be removed by reduction procedures. This is familiar for intuitionist logic from Prawitz's work. The present talk focuses on issues arising from adapting Prawitz's methods to negative free logic with the iota operator for definite descriptions. The system to be considered was formulated by Tennant. A number of new cases of maximal segments and formulas arise and to treat the iota operator requires modifying the system following an insight of Indrzejczak's.

ABSTRACT. In [1] we presented families of probability logics suitable for reasoning about quantum observations on the spaces with fnite dimension. Since quantum sys- tems are often associated by infnite dimensional Hilbert spaces, we have ex- tended this approach and we developed the logic QLPinf , so that we can con- sider measurements on infnite dimensional spaces as well. The basic "quantum logic statement" we are considering is:"By measuring some observable, let's say O, we obtained its eigenvalue a". In order to express it we use modal formulas of the form ◻♢α. Using modal formula ◻♢α instead of propositional formula α was introduced to distinguish the concepts: "Something is true" (which we de- note by α) and "Something is oberved to be true, i.e., it is measured" (denoted by ).◻♢α Applying this approach and relying on the fact that ◻ does not dis- tribute over ∨, we do not need non-distributive structures (like non-distributive lattices with numerous axioms and rules which are normally used in quantum logics). In [1] we gave an example and a detailed discussion of overcoming non- distributivity in this way. In quantum mechanics complex numbers are used for representation of waves. Thus the square of the modulus of complex numbers represents the probability of measuring certain values. Since the feld of complex numbers is uncountable, in our semantics we use complex numbers with rational coordinates, i.e., numbers of the form z = a + ib where a,bϵ Q. The set of formulas consists of modal formulas and probability formulas. Basic probability formula is a formula of the form CSz1;r1z2;r2;...zj;rj ...◻♢α and we can explain its meaning in the following way: • Suppose that we have an observable O with infnitary many eigenvalues a1, a2,...

• Let w1;1;w1;2; : : : be eigenvectors that correspond to a1 and assume that w is arbitrary vector and c11, c12, ... are coefcients in linear repre- sentation of w in the system w11,1;w12,... • Suppose that ◻♢α means: "By measuring O we obtained a1. Then CSz11,r11;z12,2;r12...;z1j,r1j... ◻♢α means that z11, z12, ...approximate c11, c12, ... in such way that ǁz1i-c1iǁ ≤r1i where iǁs a complex norm. Formulas are interpreted in re exive and symmetric Kripke models equipped with probability distributions over families of subsets of possible worlds that are orthocomplemented lattices. We give infnitary axiomatizations, prove the corresponding soundness and strong completeness theorems, and also decid- ability. In order to prove completeness, as expected, we proved Lindenbaum's theorem where we provided that in every maximal consistent set T, for ev- ery formula ◻♢α and every kϵN there is a sequence zk1,zk2 such that CSzk1,1/k;zk2,1/k...◻♢α ϵ T Then in the canonical model every world w is a maxi- mal consistent set and μ(w,◻♢α) = (lim k→ꚙ zk1; lim k→ꚙ zk2...) = (c1; c2; ...) where (c1; c2; : : :) are required coecients in linear representation of w. Finally, we mention that there is a signifcant diference in axiomatization (and thus in the parts that lead to proving the completeness theorem) between logics in [1] and the logic QLPinf , in the sense that the rules of logic QLPinf represent a signicantly greater challenge.

References

[1] Ilić Stepić, A. and Ognjanović, Z. and Perović, A. Probability Logics for Reasoning About QuantumObservations Logica Universalis, 17(2):175-219 (2023)

ABSTRACT. It is well-known that ZF, the most widely used foundation for mathematics, has two pathological features, which Von Neumann and Zermelo himself were not happy with: (i) ZF has infinitely many axioms; (ii) if ZF has a model, it has a countable model. It is also well-known, in fact proven, that this cannot be fixed in the framework of classical first-order logic.

In [1], a finitely axiomatized nonclassical theory T of sets and functions, which incorporates category theory and axiomatic set theory, has been introduced as the collection of axioms one has to accept to get rid of the features (i) and (ii). The theory T consists of some twenty axioms that can be reformulated as simple theorems of ZF, plus one nonclassical axiom, which is called the 'sum function axiom': this sum function axiom is a new mathematical principle, which is so powerful that it allows the derivation of the infinite schemes of separation and replacement of ZF from T—with the help of nonclassical rules of inference, that is. Due to the definition of validity of nonclassical formulas in a model M of T, the downward Loewenheim-Skolem theorem does not hold; consequently, if T has a model, it doesn't have a countable model. And just now it has been proven that T is relatively consistent with ZF, demonstrating that T is an advancement in the foundations of mathematics [2]. Of course one may doubt that nonclassical mathematics will ever become mainstream in everyday mathematical practice, but the thing here is that the sum function axiom can stay in the background: for everyday mathematical practice it suffices to use the standard first-order theorems of T.

The purpose of this talk is to give a general overview of this research program. An attempt will be made to explain the nonclassical sum function axiom to the audience in the available time slot, using Venn diagrams.

References

[1] M.J.T.F. Cabbolet, "A Finitely Axiomatized Non-Classical First-Order Theory Incorporating Category Theory and Axiomatic Set Theory", Axioms 10(2), 119 (2021)

[2] M.J.T.F. Cabbolet, "Relative consistency of a finite non-classical theory incorporating ZF and category theory with ZF", in preparation (2024)

ABSTRACT. Two Gentzen-style twist sequent calculi for normal modal logic S4 are introduced and investigated. The proposed calculi, which do not employ standard logical inference rules for the negation connective, are characterized by several twist logical inference rules for negated logical connectives. Short proofs for provable negated modal formulas containing numerous negation connectives can be generated by these calculi. The cut-elimination theorems for the calculi are proved, and the subformula properties for the calculi are also obtained.

ABSTRACT. The cut-elimination procedure for the provability logic is known to be problematic: A Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby complicating the proof of termination. In this paper, we present a syntactic cut-elimination proof based on nested sequents, a generalization of sequents that allows a sequent to contain other sequents as single elements. A similar calculi was developed by Poggiolesi (2009), but there are certain ambiguities in the proof. By adopting the idea of Kushida (2020) into nested sequents, our proof does not require an extra measure on cuts or error-prone, intricate rewriting on derivations, but only straightforward inductions, thus leading to less ambiguity and confusion.

ABSTRACT. This work studies the proof theory of left (right) skew monoidal closed categories and skew bi-closed categories with concepts and methods from non-associative Lambek calculus. Skew monoidal closed categories represent a relaxed version of monoidal closed categories, where the structural laws are not invertible; instead, they are natural transformations with a specific orientation. Uustalu et al. used sequents with stoup to syntactically model left skew monoidal closed categories, yielding results regarding proof identities and categorical coherence. However, their syntax does not work well when modeling right skew monoidal closed and skew bi-closed categories.

We solve the problem by constructing cut-free sequent calculi for left skew monoidal closed and skew bi-closed categories, reminiscent of non-associative Lambek calculus, with trees as antecedents. Each calculus is respectively equivalent to the sequent calculus with stoup (for left skew monoidal categories) and the axiomatic calculus (for skew bi-closed categories). Moreover, the relational semantics of the axiomatic calculus for skew bi-closed categories provides an algebraic way to understand the internal relationship between the left and right skew monoidal (closed) categories.

ABSTRACT. The Nonassociative Lambek Calculus (NL) represents a logic devoid of the structural rules of exchange, weakening, and contraction, and it does not presume the associativity of its connectives. Its finitary consequence relation is decidable in polynomial time. However, the addition of classical connectives conjunction and disjunction makes consequence relation undecidable. Interestingly, if these connectives are distributive, the consequence relation is decidable in exponential time. This paper provides the proof, that we can merge classical logic and NL, and still consequence relation is decidable in exponential time.