By algebraic means, we give an equational axiomatization of the equational fragments of various systems of arithmetic. We also introduce a faithful semantics according to which, for every reasonable system T for arithmetic, there is a model where exactly the theorems of T are true.

In treatises or advanced textbooks on theoretical physics, it is apparent that the way mathematics is used is very different from what is to be found in books of mathematics. There is, for example, no close connection between books on analysis, on the one hand, and any classical textbook in quantum mechanics, for example, Schiff, [11], or quite recent books, for example Ryder, [10], on quantum field theory. The differences run a good deal deeper than the fact that the books (...) on theoretical physics are not written in the definition-theorem-proof style characteristic of pure mathematics. Although a good many propositions are proved in the books on physics, there are almost with exception no existential proofs, and consequently there is no really serious systematic use of quantifiers. Another important characteristic is the free use of infinitesimals. In fact, most results would not lose anything, from a physicist's point of view, by leaving them in approximate form, i.e., instead of strict equalities or inequalities, using equalities or inequalities only up to an infinitesimal.The discrepancy between the way mathematics is ordinarily done in theoretical physics and the way it is built up from a foundational standpoint in any of the standard modern views raises the question of whether it might be possible to construct quite directly a rigorous foundation that reflects a significant part of this standard practice in theoretical physics. Other parts of standard practice in physics, for example, the use of physically intuitive but nonrigorous arguments, are not present in our system. (shrink)

In this paper we provide quantifier-free, constructive axiomatizations for 2-dimensional absolute, Euclidean, and hyperbolic geometry. The main novelty consists in the first-order languages in which the axiom systems are formulated.

We present a general approach to quantified modal logics that can simulate most other approaches. The language is based on operators indexed by terms which allow to express de re modalities and to control the interaction of modalities with the first-order machinery and with non-rigid designators. The semantics is based on a primitive counterpart relation holding between n-tuples of objects inhabiting possible worlds. This allows an object to be represented by one, many, or no object in an accessible world. Moreover (...) by taking as primitive a relation between n-tuples we avoid some shortcoming of standard individual counterparts. Finally, we use cut-free labelled sequent calculi to give a proof-theoretic characterisation of the quantified extensions of each first-order definable propositional modal logic. In this way we show how to complete many axiomatically incomplete quantified modal logics. (shrink)

This paper contains an axiomatic theory of first order modal logic with operations, identity, and descriptions together with a formal semantics which interprets the theory in such a manner that empty universes of discourse and denotationless terms are allowed for at each possible world. The intuitive basis of the theory is discussed in preliminary sections, the syntax and semantics of theory are then characterized, its semantical adequacy is demonstrated, and certain important axioms and theorems are discussed in detail in later (...) sections. (shrink)

When restricted to proving $\Sigma _{i}^{q}$ formulas, the quantified propositional proof system $G_{i}^{\ast}$ is closely related to the $\Sigma _{i}^{b}$ theorems of Buss's theory $S_{2}^{i}$ . Namely, $G_{i}^{\ast}$ has polynomial-size proofs of the translations of theorems of $S_{2}^{i}$ , and $S_{2}^{i}$ proves that $G_{i}^{\ast}$ is sound. However, little is known about $G_{i}^{\ast}$ when proving more complex formulas. In this paper, we prove a witnessing theorem for $G_{i}^{\ast}$ similar in style to the KPT witnessing theorem for $T_{2}^{i}$ . This witnessing theorem (...) is then used to show that $S_{2}^{i}$ proves $G_{i}^{\ast}$ is sound with respect to $\Sigma _{i+1}^{q}$ formulas. Note that unless the polynomial-time hierarchy collapses $S_{2}^{i}$ is the weakest theory in the s₂ hierarchy for which this is true. The witnessing theorem is also used to show that $G_{i}^{\ast}$ is p-equivalent to a quantified version of extended-Frege for prenex formulas. This is followed by a proof that Gi p-simulates $G_{i+1}^{\ast}$ with respect to all quantified propositional formulas. We finish by proving that S₂ can be axiomatized by $S_{2}^{1}$ plus axioms stating that the cut-free version of $G_{0}^{\ast}$ is sound. All together this shows that connection between $G_{i}^{\ast}$ and $S_{2}^{i}$ does not extend to more complex formulas. (shrink)

