In this paper we first show that Robin Smith’s ecthetic system SE for Aristotle’s assertoric syllogistic is not complete, despite what is claimed by Smith. SE is then not adequate to establish that ecthesis allows one to dispense with indirect or per impossibile deductions in Aristotle’s assertoric logic. As an alternative to SE, we then present a stronger system EC which is adequate for this purpose. EC is a nonexplosive ecthetic system which is shown to be (...) sound and complete with respect to all valid syllogistic arguments with a consistent set of premises. (shrink)

We introduce a basic intuitionistic conditional logic \(\textsf{IntCK}\) that we show to be complete both relative to a special type of Kripke models and relative to a standard translation into first-order intuitionistic logic. We show that \(\textsf{IntCK}\) stands in a very natural relation to other similar logics, like the basic classical conditional logic \(\textsf{CK}\) and the basic intuitionistic modal logic \(\textsf{IK}\). As for the basic intuitionistic conditional logic \(\textsf{ICK}\) proposed in Weiss (_Journal of Philosophical Logic_, _48_, 447–469, 2019 ), (...) \(\textsf{IntCK}\) extends its language with a diamond-like conditional modality \(\Diamond \hspace{-4.0pt}\rightarrow \), but its ( \(\Diamond \hspace{-4.0pt}\rightarrow \) )-free fragment is also a proper extension of \(\textsf{ICK}\). We briefly discuss the resulting gap between the two candidate systems of basic intuitionistic conditional logic and the possible pros and cons of both candidates. (shrink)

In the domain of information systems ontologies, the notion of completeness refers to ontological contents by demanding that they be exhaustive with respect to the domain that the ontology aims to represent. The purpose of this paper is to analyze such a notion, by distinguishing different varieties of completeness and by questioning its consistency with the open-world assumption, which formally assumes the incompleteness of conceptualizations on information systems ontologies.

For each truth-functionally complete set of connectives, we construct a sound and complete natural deduction system containing no axioms and the smallest possible number of inference rules, namely one.

In this paper, we extend the system AF2 in order to have the subject reduction for the $betaeta$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.

Combining modalities has proven to have interesting applications and many approaches that combine time with other types of modalities have been developed. One of these approaches uses accessibility functions between flows of time to study the basic properties of the functions, such as being total or partial, injective, surjective, etc. The completeness of certain systems expressing many of these properties, with the exception of surjectivity, has been proven. In this paper we propose a language with nominals to denote the initial (...) and final sets of each function in a model in order to obtain a complete system for reasoning about surjective partial functions. (shrink)

A formal logical system for sortal quantifiers, sortal identity and (second order) quantification over sortal concepts is formulated. The absolute consistency of the system is proved. A completeness proof for the system is also constructed. This proof is relative to a concept of logical validity provided by a semantics, which assumes as its philosophical background an approach to sortals from a modern form of conceptualism.

In previous works, we presented a modification of the usual possible world semantics by introducing an independent temporal structure in each world and using accessibility functions to represent the relation among them. Different properties ofthe accessibility functions have been considered and axiomatic systems which define these properties have been given. Only a few ofthese systems have been proved tobe complete. The aim ofthis paper is to make a progress in the study ofcompleteness for functional systems. For this end, we (...) use indexes as names for temporal flows and give new proofs of completeness. Specifically, we focus our attention on the system which defines injectivity, because the system which defines this property without using indexes was proved to be incomplete in previous works. The only system considered which remains incomplete is the one which defines surjectivity, even ifwe consider a sequence ofnatural extensions ofthe previous one. (shrink)

System image is an extension of multiplicative linear logic with the rules mix, nullary mix, and a self-dual, noncommutative logical operator, called seq. While the rules mix and nullary mix extend the deductive system, the operator seq extends the language of image. Due to the operator seq, system image extends the applications of image to those where the sequential composition is crucial, e.g., concurrency theory. System image is an extension of image with the rules mix and (...) nullary mix. In this paper, by relying on the fact that system image is a conservative extension of system image, I show that system image is NP-complete by encoding the 3-Partition problem in image. I provide a simple completeness proof of this encoding by resorting to a novel proof theoretical method for reducing nondeterminism in proof search, which is also of independent interest. (shrink)

