Kooi and Tamminga's correspondence analysis is a technique for designing proof systems, mostly, natural deduction and sequent systems. In this paper it is used to generate sequent calculi with invertible rules, whose only branching rule is the rule of cut. The calculi pertain to classical propositional logic and any of its fragments that may be obtained from adding a set of rules characterizing a two-argument Boolean function to the negation fragment of classical propositional logic. The properties of soundness and completeness (...) of the calculi are demonstrated. The proof of completeness is conducted by Kalmár's method. Most of the presented sequent-calculus rules have been obtained automatically, by a rule-generating algorithm implemented in Python. Correctness of the algorithm is demonstrated. This automated approach allowed us to analyse thousands of possible rules' schemes, hundreds of rules corresponding to Boolean functions, and to nd dozens of those invertible. Interestingly, the analysis revealed that the presented proof-theoretic framework provides a syntactic characteristics of such an important semantic property as functional completeness. (shrink)

This issue of Bijdragen ends with a new edition, on the basis of more manuscripts, of CPL 1752. This credal text was first published in this journal in 1991, with an extensive commentary.

This paper introduces the construct of an ultravaluation inspired by the well-known ultraproduct. Basic properties and exemplary applications of this notion are shown: for compactness and definability theorems. We also use ultravaluations to check failure of compactness and undefinability.

The Gelasian letter, Famuli uestrae pietatis, addressed to Emperor Anastasius I (491-518), is famous for the so-called theory of two powers that has enjoyedconsiderable fortune and has received continual attention in the history and thought of the Latin West in view of its arguments about the relationshipbetween the Church and secular power. Scholars have been primarily interested in the Wirkungsgeschichte of the letter. Less frequently studied is the letter's specific religious context, characterized by the Acacian schism (484- 519), the dispute (...) between the episcopal sees of Rome and Constantinople. This article seeks to situate this document from the late fifth-century Roman pontifical chancery in its specific historical and ecclesial context, and to provide a commentary on the entire letter. A brief, final chapter offers a synthetic excursus on the immediate reception of the text in the Early Middle Ages before the Gregorian Reform. (shrink)

Journal of Mathematical Logic, Volume 22, Issue 03, December 2022. We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory [math] of [E. Jeřábek, Approximate counting by hashing in bounded arithmetic, J. Symb. Log. 74(3) (2009) 829–860]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational (...) characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS. As CPLS is provably total in the theory [math], this shows that [math] does not prove every [math] sentence which is provable in bounded arithmetic. This answers the question posed in [S. Buss, L. A. Kołodziejczyk and N. Thapen, Fragments of approximate counting, J. Symb. Log. 79(2) (2014) 496–525] and represents some progress in the program of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences. Our main technical tool is an extension of the “fixing lemma” from [P. Pudlák and N. Thapen, Random resolution refutations, Comput. Complexity, 28(2) (2019) 185–239], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a [math] oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic. (shrink)

An important field of probability logic is the investigation of inference rules that propagate point probabilities or, more generally, interval probabilities from premises to conclusions. Conditional probability logic (CPL) interprets the common sense expressions of the form “if . . . , then . . . ” by conditional probabilities and not by the probability of the material implication. An inference rule is probabilistically informative if the coherent probability interval of its conclusion is not necessarily equal to the unit interval (...) [0, 1]. Not all logically valid inference rules are probabilistically informative and vice versa. The relationship between logically valid and probabilistically informative inference rules is discussed and illustrated by examples such as the modus ponens or the affirming the consequent. We propose a method to evaluate the strength of CPL inference. (shrink)

There are two foundational, but not fully developed, ideas in paraconsistency, namely, the duality between paraconsistent and intuitionistic paradigms, and the introduction of logical operators that express meta-logical notions in the object language. The aim of this paper is to show how these two ideas can be adequately accomplished by the Logics of Formal Inconsistency (LFIs) and by the Logics of Formal Undeterminedness (LFUs). LFIs recover the validity of the principle of explosion in a paraconsistent scenario, while LFUs recover the (...) validity of the principle of excluded middle in a paracomplete scenario. We introduce definitions of duality between inference rules and connectives that allow comparing rules and connectives that belong to different logics. Two formal systems are studied, the logics mbC and mbD, that display the duality between paraconsistency and paracompleteness as a duality between inference rules added to a common core– in the case studied here, this common core is classical positive propositional logic (CPL + ). The logics mbC and mbD are equipped with recovery operators that restore classical logic for, respectively, consistent and determined propositions. These two logics are then combined obtaining a pair of logics of formal inconsistency and undeterminedness (LFIUs), namely, mbCD and mbCDE. The logic mbCDE exhibits some nice duality properties. Besides, it is simultaneously paraconsistent and paracomplete, and able to recover the principles of excluded middle and explosion at once. The last sections offer an algebraic account for such logics by adapting the swap-structures semantics framework of the LFIs the LFUs. This semantics highlights some subtle aspects of these logics, and allows us to prove decidability by means of finite non-deterministic matrices. (shrink)