Sentences containing definite descriptions, expressions of the form ‘The F’, can be formalised using a binary quantifier ι that forms a formula out of two predicates, where ιx[F, G] is read as ‘The F is G’. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the system INFι of intuitionist negative free logic extended by such a quantifier, which was presented in (...) (Kürbis 2019), INFι is first compared to a system of Tennant’s and an axiomatic treatment of a term forming ι operator within intuitionist negative free logic. Both systems are shown to be equivalent to the subsystem of INFι in which the G of ιx[F, G] is restricted to identity. INFι is then compared to an intuitionist version of a system of Lambert’s which in addition to the term forming operator has an operator for predicate abstraction for indicating scope distinctions. The two systems will be shown to be equivalent through a translation between their respective languages. Advantages of the present approach over the alternatives are indicated in the discussion. (shrink)

Free logics is a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that the domain of interpretation is not empty, every name denotes exactly one object in the domain and the quantifiers have existential import. Free logics usually reject the claim that names need to denote in, and of the systems considered in this paper, the positive free logic concedes that (...) some atomic formulas containing non-denoting names are true, while negative free logic rejects even the latter claim. Inclusive logics, which reject, are likewise considered. These logics have complex and varied axiomatizations and semantics, and the goal of this paper is to present an orderly examination of the various systems and their mutual relations. This is done by first offering a formalization, using sequent calculi which possess all the desired structural properties of a good proof system, including admissibility of contraction and cut, while streamlining free logics in a way no other approach has. We then present a simple and unified system of abstract semantics, which allows for a straightforward demonstration of the meta-theoretical properties, and offers insights into the relationship between different logics. The final part of this paper is dedicated to extending the system with modalities by using a labeled sequent calculus, and here we are again able to map out the different approaches and their mutual relations using the same framework. (shrink)

We investigate quantifier-free induction for Lisp-like lists constructed inductively from the empty list $$ nil $$ nil and the operation $${\textit{cons}}$$ cons, that adds an element to the front of a list. First we show that, for $$m \ge 1$$ m ≥ 1, quantifier-free $$m$$ m -step induction does not simulate quantifier-free $$(m + 1)$$ ( m + 1 ) -step induction. Secondly, we show that for all $$m \ge 1$$ m ≥ 1, quantifier-free $$m$$ m -step induction does not (...) prove the right cancellation property of the concatenation operation on lists defined by left-recursion. (shrink)

The semantical structures called T x W frames were introduced in (Thomason, 1984) for the Ockhamist temporal-modal language, $[Unrepresented Character]_{o}$ , which consists of the usual propositional language augmented with the Priorean operators P and F and with a possibility operator ◇. However, these structures are also suitable for interpreting an extended language, $[Unrepresented Character]_{so}$ , containing a further possibility operator $\lozenge^{s}$ which expresses synchronism among possibly incompatible histories and which can thus be thought of as a cross-history 'simultaneity' operator. (...) In the present paper we provide an infinite set of axioms in $[Unrepresented Character]_{so}$ , which is shown to be strongly complete for T x W-validity. Von Kutschera (1997) contains a finite axiomatization of T x W-validity which however makes use of the Gabbay Irreflexivity Rule (Gabbay, 1981). In order to avoid using this rule, the proof presented here develops a new technique to deal with reflexive maximal consistent sets in Henkin-style constructions. (shrink)

The semantical structures called T×W frames were introduced in (Thomason, 1984) for the Ockhamist temporal-modal language, ℒO, which consists of the usual propositional language augmented with the Priorean operators P and F and with a possibility operator ⋄. However, these structures are also suitable for interpreting an extended language, ℒSO, containing a further possibility operator ⋄s which expresses synchronism among possibly incompatible histories and which can thus be thought of as a cross-history ‘simultaneity’ operator. In the present paper we provide (...) an infinite set of axioms in ℒSO, which is shown to be strongly complete forT ×W-validity. Von Kutschera (1997) contains a finite axiomatization of T×W-validity which however makes use of the Gabbay Irreflexivity Rule (Gabbay, 1981). In order to avoid using this rule, the proof presented here develops a new technique to deal with reflexive maximal consistent sets in Henkin-style constructions. (shrink)

We consider the notion of bounded m-ary patch-width defined in [9], and its very close relative m-constructibility defined below. We show that the notions of m-constructibility all coincide for m ≥ 3, while 1-constructibility is a weaker notion. The same holds for bounded m-ary patch-width. The case m = 2 is left open.