This paper presents a calculus for mereotopological reasoning in which two-dimensional spatial regions are treated as primitive entities. A first order predicate language ℒ with a distinguished unary predicate c(x), function-symbols +, · and - and constants 0 and 1 is defined. An interpretation ℜ for ℒ is provided in which polygonal open subsets of the real plane serve as elements of the domain. Under this interpretation the predicate c(x) is read as 'region x is connected' and the function-symbols and (...) constants are given their meaning in terms of a Boolean algebra of polygons. We give an alternative interpretation ������ base on the real closed plane which turns out to be isomorphic to ℜ. A set of axioms and a rule of inference are introduced. We prove the soundness and completeness of the calculus with respect to the given interpretation. (shrink)

In this paper we present a tableau proof system for basic hybrid logic extended with quantification over basic modal propositions, and prove its completeness with respect to general models. This paper is largely devoted to the technical details of the proof, but we also discuss the link with the philosophical work of Arthur Prior, which led us to this system in the first place.

The usual completeness theorem for first-order logic is extended in order to allow for a natural incorporation of real analysis. Essentially, this is achieved by building in the set of real numbers into the structures for the language, and by adjusting other semantical notions accordingly. We use many-sorted languages so that the resulting formal systems are general enough for axiomatic treatments of empirical theories without recourse to elements of set theory which are difficult to interprete empirically. Thus we provide a (...) way of applying model theory to empirical theories without tricky detours. Our frame is applied to axiomatizations of three empirical theories: classical mechanics, phenomenological thermodynamics, and exchange economics. (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators or, in a more direct way, in which derivations are not translated. Both translations are (...) closely related in a canonical way. The two direct translations turn out to be complete. The paper fulfills the program of Church [1932], [1933] and Curry [1930] to base logic on a consistent system of λ-terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)

To the axioms of Peano arithmetic formulated in a language with an additional unary predicate symbol T we add the rules of necessitation and conecessitation T and axioms stating that T commutes with the logical connectives and quantifiers. By a result of McGee this theory is -inconsistent, but it can be approximated by models obtained by a kind of rule-of-revision semantics. Furthermore we prove that FS is equivalent to a system already studied by Friedman and Sheard and give an (...) analysis of its proof theory. (shrink)

This paper tackles an open problem posed by Åqvist. It is the problem of whether his dyadic deontic systemsEandFare complete with respect to their intended Hanssonian preference-based semantics. It is known that there are two different ways of interpreting what it means for a world to be best or top-ranked among alternatives. This can be understood as saying that it is optimal among them, or maximal among them. First, it is established that, under either the maximality rule or the (...) optimality rule,Eis sound and complete with respect to the class of all preference models, the class of those in which the betterness relation is reflexive, and the class of those in which it is total. Next, an analogous result is shown to hold forF. That is, it is established that, under either rule,Fis sound and complete with respect to the class of preference models in which the betterness relation is limited, the class of those in which it is limited and reflexive, and the class of those in which it is limited and total. (shrink)

Illative combinatory logic consists of the theory of combinators or lambda calculus extended by extra constants (and corresponding axioms and rules) intended to capture inference. The paper considers 4 systems of illative combinatory logic that are sound for first-order propositional and predicate calculus. The interpretation from ordinary logic into the illative systems can be done in two ways: following the propositions-as-types paradigm, in which derivations become combinators, or in a more direct way, in which derivations are not translated. Both translations (...) are closely related in a canonical way. In a preceding paper, Barendregt, Bunder and Dekkers, 1993, we proved completeness of the two direct translations. In the present paper we prove completeness of the two indirect translations by showing that the corresponding illative systems are conservative over the two systems for the direct translations. In another version, DBB (1997), we shall give a more direct completeness proof. These papers fulfill the program of Church and Curry to base logic on a consistent system of $\lambda$ -terms or combinators. Hitherto this program had failed because systems of ICL were either too weak (to provide a sound interpretation) or too strong (sometimes even inconsistent). (shrink)

