What the Tortoise Said to Achilles: Lewis Carroll’s Paradox in Terms of Hilbert Arithmetic

Lewis Carroll, both logician and writer, suggested a logical paradox containing furthermore two connotations (connotations or metaphors are inherent in literature rather than in mathematics or logics). The paradox itself refers to implication demonstrating that an intermediate implication can be always inserted in an implication therefore postponing its ultimate conclusion for the next step and those insertions can be iteratively and indefinitely added ad lib, as if ad infinitum. Both connotations clear up links due to the shared formal structure with other well-known mathematical observations: (1) the paradox of Achilles and the Turtle; (2) the transitivity of the relation of equality. Analogically to (1), one can juxtapose the paradox of the Liar (for Lewis Carroll’s paradox) and that of the arrow (for “Achilles and the Turtle”), i.e. a logical paradox, on the one hand, and an aporia of motion, on the other hand, suggesting a shared formal structure of both, which can be called “ontological”, on which basis “motion” studied by physics and “conclusion” studied by logic can be unified being able to bridge logic and physics philosophically in a Hegelian manner: even more, the bridge can be continued to mathematics in virtue of (2), which forces the equality (for its property of transitivity) of any two quantities to be postponed analogically ad lib and ad infinitum. The paper shows that Hilbert arithmetic underlies naturally Lewis Carroll’s paradox admitting at least three interpretations linked to each other by it: mathematical, physical and logical. Thus, it can be considered as both generalization and solution of his paradox therefore naturally unifying the completeness of quantum mechanics (i.e. the absence of hidden variables) and eventual completeness of mathematics as the same and isomorphic to the completeness of propositional logic in relation to set theory as a first-order logic (in the sense of Gödel (1930)’s completeness theorems).

What the Tortoise Said to Achilles: Lewis Carroll’s paradox in terms of Hilbert arithmetic

Lewis Carroll, both logician and writer, suggested a logical paradox containing furthermore two connotations (connotations or metaphors are inherent in literature rather than in mathematics or logics). The paradox itself refers to implication demonstrating that an intermediate implication can be always inserted in an implication therefore postponing its ultimate conclusion for the next step and those insertions can be iteratively and indefinitely added ad lib, as if ad infinitum. Both connotations clear up links due to the shared formal structure with other well-known mathematical observations: (1) the paradox of Achilles and the Turtle; (2) the transitivity of the relation of equality. Analogically to (1), one can juxtapose the paradox of the Liar (for Lewis Carroll’s paradox) and that of the arrow (for “Achillesand the Turtle”), i.e. a logical paradox, on the one hand, and an aporia of motion, on the other hand, suggesting a shared formal structure of both, which can be called “ontological”, on which basis “motion” studied by physics and “conclusion” studied by logic can be unified being able to bridge logic and physics philosophically in a Hegelian manner: even more, the bridge can be continued to mathematics in virtue of (2), which forces the equality (for its property of transitivity) of any two quantities to be postponed analogically ad lib and ad infinitum. The paper shows that Hilbert arithmetic underlies naturally Lewis Carroll’s paradox admitting at least three interpretations linked to each other by it: mathematical, physical and logical. Thus, it can be considered as both generalization and solution of his paradox thereforenaturally unifying the completeness of quantum mechanics (i.e. the absence of hidden variables) and eventual completeness of mathematics as the same and isomorphic to the completeness of propositional logic in relation to set theory as a first-order logic (in the sense of Gödel (1930)’s completeness theorems).

S5-Style Non-Standard Modalities in a Hypersequent Framework

The aim of the paper is to present some non-standard modalities (such as non-contingency, contingency, essence and accident) based on S5-models in a framework of cut-free hypersequent calculi. We also study negated modalities, i.e. negated necessity and negated possibility, which produce paraconsistent and paracomplete negations respectively. As a basis for our calculi, we use Restall's cut-free hypersequent calculus for S5. We modify its rules for the above-mentioned modalities and prove strong soundness and completeness theorems by a Hintikka-style argument. As a consequence, we obtain a cut admissibility theorem. Finally, we present a constructive syntactic proof of cut elimination theorem.

Ternary Relational Semantics for the Variants of BN4 and E4 which Contain Routley and Meyer's Logic B

Six hopefully interesting variants of the logics BN4 and E4 – which can be considered as the 4-valued logics of the relevant conditional and (relevant) entailment, respectively – were previously developed in the literature. All these systems are related to the family of relevant logics and contain Routley and Meyer's basic logic B, which is well-known to be specifically associated with the ternary relational semantics. The aim of this paper is to develop reduced general Routley-Meyer semantics for them. Strong soundness and completeness theorems are proved for each one of the logics.

Model Theory in a Paraconsistent Environment

The purpose of this thesis is to develop a paraconsistent Model Theory. The basis for such a theory was launched by Walter Carnielli, Marcelo Esteban Coniglio, Rodrigo Podiack, and Tarcísio Rodrigues in the article ‘On the Way to a Wider Model Theory: Completeness Theorems for First-Order Logics of Formal Inconsistency’ [The Review of Symbolic Logic, vol. 7 (2014)].Naturally, a complete theory cannot be fully developed in a single work. Indeed, the goal of this work is to show that a paraconsistent Model Theory is a sound and worthy possibility. The pursuit of this goal is divided in three tasks: The first one is to give the theory a philosophical meaning. The second one is to transpose as many results from the classical theory to the new one as possible. The third one is to show an application of the theory to practical science.The response to the first task is a Paraconsistent Reasoning System. The start point is that paraconsistency is an epistemological concept. The pursuit of a deeper understanding of the phenomenon of paraconsistency from this point of view leads to a reasoning system based on the Logics of Formal Inconsistency. Models are regarded as states of knowledge and the concept of isomorphism is reformulated so as to give raise to a new concept that preserves a portion of the whole knowledge of each state. Based on this, a notion of refinement is created which may occur from inside or from outside the state.In order to respond to the second task, two important classical results, namely the Omitting Types Theorem and Craig’s Interpolation Theorem are shown to hold in the new system and it is also shown that, if classical results in general are to hold in a paraconsistent system, then such a system should be in essence how it was developed here.Finally, the response to the third task is a proposal of what a Paraconsistent Logic Programming may be. For that, the basis for a paraconsistent PROLOG is settled in the light of the ideas developed so far.Abstract prepared by Bruno Costa Coscarelli.E-mail: [email protected]: http://repositorio.unicamp.br/jspui/handle/REPOSIP/331697

Completeness theorems for first-order logic analysed in constructive type theory

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak K̋nig’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative completeness theorems of real numbers. These theorems include the Dedekind fundamental theorem, Supremum theorem, Monotone convergence theorem, Nested interval theorem, Finite cover theorem, Accumulation point theorem, Sequential compactness theorem, and Cauchy completeness theorem. We formalize the real number theory strictly following Landau’s Foundations of Analysis where the Dedekind fundamental theorem can be proved. We extend this system and complete the related notions and properties for finiteness and sequence. We prove these theorems in turn from Dedekind fundamental theorem, and finally prove the Dedekind fundamental theorem by the Cauchy completeness theorem. The full details of formal proof are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. This work can lay the foundation for many applications, especially in calculus and topology.