The following result is an approximation to the answer of the question of Kokorin about decidability of a quantifier-free theory of field of rational numbers. Let Q0 be a subset of the set of all rational numbers which contains integers 1 and −1. Let be a set containing Q0 and closed by the functions of addition, subtraction and multiplication. For example coincides with Q0 if Q0 is the set of all binary rational numbers or the set of all decimal rational (...) numbers. It is clear that , where Z is the set of all integers and Q is the set of all rational numbers. A negationless theory uses only conjunction and disjunction as logical connectives. Let T be a quantifier-free negationless elementary theory of signature , where Pol is the list of all polynomials with rational coefficients from Q0 in which exponent of the polynomials and rational coefficients are written in binary number system. Theorem 1. Theory T is NP-hard and if is everywhere dense then the theory T is decidable by an algorithm which belongs to EXPTIME. The set of all rational numbers or the set of all binary rational numbers may be taken instead of . The quantifier-free negationless theory of the field of rational numbers may be regarded as a base of constructive mathematics. (shrink)

This paper continues the investigations begun in [6] and continued in [7] about quantifier-free axiomatizations of plane Euclidean geometry using ternary operations. We show that plane Euclidean geometry over Archimedean ordered Euclidean fields can be axiomatized using only two ternary operations if one allows axioms that are not first-order but universal Lw1,w sentences. The operations are: the transport of a segment on a halfline that starts at one of the endpoints of the given segment, and the operation which produces one (...) of the intersection points of a perpendicular on a diameter of a circle with that circle. MSC: 03F65, 51M05, 51M15. (shrink)

One of the central logical ideas in Wittgenstein’sTractatus logico-philosophicusis the elimination of the identity sign in favor of the so-called “exclusive interpretation” of names and quantifiers requiring different names to refer to different objects and (roughly) different variables to take different values. In this paper, we examine a recent development of these ideas in papers by Kai Wehmeier. We diagnose two main problems of Wehmeier’s account, the first concerning the treatment of individual constants, the second concerning so-called “pseudo-propositions” (Scheinsätze) of (...) classical logic such as$a=a$or$a=b \wedge b=c \rightarrow a=c$. We argue that overcoming these problems requires two fairly drastic departures from Wehmeier’s account: (1) Not every formula of classical first-order logic will be translatable into asingleformula of Wittgenstein’s exclusive notation. Instead, there will often be a multiplicity of possible translations, revealing the original “inclusive” formulas to beambiguous. (2) Certain formulas of first-order logic such as$a=a$will not be translatable into Wittgenstein’s notation at all, being thereby revealed as nonsensical pseudo-propositions which should be excluded from a “correct” conceptual notation. We provide translation procedures from inclusive quantifier-free logic into the exclusive notation that take these modifications into account and define a notion of logical equivalence suitable for assessing these translations. (shrink)

We study the computational complexity of the model checking problem for quantifier-free dependence logic ${(\mathcal{D})}$ formulas. We characterize three thresholds in the complexity: logarithmic space (LOGSPACE), non-deterministic logarithmic space (NL) and non-deterministic polynomial time (NP).

In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of Gödel"s functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for Π0 1-axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.

In Cieśliński (J Philos Logic 39:325–337, 2010), Cieśliński asked whether compositional truth theory with the additional axiom that all propositional tautologies are true is conservative over Peano Arithmetic. We provide a partial answer to this question, showing that if we additionally assume that truth predicate agrees with arithmetical truth on quantifier-free sentences, the resulting theory is as strong as $$\Delta _0$$ Δ 0 -induction for the compositional truth predicate, hence non-conservative. On the other hand, it can be shown with a (...) routine argument that the principle of quantifier-free correctness is itself conservative. (shrink)

We axiomatize all quantifier properties which can be expressed by a universal condition on the class of algebras of sets.

Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of ∃x◻φ, e.g., knowing how to achieve φ roughly means that there exists a way such that you know that it is a way to ensure that φ. Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we (...) propose a very general and powerful framework based on quantifier-free predicate language extended by a new modality, which packs exactly ∃x◻ together. We show that the resulting language, though much more expressive, shares many good properties of the basic propositional modal logic over arbitrary models, such as finite-tree-model property and van Benthem-like characterization w.r.t.\ first-order modal logic. We axiomatize the logic over S5 frames with intuitive axioms to capture the interaction between the new modality and know-that operator in an epistemic setting. (shrink)

A calculus of names is a logical theory describing relations between names. By a pure calculus of names we mean a quantifier-free formulation of such a theory, based on classical propositional calculus. An axiomatisation of a pure calculus of names is presented and its completeness is discussed. It is shown that the axiomatisation is complete in three different ways: with respect to a set theoretical model, with respect to Leśniewski's Ontology and in a sense defined with the use of axiomatic (...) rejection. The independence of axioms is proved. A decision procedure based on syntactic transformations and models defined in the domain of only two members is defined. (shrink)