In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions (...) of saturation (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

It is argued that behavior analysis is an actual or potential axiomatic system based upon the schedules of reinforcement which are behavioral, causative laws. Gödel proved that all axiomatic systems are complete or consistent, but not both at the same time. The point is made that behavior analysis is an incomplete, consistent system. The system's incompleteness is compensated for by the concept of the behavioral repertoire which, although in part lying outside of the axiomatic core of (...) behavior analysis, both extends and strengthens it. (shrink)

In previous articles, it has been shown that the deductive system developed by Aristotle in his "second logic" is a natural deduction system and not an axiomatic system as previously had been thought. It was also stated that Aristotle's logic is self-sufficient in two senses: First, that it presupposed no other logical concepts, not even those of propositional logic; second, that it is (strongly) complete in the sense that every valid argument expressible in the language of (...) the system is deducible by means of a formal deduction in the system. Review of the system makes the first point obvious. The purpose of the present article is to prove the second. Strong completeness is demonstrated for the Aristotelian system. (shrink)

We say that a system S of sentential calculus is an extension of a system R, if R and S have the same class of (meaningful) sentences, and every provable sentence of R is also provable in S. If the two classes of provable sentences do not coincide, we call S a proper extension of R. By a complete system of sentential calculus is meant one which is itself consistent, but has no consistent proper extensions. Thus (...) one cannot add a new independent primitive sentence to a complete system without obtaining an inconsistent system. The usual two-valued sentential calculus is complete in the sense defined. It has been shown by Lindenbaum that every incomplete system of sentential calculus possesses at least one complete extension. In this paper we shall examine how many complete extensions there are of some of the Lewis systems of sentential calculus. We shall show that there is only one complete extension of S4 (and hence also of S5, which is an extension of S4), and that there are infinitely many complete extensions of S2 (and hence also of S1, since S2 is an extension of S1). We leave open the question how many complete extensions there are of S3. (shrink)

The author establishes an elementary system AS which contains functions +, ≐ and a constant 0 and then proves the semi-completeness and the decidability of AS, using the theory of systems of inequalities.

Frege’s project has been characterized as an attempt to formulate a complete system of logic adequate to characterize mathematical theories such as arithmetic and set theory. As such, it was seen to fail by Gödel’s incompleteness theorem of 1931. It is argued, however, that this is to impose a later interpretation on the word ‘complete’ it is clear from Dedekind’s writings that at least as good as interpretation of completeness is categoricity. Whereas few interesting first-order mathematical theories (...) are categorical or complete, there are logical extensions of these theories into second-order and by the addition of generalized quantifiers which are categorical. Frege’s project really found success through Gödel’s completeness theorem of 1930 and the subsequent development of first- and higher-order model theory. (shrink)

The Quantified Argument Calculus (Quarc) is a formal logic system, first developed by Hanoch Ben-Yami in (Ben-Yami 2014), and since then extended and applied by several authors. The aim of this paper is to further these contributions by, first, providing a philosophical motivation for the truth-valuational, substitutional approach of (Ben-Yami 2014) and defending it against a common objection, a topic also of interest beyond its specific application to Quarc. Second, we fill the formal lacunae left in the original presentation, (...) which did not incorporate identity systematically into Quarc, and although it proved the soundness of the system did not prove its completeness. (shrink)

The most difficult problem that Leniewski came across in constructing his system of the foundations of mathematics was the problem of defining definitions, as he used to put it. He solved it to his satisfaction only when he had completed the formalization of his protothetic and ontology. By formalization of a deductive system one ought to understand in this context the statement, as precise and unambiguous as possible, of the conditions an expression has to satisfy if it is (...) added to the system as a new thesis. Now, some protothetical theses, and some ontological ones, included in the respective systems, happen to be definitions. In the present essay I employ Leniewski's method of terminological explanations for the purpose of formalizing ukasiewicz's system of implicational calculus of propositions, which system, without having recourse to quantification, I first extended some time ago into a functionally complete system. This I achieved by allowing for a rule of implicational definitions, which enabled me to define any propositionforming functor for any finite number of propositional arguments. (shrink)

This paper establishes two related structural results within the Cognitional Mechanics (CM) framework. Part I proves that the spectral coupling constant ξ² = (μα)² is a complete statistic for the observational content of M₃(ℂ). The state space S is defined generatively as the union of O-orbits of the one-parameter family H_λ = diag(λ, λ, −2λ), where O is the operation algebra derived from axioms A1–A4. Normality of all elements of S holds by construction, eliminating Jordan structure entirely. The residual (...) degree of freedom is λ ∈ ℝ⁺, uniquely recoverable from any state s via λ(s) = √(Tr(s²)/6). The map f(s) = Tr(s²)·(αμ₀)² satisfies f ∝ λ² and induces a bijection S/∼_f ≅ Im(f) of dimension exactly 1: all observational distinctions within M₃(ℂ) collapse to a single scalar. Part II classifies the 19 Standard Model parameters as eigenvalue-type (12), orbit-invariant (4), and basis-mixing (3) projections of Spec(D), and bounds the independent degrees of freedom to at most 11. The connecting corollary establishes that every Standard Model projection map πᵢ is a rational function of ξ² alone, so that the Standard Model parameter structure is a representation layer of the invariant algebra, not an independent ontological structure. Anomaly cancellation and asymptotic freedom are shown to be algebraic necessities of M₃(ℂ) at n = 3. A falsifiable prediction is derived: the ratio αₛ/α_em at the Planck scale equals Φ₃/Φ₆ = 13/7 ≈ 1.857, deviating from the Standard Model perturbative result by approximately 0.24. No free parameters are introduced at any stage. All logical gaps are closed within the CM axiom system. -/- Published on April 26, 2026 doi: 10.5281/zenodo.19784769 . (shrink)

This paper is the second in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)