This article analyzes gun carry licensing as a disciplinary mechanism that places African American men in a liminal zone where they are legally armed but presumed dangerous, even as African Americans now experience broadened access to concealed pistol licenses amid contemporary U.S. gun laws. Using observational data from now-defunct public gun boards in Metropolitan Detroit, this article systematically explores how CPLs are mobilized by administrators to reflect and reinforce racial/gender hierarchies. This article broadens scholarly understandings of how tropes of (...) criminality shape racialized men’s encounters with the state beyond nonvoluntary, coercive settings and unpacks how race and gender interlock to shape these encounters. I extend insights from intersectionality scholarship to examine gun board meetings as degradation ceremonies whereby African American men are held accountable to controlling images of Black masculinity in exchange for a CPL. This article sharpens the conceptual apparatus that accounts for marginalized men’s subordination vis-à-vis the state by focusing on the provision of legitimate violence and revealing the persistent, if paradoxical, mobilization of legitimate violence in the reproduction of racial/gender hierarchies. (shrink)

In this paper we study intermediate logics between the logic G≤∼, the degree preserving companion of Gödel fuzzy logic with involution G∼ and classical propositional logic CPL, as well as the intermediate logics of their finite-valued counterparts G≤n∼. Although G≤∼ and G≤ are explosive w.r.t. Gödel negation ¬, they are paraconsistent w.r.t. the involutive negation ∼. We introduce the notion of saturated paraconsistency, a weaker notion than ideal paraconsistency, and we fully characterize the ideal and the saturated paraconsistent logics between (...) G≤n∼ and CPL. We also identify a large family of saturated paraconsistent logics in the family of intermediate logics for degree-preserving finite-valued Łukasiewicz logics. (shrink)

?On or about XX1100XXX2009? I arrived at Compound XX, TIF Defender, Camp Bucca Iraq and discovered that SFC XXXX and CPL XXXX had, in contravention of standard operating procedure and the requirements of Combined Joint Task Force 134 General Orders, entered Compound XX without first securing all detainees in the Salat, and walked to the rear fenceline through the occupied Compound, many times within deadspace [outside the] guard force's line of sight, and back through the sally port.1 SFC XXXX and (...) CPL XXXX were unmolested during this entry. No prior coordination was performed with the other members of the guard force, other than PFC XXXX who was ordered by SFC XXXX to open the sally port to allow entry. SFC XXXX and CPL XXXX were in a Compound occupied at the time by approximately 1038 Iraqi Security Detainees, and could have been harmed or taken hostage with little warning, leaving the guard force few options other than to attempt to defend SFC XXXX and CPL XXXX by lethal means, as these were the only weapons available that had the range and accuracy required? (shrink)

Contrary to received opinion, the Aristotelian Square of Opposition (square) is logically sound, differing from standard modern predicate logic (SMPL) only in that it restricts the universe U of cognitively constructible situations by banning null predicates, making it less unnatural than SMPL. U-restriction strengthens the logic without making it unsound. It also invites a cognitive approach to logic. Humans are endowed with a cognitive predicate logic (CPL), which checks the process of cognitive modelling (world construal) for consistency. The square is (...) considered a first approximation to CPL, with a cognitive set-theoretic semantics. Not being cognitively real, the null set Ø is eliminated from the semantics of CPL. Still rudimentary in Aristotle’s On Interpretation (Int), the square was implicitly completed in his Prior Analytics (PrAn), thereby introducing U-restriction. Abelard’s reconstruction of the logic of Int is logically and historically correct; the loca (Leaking O-Corner Analysis) interpretation of the square, defended by some modern logicians, is logically faulty and historically untenable. Generally, U-restriction, not redefining the universal quantifier, as in Abelard and loca, is the correct path to a reconstruction of CPL. Valuation Space modelling is used to compute the effects of U-restriction. (shrink)

This note is on cautious cut elimination for one of Veitman's might logics. Syntactically, the logic is presented as an extension of a sequent system for classical proposition logic . I show that this extension preserves the completeness and decidability of CPL. The proof has cautious cut elimination as a corollary. I also give a rather general syntactic proof of cautious cut elimination. It states that any ‘base’ logic which has a reflexive, monotone consequence relation that allows cautious cut to (...) be eliminated preserves cautious cut elimination when extended to a might logic. (shrink)

Through an analysis of the transmission and the historical context of the text, as well as of the doctrinal content of CPL 1610, this paper substantiates the likelihood of the Gelasian authorship of the letter, which was called into question by Coustant Thiel and Schwartz and supported by Nautin.