Hyperbolic geometry can be axiomatized using the notions of order andcongruence (as in Euclidean geometry) or using the notion of incidencealone (as in projective geometry). Although the incidence-based axiomatizationmay be considered simpler because it uses the single binary point-linerelation of incidence as a primitive notion, we show that it issyntactically more complex. The incidence-based formulation requires some axioms of the quantifier-type \forall\exists\forall, while the axiom system based on congruence and order can beformulated using only \forall\exists-axioms.

In this paper we provide quantifier-free, constructive axiomatizations for several fragments of plane Euclidean geometry over Euclidean fields, such that each axiom contains at most 4 variables. The languages in which they are expressed contain only at most ternary operations. In some precisely defined sense these axiomatizations are the simplest possible.

We provide tools for a concise axiomatization of a broad class of quantifiers in many-valued logic, so-called distribution quantifiers. Although sound and complete axiomatizations for such quantifiers exist, their size renders them virtually useless for practical purposes. We show that for quantifiers based on finite distributive lattices compact axiomatizations can be obtained schematically. This is achieved by providing a link between skolemized signed formulas and filters/ideals in Boolean set lattices. Then lattice theoretic tools such as Birkhoff's representation theorem for (...) finite distributive lattices are used to derive tableau-style axiomatizations of distribution quantifiers. (shrink)

The present article employs a model-theoretic semantics to interpret a fragment of the language of the Quantified Argument Calculus (Quarc), a recently introduced logical system whose main aim is capturing the structure of natural language sentences in a closer way than does the language of classical logic. The main contribution is an axiomatization for the set of formulas that are valid in all standard interpretations within the employed semantics.

In this paper we provide a quantifier-free, constructive axiomatization of metric-Euclidean and of rectangular planes . The languages in which the axiom systems are expressed contain three individual constants and two ternary operations. We also provide an axiom system in algorithmic logic for finite Euclidean planes, and for several minimal metric-Euclidean planes. The axiom systems proposed will be used in a sequel to this paper to provide ‘the simplest possible’ axiom systems for several fragments of plane Euclidean geometry.

Hyperbolic geometry can be axiomatized using the notions of order andcongruence (as in Euclidean geometry) or using the notion of incidencealone (as in projective geometry). Although the incidence-based axiomatizationmay be considered simpler because it uses the single binary point-linerelation of incidence as a primitive notion, we show that it issyntactically more complex. The incidence-based formulation requires some axioms of the quantifier-type forallexistsforall, while the axiom system based on congruence and order can beformulated using only forallexists-axioms.

We axiomatize all quantifier properties which can be expressed by a universal condition on the class of algebras of sets.

In this paper we provide a quantifier-free constructive axiomatization for Euclidean planes in a first-order language with only ternary operation symbols and three constant symbols . We also determine the algorithmic theories of some ‘naturally occurring’ plane geometries.

The paper presents an epistemic logic with quantification over agents of knowledge and with a syntactical distinction between de re and de dicto occurrences of terms. Knowledge de dicto is characterized as ‘knowledge that’, and knowlegde de re as ‘knowledge of’. Transition semantics turns out to be an adequate tool to account for the distinctions introduced.

Axiomatics which do not employ rules of inference other than the cut rule are given for commutative product-free Lambek calculus in two variants: with and without the empty string. Unlike the former variant, the latter one turns out not to be finitely axiomatizable in that way.

Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automated reasoning tools integrated with Isabelle/HOL. We also address the (...) relation of our axiom systems to alternative proposals from the literature, including an axiom set proposed by Freyd and Scedrov for which we reveal a technical issue (when encoded in free logic where free variables range over defined and undefined objects): either all operations, e.g. morphism composition, are total or their axiom system is inconsistent. The repair for this problem is quite straightforward, however. (shrink)

We investigate how the sentence choice semantics for propositional superposition logic developed in Tzouvaras could be extended so as to successfully apply to first-order superposition logic. There are two options for such an extension. The apparently more natural one is the formula choice semantics based on choice functions for pairs of arbitrary formulas of the basis language. It is proved however that the universal instantiation scheme of first-order logic, $\varphi \rightarrow \varphi $, is false, as a scheme of tautologies, with (...) respect to FCS. This causes the total failure of FCS as a candidate semantics. Then we turn to the other option, which is a variant of SCS, since it uses again choice functions for pairs of sentences only. This semantics however presupposes that the applicability of the connective | is restricted to quantifier-free sentences, and thus the class of well-formed formulas and sentences of the language is restricted too. Granted these syntactic restrictions, the usual axiomatizations of FOLS turn out to be sound and conditionally complete with respect to this second semantics, just like the corresponding systems of PLS. (shrink)