ABSTRACT In this paper we study consequence relations on the set of many sided sequents over a propositional language. We deal with the consequence relations axiomatized by the sequent calculi defined in [2] and associated with arbitrary finite algebras. These consequence relations are examples of what we call Gentzen systems. We define a semantics for these systems and prove a Strong Completeness Theorem, which is an extension of the Completeness Theorem for provable sequents stated in [2]. For the special case (...) of the finite linear MV-algebras, the Strong Completeness Theorem was proved in [10], as a consequence of McNaughton's Theorem. The main tool to prove this result for arbitrary algebras is the deduction-detachment theorem for Gentzen systems. (shrink)

Towards the end of his life, Descartes published the first four parts of a projected six-part work, The Principles of Philosophy. This was intended to be the definitive statement of his complete system of philosophy, dealing with everything from cosmology to the nature of human happiness. In this book, Stephen Gaukroger examines the whole system, and reconstructs the last two parts, 'On Living Things' and 'On Man', from Descartes' other writings. He relates the work to the tradition (...) of late Scholastic textbooks which it follows, and also to Descartes' other philosophical writings, and he examines the ways in which Descartes transformed not only the practice of natural philosophy but also our understanding of what it is to be a philosopher. His book is a comprehensive examination of Descartes' complete philosophical system. (shrink)

In 2015 Dag Prawitz proposed an Ecumenical system where classical and intuitionistic logic could coexist in peace. The classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz’ main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. The aim of the present paper is (...) [1] to prove the normalization theorem for the propositional fragment NEp of Prawitz’ ecumenical system, and [2] to show that NEp is sound and complete with respect to a Kripke-style semantics for the language of NEp. (shrink)

The article concerns two axiom systems of Słupecki for the functionally complete three-valued propositional logic: W1–W6 and A1–A9. The article proves that both of them are inadequate—W1–W6 is semantically incomplete, on the other hand, A1–A9 governs a functionally incomplete calculus, and thus, it cannot be a semantically complete axiom system for the functionally complete three-valued logic.

Dmitrii Mendeleev’s periodic system is known for its predictive accuracy, but talk of its completeness is rarer. This is surprising because completeness was a quality that Mendeleev saw as important for a systematization of the chemical elements. Here, I explain how Mendeleev’s valuing of completeness influenced the development of his periodic system. After introducing five indicators of its completeness, I zoom into one in particular: Mendeleev’s inclusion of a schematic row of oxides. I then show how it guided (...) Mendeleev’s predictions of indium and ekaboron, which suggests that the valuing of completeness was instrumental for making predictions. (shrink)

This paper is the first in a two-part series in which we discuss several notions of completeness for systems of mathematical axioms, with special focus on their interrelations and historical origins in the development of the axiomatic method. We argue that, both from historical and logical points of view, higher-order logic is an appropriate framework for considering such notions, and we consider some open questions in higher-order axiomatics. In addition, we indicate how one can fruitfully extend the usual set-theoretic semantics (...) so as to shed new light on the relevant strengths and limits of higher-order logic. (shrink)

A simple complete axiomatic system is presented for the many-valued propositional logic based on the conjunction interpreted as product, the coresponding implication (Goguen's implication) and the corresponding negation (Gödel's negation). Algebraic proof methods are used. The meaning for fuzzy logic (in the narrow sense) is shortly discussed.

Hereditary structural completeness is established for a range of substructural logics, mainly without the weakening rule, including fragments of various relevant or many-valued logics. Also, structural completeness is disproved for a range of systems, settling some previously open questions.