In 1958 Gödel published his Dialectica interpretation, which reduces classical arithmetic to a quantifier-free theory T axiomatizing the primitive recursive functionals of finite type. Here we extend Gödel's T to theories Pn of “predicative” functionals, which are defined using Martin-Löf's universes of transfinite types. We then extend Gödel's interpretation to the theories of arithmetic inductive definitions IDn, so that each IDn is interpreted in the corresponding Pn. Since the strengths of the theories IDn are cofinal in the ordinal Γ0, as (...) a corollary this analysis provides an ordinal-free characterization of the <Γ0-recursive functions. (shrink)

Independently and pursuing different aims, Hrushovski and Srour (On stable non-equational theories. Unpublished manuscript, 1989) and Baudisch and Pillay (J Symb Log 65(1):443–460, 2000) have introduced two free pseudospaces that generalize the well know concept of Lachlan’s free pseudoplane. In this paper we investigate the relationship between these free pseudospaces, proving in particular, that the pseudospace of Baudisch and Pillay is a reduct of the pseudospace of Hrushovski and Srour.

This paper expands upon the work by Wang (Proceedings of TARK, pp. 493–512, 2017) who proposes a new framework based on quantifier-free predicate language extended by a new bundled modality \(\exists x\Box \) and axiomatizes the logic over S5 frames. This paper first gives complete axiomatizations of the logics over K, D, T, 4, S4 frames with increasing domains and constant domains, respectively. The systems w.r.t. constant domains feature infinitely many additional rules defined inductively than systems w.r.t. increasing domains. In (...) the second part of the paper, we show that these rules are admissible in the systems without them by providing a general strategy for proving completeness theorems for the logics without these rules over constant domain models (also increasing domain models). (shrink)

This paper presents a way of formalising definite descriptions with a binary quantifier ι, where ιx[F, G] is read as ‘The F is G’. Introduction and elimination rules for ι in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form ιx[F, G] are given, and it is shown that deductions in the system can be brought into normal form.

Wilkie 5 397) proved a “theorem of the complement” which implies that in order to establish the o-minimality of an expansion of with C∞ functions it suffices to obtain uniform bounds on the number of connected components of quantifier free definable sets. He deduced that any expansion of with a family of Pfaffian functions is o-minimal. We prove an effective version of Wilkie's theorem of the complement, so in particular given an expansion of the ordered field with finitely many C∞ (...) functions, if there are uniform and computable upper bounds on the number of connected components of quantifier free definable sets, then there are uniform and computable bounds for all definable sets. In such a case the theory of the structure is effectively o-minimal: there is a recursively axiomatized subtheory such that each of its models is o-minimal. This implies the effective o-minimality of any expansion of with Pfaffian functions. We apply our results to the open problem of the decidability of the theory of the real field with the exponential function. We show that the decidability is implied by a positive answer to the following problem ): given a language L expanding the language of ordered rings, if an L-sentence is true in every L-structure expanding the ordered field of real numbers, then it is true in every o-minimal L-structure expanding any real closed field. (shrink)

A predicate extension SQHT= of the logic of here-and-there was introduced by V. Lifschitz, D. Pearce, and A. Valverde to characterize strong equivalence of logic programs with variables and equality with respect to stable models. The semantics for this logic is determined by intuitionistic Kripke models with two worlds with constant individual domain and decidable equality. Our sequent formulation has special rules for implication and for pushing negation inside formulas. The soundness proof allows us to establish that SQHT= is a (...) conservative extension of the logic of weak excluded middle with respect to sequents without positive occurrences of implication. The completeness proof uses a non-closed branch of a proof search tree. The interplay between rules for pushing negation inside and truth in the “there” world of the resulting Kripke model can be of independent interest. We prove that existence is definable in terms of remaining connectives. (shrink)

This paper presents rules in sequent calculus for a binary quantifier I to formalise definite descriptions: Ix[F, G] means ‘The F is G’. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of I. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a (...) term forming operator. In the final section rules for I for negative free and classical logic are also mentioned. (shrink)