Hilbert arithmetic in a wide sense, including Hilbert arithmetic in a narrow sense consisting by two dual and anti-isometric Peano arithmetics, on the one hand, and the qubit Hilbert space (originating for the standard separable complex Hilbert space of quantum mechanics), on the other hand, allows for an arithmetic version of Gentzen’s cut elimination and quantum measurement to be described uniformy as two processes occurring accordingly in those two branches. A philosophical reflection also (...) justifying that unity by quantum neo-Pythagoreanism links it to the opposition of propositional logic, to which Gentzen’s cut rule refers immediately, on the one hand, and the linguistic and mathematical theory of metaphor therefore sharing the same structure borrowed from Hilbert arithmetic in a wide sense. An example by hermeneutical circle modeled as a dual pair of a syllogism (accomplishable also by a Turing machine) and a relevant metaphor (being a formal and logical mistake and thus fundamentally inaccessible to any Turing machine) visualizes human understanding corresponding also to Gentzen’s cut elimination and the Gödel dichotomy about the relation of arithmetic to set theory: either incompleteness or contradiction. The metaphor as the complementing “half” of any understanding of hermeneutical circle is what allows for that Gödel-like incompleteness to be overcome in human thought. (shrink)

The paper is the final, fifth part of a series of studies introducing the new conceptions of “Hilbert mathematics” and “ontomathematics”. The specific subject of the present investigation is the proper philosophical sense of both, including philosophy of mathematics and philosophy of physics not less than the traditional “first philosophy” (as far as ontomathematics is a conservative generalization of ontology as well as of Heidegger’s “fundamental ontology” though in a sense) and history of philosophy (deepening Heidegger’s destruction of it (...) from the pre-Socratics to the Pythagoreans). Husserl’s phenomenology and Heidegger’s derivative “fundamental ontology” as well as his later doctrine after the “turn” are the starting point of the research as established and well known approaches relative to the newly introduced conception of ontomathematics, even more so that Husserl himself started criticizing his “Philosophy of arithmetic” as too naturalistic and psychological turning to “Logical investigations” and the foundations of phenomenology. Heidegger’s “Aletheia” is also interpreted ontomathematically: as a relation of locality and nonlocality, respectively as a motion from nonlocality to locality if both are physically considered. Aristotle’s ontological revision of Plato’s doctrine is “destructed” further from the pre-Socratics' “Logos” or Heideger’s “Language” (after the “turn”) to the Pythagoreans “Numbers” or “Arithmetics” as an inherent and fundamental philosophical doctrine. Then, a leap to contemporary physics elucidates the essence of ontomathematics overcoming the Cartesian abyss inherited from Plato’s opposition of “ideas” versus “things”, and now unifying physics and mathematics, particularly allowing for the “creation from nothing” instead of the quasi-scientific myth of the “Big Bang”. Furthermore, ontomathematics needs another interpretation of arithmetic, propositional logic and set theory in the foundations of mathematics, where the latter two ones are both identified with Boolean algebra, and the former is considered to be a “half of Boolean algebra” in the exact meaning to be equated to it after doubling by a dual anti-isometric counterpart of Peano arithmetic. That unified algebraic realization of the foundations of mathematics is related to Hilbert mathematics in both “narrow and wide senses” where the latter is isomorphic to the qubit Hilbert space, thus underlying all the physical world by the newly introduced substance of quantum information being physically dimensionless and generalizing classical information measured in bits. The substance of information, whether classical or quantum, visualizes the way of the unification of physics and mathematics by merging their foundations in Hilbert arithmetic and Hilbert mathematics: thus how ontomathetics is a “first philosophy”. The relation of ontomathematics to the Socratic “human problematics”, furthermore being fundamental for Western philosophy in Modernity, is discussed. Ontomathematics implies its “substitution” by abstract information (or by “subjectless choice” relevant to it), thus “obliterating the human outline on the ocean beach sand” (by Michel Foucault’s metaphor). A reflection back from the viewpoint of mathematic to Western philosophy as the philosophy of locality ends the study. (shrink)

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). (shrink)

Compound propositions which can successfully be defended in a quantumdialogue independent of the elementary propositions contained in it, must have this property also independent of the mutual elementary commensur-abilities. On the other hand, formal commensurabilities must be taken into account. Therefore, for propositions which can be proved by P, irrespective of both the elementary propositions and of the elementary commensur-abilities, there exists a formal strategy of success. The totality of propositions with a formal strategy of success in a quantum (...) dialogue form the effective quantum logic. The propositions of the effective quantum logic can be derived from a calculus Q eff which is — on the other hand — equivalent to a lattice L qi.Propositions about measuring results are above all time dependent propositions A(S;t). In a dialogue, different partial propositions will have in general different time values. If one can (accidentally) win a material dialogue, this dialogue can be related to a single time value. For the propositions of the effective quantum logic there exist formal strategies of success, independent of the elementary propositions contained in it. All partial propositions appearing in the dialogue are formally commensurable. Therefore the propositions of effective quantum logic which can be proved by formal dialogues can always be related to a single time. They present a description of the system S considered in which all partial propositions can be related jointly to the state of S.Therefore in the effective quantum logic we have — in the limit of equal time values — a situation which corresponds conceptually to the description of the system (S; ψ) in Hilbert space. Consequently, one would expect that also the lattice L qi — except from the tertium non datur 8 — agrees with the lattice L q of subspaces of Hilbert space. It has been shown that these lattices are in fact isomorphic. (shrink)

A well established technique toward developing the proof theory of a Hilbert-style modal logic is to introduce a Gentzen-style equivalent (a Gentzenisation), then develop the proof theory of the latter, and finally transfer the metatheoretical results to the original logic (e.g., [1, 6, 8, 18, 10, 12]). In the first-order modal case, on one hand we know that the Gentzenisation of the straightforward first-order extension of GL, the logic QGL, admits no cut elimination (if the rule is included as (...) primitive; or, if not included, then the rule is not admissible [1]). On the other hand the (cut-free) Gentzenisations of the first-order modal logics M3 and ML3 of [10, 12] do have cut as an admissible rule. The syntactic cut admissibility proof given in [18] for the Gentzenisation of the propositional provability logic GL is extremely complex, and it was the basis of the proofs of cut admissibility of the Gentzenisations of M3 and ML3, where the presence of quantifiers and quantifier rules added to the complexity and length of the proof. A recent proof of cut admissibility in a cut-free Gentzenisation of GL is given in [5] and is quite short and easy to read. We adapt it here to revisit the proofs for the cases of M3 and ML3, resulting to similarly short and easy to read proofs, only slightly complicated by the presence of quantification and its relevant rules. (shrink)

This paper shows that the non-Boolean logic of quantum measurements is more naturally represented by a relatively new 4-operation system of Boolean fractions—conditional events—than by the standard representation using Hilbert Space. After the requirements of quantum mechanics and the properties of conditional event algebra are introduced, the quantum concepts of orthogonality, completeness, simultaneous verifiability, logical operations, and deductions are expressed in terms of conditional events thereby demonstrating the adequacy and efficacy of this formulation. Since conditional event (...) algebra is nearly Boolean and consists merely of ordered pairs of standard events or propositions, quantum events and the so-called “superpositions” of states need not be mysterious, and are here fully explicated. Conditional event algebra nicely explains these non-standard “superpositions” of quantum states as conjunctions or disjunctions of conditional events, Boolean fractions, but does not address the so-called “entanglement phenomena” of quantum mechanics, which remain physically mysterious. Nevertheless, separating the latter phenomena from superposition issues adds clarity to the interpretation of quantum entanglement, the phenomenon of influence propagated at faster than light speeds. With such treacherous possibilities present in all quantum situations, an observer has every reason to be completely explicit about the environmental–instrumental configuration, the conditions present when attempting quantum measurements. Conditional event algebra allows such explication without the physical and algebraic remoteness of Hilbert space. (shrink)

This paper studies a combined system of intuitionistic and classical propositional logic from proof-theoretic viewpoints. Based on the semantic treatment of Humberstone (J Philos Log 8:171–196, 1979) and del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996), a sequent calculus $$\textsf{G}(\textbf{C}+\textbf{J})$$ is proposed. An approximate idea of obtaining $$\textsf{G}(\textbf{C}+\textbf{J})$$ is adding rules for classical implication on top of the intuitionistic multi-succedent sequent calculus by Maehara (Nagoya Math J 7:45–64, 1954). However, in the semantic treatment, some formulas do (...) not satisfy heredity, which leads to the necessity of a restriction on the right rule for intuitionistic implication to keep the soundness of the calculus. The calculus $$\textsf{G}(\textbf{C}+\textbf{J})$$ enjoys cut elimination and Craig interpolation, whose detailed proofs are described in this paper. Cut elimination enables us to show the decidability of this combination both directly and syntactically. This paper also employs a canonical model argument to establish the strong completeness of Hilbert system $$\mathbf {C+J}$$ proposed by del Cerro and Herzig (Frontiers of combining systems: FroCoS, Springer, 1996). (shrink)

This paper introduces sequent systems for Visser's two propositional logics: Basic Propositional Logic (BPL) and Formal Propositional Logic (FPL). It is shown through semantical completeness that the cut rule is admissible in each system. The relationships with Hilbert-style axiomatizations and with other sequent formulations are discussed. The cut-elimination theorems are also demonstrated by syntactical methods.

In Schwichtenberg, Schwichtenberg fine-tuned Tait’s technique so as to provide a simplified version of Gentzen’s original cut-elimination procedure for first-order classical logic. In this note we show that, limited to the case of classical propositional logic, the Tait–Schwichtenberg algorithm allows for a further simplification. The procedure offered here is implemented on Kleene’s sequent system G4. The specific formulation of the logical rules for G4 allows us to provide bounds on the height of cut-free proofs just in terms of the (...) logical complexity of their end-sequent. (shrink)

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic (...) fixed point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

We analyse the structure of propositional proofs in the sequent calculus focusing on the well-known procedures of Interpolation and Cut Elimination. We are motivated in part by the desire to understand why a tautology might be ‘hard to prove’. Given a proof we associate to it a logical graph tracing the flow of formulas in it . We show some general facts about logical graphs such as acyclicity of cut-free proofs and acyclicity of contraction-free proofs , and we give (...) a proof of a strengthened version of the Craig Interpolation Theorem based on flows of formulas. We show that tautologies having minimal interpolants of non-linear size must have proofs with certain precise structural properties. We then show that given a proof Π and a cut-free form Π′ associated to it , certain subgraphs of Π′ which are logical graphs correspond to subgraphs of Π which are logical graphs for the same sequent. This locality property of cut elimination leads to new results on the complexity of interpolants, which cannot follow from the known constructions proving the Craig Interpolation Theorem. (shrink)

The previous Part I of the paper discusses the option of the Gödel incompleteness statement (1931: whether “Satz VI” or “Satz X”) to be an axiom due to the pair of the axiom of induction in arithmetic and the axiom of infinity in set theory after interpreting them as logical negations to each other. The present Part II considers the previous Gödel’s paper (1930) (and more precisely, the negation of “Satz VII”, or “the completeness theorem”) as a necessary condition for (...) granting the Gödel incompleteness statement to be a theorem just as the statement itself, to be an axiom. Then, the “completeness paper” can be interpreted as relevant to Hilbert mathematics, according to which mathematics and reality as well as arithmetic and set theory are rather entangled or complementary rather than mathematics to obey reality able only to create models of the latter. According to that, both papers (1930; 1931) can be seen as advocating Russell’s logicism or the intensional propositional logic versus both extensional arithmetic and set theory. Reconstructing history of philosophy, Aristotle’s logic and doctrine can be opposed to those of Plato or the pre-Socratic schools as establishing ontology or intensionality versus extensionality. Husserl’s phenomenology can be analogically realized including and particularly as philosophy of mathematics. One can identify propositional logic and set theory by virtue of Gödel’s completeness theorem (1930: “Satz VII”) and even both and arithmetic in the sense of the “compactness theorem” (1930: “Satz X”) therefore opposing the latter to the “incompleteness paper” (1931). An approach identifying homomorphically propositional logic and set theory as the same structure of Boolean algebra, and arithmetic as the “half” of it in a rigorous construction involving information and its unit of a bit. Propositional logic and set theory are correspondingly identified as the shared zero-order logic of the class of all first-order logics and the class at issue correspondingly. Then, quantum mechanics does not need any quantum logics, but only the relation of propositional logic, set theory, arithmetic, and information: rather a change of the attitude into more mathematical, philosophical, and speculative than physical, empirical and experimental. Hilbert’s epsilon calculus can be situated in the same framework of the relation of propositional logic and the class of all mathematical theories. The horizon of Part III investigating Hilbert mathematics (i.e. according to the Pythagorean viewpoint about the world as mathematical) versus Gödel mathematics (i.e. the usual understanding of mathematics as all mathematical models of the world external to it) is outlined. (shrink)

It is shown that every displayable propositional logic enjoys strong cut-elimination. This result strengthens Belnap's general cut-elimination theorem for Display Logic.

This paper uses a non-distributive system of Boolean fractions (a|b), where a and b are 2-valued propositions or events, to express uncertain conditional propositions and conditional events. These Boolean fractions, 'a if b' or 'a given b', ordered pairs of events, which did not exist for the founders of quantum logic, can better represent uncertain conditional information just as integer fractions can better represent partial distances on a number line. Since the indeterminacy of some pairs of quantum events (...) is due to the mutual inconsistency of their experimental conditions, this algebra of conditionals can express indeterminacy. In fact, this system is able to express the crucial quantum concepts of orthogonality, simultaneous verifiability, compatibility, and the superposition of quantum events, all without resorting to Hilbert space. A conditional (a|b) is said to be "inapplicable" (or "undefined") in those instances or models for which b is false. Otherwise the conditional takes the truth-value of proposition a. Thus the system is technically 3-valued, but the 3rd value has nothing to do with a state of ignorance, nor to some half-truth. People already routinely put statements into three categories: true, false, or inapplicable. As such, this system applies to macroscopic as well as microscopic events. Two conditional propositions turn out to be simultaneously verifiable just in case the truth of one implies the applicability of the other. Furthermore, two conditional propositions (a|b) and (c|d) reside in a common Boolean sub-algebra of the non-distributive system of conditional propositions just in case b = d, their conditions are equivalent. Since all aspects of quantum mechanics can be represented with this near classical logic, there is no need to adopt Hilbert space logic as ordinary logic, just a need perhaps to adopt propositional fractions to do logic, just as we long ago adopted integer fractions to do arithmetic. The algebra of Boolean fractions is a natural, near-Boolean extension of Boolean algebra adequate to express quantum logic. While this paper explains one group of quantum anomalies, it nevertheless leaves no less mysterious the 'influence-at-a-distance', quantum entanglement phenomena. A quantum realist must still embrace non-local influences to hold that "hidden variables" are the measured properties of particles. But that seems easier than imaging wave-particle duality and instant collapse, as offered by proponents of the standard interpretation of quantum mechanics. (shrink)

We develop a Gentzen-style proof theory for super-Belnap logics, expanding on an approach initiated by Pynko. We show that just like substructural logics may be understood proof-theoretically as logics which relax the structural rules of classical logic but keep its logical rules as well as the rules of Identity and Cut, super-Belnap logics may be seen as logics which relax Identity and Cut but keep the logical rules as well as the structural rules of classical logic. A generalization of the (...) cut elimination theorem for classical propositional logic is then proved and used to establish interpolation for various super-Belnap logics. In particular, we obtain an alternative syntactic proof of a refinement of the Craig interpolation theorem for classical propositional logic discovered recently by Milne. (shrink)

The new logic of partitions is dual to the usual Boolean logic of subsets (usually presented only in the special case of the logic of propositions) in the sense that partitions and subsets are category-theoretic duals. The new information measure of logical entropy is the normalized quantitative version of partitions. The new approach to interpreting quantum mechanics (QM) is showing that the mathematics (not the physics) of QM is the linearized Hilbert space version of the mathematics of partitions. (...) Or, putting it the other way around, the math of partitions is a skeletal version of the math of QM. The key concepts throughout this progression from logic, to logical information, to quantum theory are distinctions versus indistinctions, definiteness versus indefiniteness, or distinguishability versus indistinguishability. The distinctions of a partition are the ordered pairs of elements from the underlying set that are in different blocks of the partition and logical entropy is defined (initially) as the normalized number of distinctions. The cognate notions of definiteness and distinguishability run throughout the math of QM, e.g., in the key non-classical notion of superposition (= ontic indefiniteness) and in the Feynman rules for adding amplitudes (indistinguishable alternatives) versus adding probabilities (distinguishable alternatives). (shrink)

We provide a constructive, direct, and simple proof of the completeness of the cut-free part of the hypersequential calculus for G¨odel logic (thereby proving both completeness of the calculus for its standard semantics, and the admissibility of the cut rule in the full calculus). We then extend the results and proofs to derivations from assumptions, showing that such derivations can be confined to those in which cuts are made only on formulas which occur in the assumptions.

In this article, a cut-free system TLMω1 for infinitary propositional modal logic is proposed which is complete with respect to the class of all Kripke frames.The system TLMω1 is a kind of Gentzen style sequent calculus, but a sequent of TLMω1 is defined as a finite tree of sequents in a standard sense. We prove the cut-elimination theorem for TLMω1 via its Kripke completeness.

We provide a non-Gentzen, though fully syntactical, cut-elimination algorithm for classical propositional logic. The designed procedure is implemented on $$\textsf{GS4}$$ GS 4, the one-sided version of Kleene’s sequent system $$\textsf{G4}$$ G 4. The algorithm here proposed proves to be more ‘dexterous’ than other, more traditional, Gentzen-style techniques as the size of proofs decreases at each step of reduction. As a corollary result, we show that analyticity always guarantees minimality of the size of $$\textsf{GS4}$$ GS 4 -proofs.

In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.

In this paper we discuss sequent calculi for the propositional fragment of the logic of HYPE. The logic of HYPE was recently suggested by Leitgeb as a logic for hyperintensional contexts. On the one hand we introduce a simple \-system employing rules of contraposition. On the other hand we present a \-system with an admissible rule of contraposition. Both systems are equivalent as well as sound and complete proof-system of HYPE. In order to provide a cut-elimination procedure, we expand (...) the calculus by connections as introduced in Kashima and Shimura. (shrink)

In this paper we discuss sequent calculi for the propositional fragment of the logic of HYPE. The logic of HYPE was recently suggested by Leitgeb as a logic for hyperintensional contexts. On the one hand we introduce a simple \-system employing rules of contraposition. On the other hand we present a \-system with an admissible rule of contraposition. Both systems are equivalent as well as sound and complete proof-system of HYPE. In order to provide a cut-elimination procedure, we expand (...) the calculus by connections as introduced in Kashima and Shimura. (shrink)

Context-dependent rules are an obstacle to cut elimination. Turning to a generalised sequent style formulation using deep inferences is helpful, and for the calculus presented here it is essential. Cut elimination is shown for a substructural, multiplicative, pure propositional calculus. Moreover we consider the extra problems induced by non-logical axioms and extend the results to additive connectives and quantifiers.

The previous two parts of the paper demonstrate that the interpretation of Fermat’s last theorem (FLT) in Hilbert arithmetic meant both in a narrow sense and in a wide sense can suggest a proof by induction in Part I and by means of the Kochen - Specker theorem in Part II. The same interpretation can serve also for a proof FLT based on Gleason’s theorem and partly similar to that in Part II. The concept of (probabilistic) measure of a (...) subspace of Hilbert space and especially its uniqueness can be unambiguously linked to that of partial algebra or incommensurability, or interpreted as a relation of the two dual branches of Hilbert arithmetic in a wide sense. The investigation of the last relation allows for FLT and Gleason’s theorem to be equated in a sense, as two dual counterparts, and the former to be inferred from the latter, as well as vice versa under an additional condition relevant to the Gödel incompleteness of arithmetic to set theory. The qubit Hilbert space itself in turn can be interpreted by the unity of FLT and Gleason’s theorem. The proof of such a fundamental result in number theory as FLT by means of Hilbert arithmetic in a wide sense can be generalized to an idea about “quantum number theory”. It is able to research mathematically the origin of Peano arithmetic from Hilbert arithmetic by mediation of the “nonstandard bijection” and its two dual branches inherently linking it to information theory. Then, infinitesimal analysis and its revolutionary application to physics can be also re-realized in that wider context, for example, as an exploration of the way for physical quantity of time (respectively, for time derivative in any temporal process considered in physics) to appear at all. Finally, the result admits a philosophical reflection of how any hierarchy arises or changes itself only thanks to its dual and idempotent counterpart. (shrink)

Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula property, in which exactly one occurrence of a connective is introduced in the conclusion, and no other occurrence of any connective is mentioned anywhere else. In this paper we considerably generalize the notion of a “canonical system” to first-order languages and beyond. We extend the Propositional coherence criterion for the non-triviality of such systems to (...) rules with unary quantifiers and show that it remains constructive. Then we provide semantics for such canonical systems using 2-valued non-deterministic matrices extended to languages with quantifiers, and prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix. (shrink)

Two cut-free sequent calculi which are conservative extensions of Visser's Formal Propositional Logic are introduced. These satisfy a kind of subformula property and by this property the interpolation theorem for FPL are proved. These are analogies to Aghaei-Ardeshir's calculi for Visser's Basic Propositional Logic.

The paper continues the consideration of Hilbert mathematics to mathematics itself as an additional “dimension” allowing for the most difficult and fundamental problems to be attacked in a new general and universal way shareable between all of them. That dimension consists in the parameter of the “distance between finiteness and infinity”, particularly able to interpret standard mathematics as a particular case, the basis of which are arithmetic, set theory and propositional logic: that is as a special “flat” case (...) of Hilbert mathematics. The following four essential problems are considered for the idea to be elucidated: Fermat’s last theorem proved by Andrew Wiles; Poincaré’s conjecture proved by Grigori Perelman and the only resolved from the seven Millennium problems offered by the Clay Mathematics Institute (CMI); the four-color theorem proved “machine-likely” by enumerating all cases and the crucial software assistance; the Yang-Mills existence and mass gap problem also suggested by CMI and yet unresolved. They are intentionally chosen to belong to quite different mathematical areas (number theory, topology, mathematical physics) just to demonstrate the power of the approach able to unite and even unify them from the viewpoint of Hilbert mathematics. Also, specific ideas relevant to each of them are considered. Fermat’s last theorem is shown as a Gödel insoluble statement by means of Yablo’s paradox. Thus, Wiles’s proof as a corollary from the modularity theorem and thus needing both arithmetic and set theory involves necessarily an inverse Grothendieck universe. On the contrary, its proof in “Fermat arithmetic” introduced by “epoché to infinity” (following the pattern of Husserl’s original “epoché to reality”) can be suggested by Hilbert arithmetic relevant to Hilbert mathematics, the mediation of which can be removed in the final analysis as a “Wittgenstein ladder”. Poincaré’s conjecture can be reinterpreted physically by Minkowski space and thus reduced to the “nonstandard homeomorphism” of a bit of information mathematically. Perelman’s proof can be accordingly reinterpreted. However, it is valid in Gödel (or Gödelian) mathematics, but not in Hilbert mathematics in general, where the question of whether it holds remains open. The four-color theorem can be also deduced from the nonstandard homeomorphism at issue, but the available proof by enumerating a finite set of all possible cases is more general and relevant to Hilbert mathematics as well, therefore being an indirect argument in favor of the validity of Poincaré’s conjecture in Hilbert mathematics. The Yang-Mills existence and mass gap problem furthermore suggests the most general viewpoint to the relation of Hilbert and Gödel mathematics justifying the qubit Hilbert space as the dual counterpart of Hilbert arithmetic in a narrow sense, in turn being inferable from Hilbert arithmetic in a wide sense. The conjecture that many if not almost all great problems in contemporary mathematics rely on (or at least relate to) the Gödel incompleteness is suggested. It implies that Hilbert mathematics is the natural medium for their discussion or eventual solutions. (shrink)

The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we (...) notice that cut remains eliminable when suitable arithmetical axioms are added to the system. Finally, we establish a direct link between cut-free derivability in infinitary formulations of the systems considered and fixed-point semantics. Noticeably, unlike what happens with other background logics, such links are established without imposing any restriction to the premisses of the truth rules. (shrink)

Gravitation is interpreted to be an “ontomathematical” force or interaction rather than an only physical one. That approach restores Newton’s original design of universal gravitation in the framework of “The Mathematical Principles of Natural Philosophy”, which allows for Einstein’s special and general relativity to be also reinterpreted ontomathematically. The entanglement theory of quantum gravitation is inherently involved also ontomathematically by virtue of the consideration of the qubit Hilbert space after entanglement as the Fourier counterpart of pseudo-Riemannian space. Gravitation (...) can be also interpreted as purely mathematical or logical “force” or “interaction” as a corollary from its ontomathematical (rather than physical) realization. The ontomathematical approach to gravitation is implicit in general relativity equating it to operators in pseudo-Riemannian space obeying the Einstein field equation and also well-known by the “geometrization of physics”. Quantum mechanics shares the same by the separable complex Hilbert space and defining “physical quantity” by the Hermitian operators on it. One can interpret special Minkowski space involved by special relativity and the qubit Hilbert space of quantum information as Fourier counterparts immediately noticing that general relativity means gravitation as the Fourier counterpart of non-Hermitian operators implying non-unitarity and the violation of energy conservation and thus destroying Pauli’s particle paradigm. Since the Standard model obeys it, this explains the impossibility of “quantum gravitation” in any framework conservatively generalizing the Standard model so that it would include gravitation along with electromagnetic, weak, and strong interactions. Einstein’s geometrization of gravitation can be continued into a purely mathematical theory of it following Euclid’s realization for geometry to be exhaustively built in a deductive and axiomatic way as well as Riemann’s parametrization of all the class of Euclidean and non-Euclidean geometries by “space curvature”, then being generalized to Minkowski space as the operators on pseudo-Riemannian space as the Einstein field equation means gravitation. The transition from mathematical gravitation to logical one can rely on the historical lesson of the pair of Lobachevski’s and Riemann’s approaches now “reversely”, i.e., from the latter to the former. Logical gravitation is linkable to Hegel’s dialectical logic and ontological dialectics abandoning their interpretations as a new zero logic substituting classical propionyl logic. The approach of ontomathematics generalizing that of ontology, traceable even to Aristotle’s reformation of Plato’s doctrine, needs Hegel’s doctrine to be formalized as a first-order logic naturally containing Boolean algebra, isomorphic to both classical propositional logic and set theory being the class of all first-order logics, as a sub-logic along with Peano arithmetic as another sub-logic. The first-order logic at issue is called Hilbert arithmetic and elaborated in detail in other papers. It allows for both self-foundation of mathematics to be internally proved as complete and furthermore, quantum mechanics reinterpreted as quantum information to be included by the qubit Hilbert space interpretable in turn as a dual and physical counterpart of Hilbert arithmetic in a narrow sense, that is, both counterparts constitute Hilbert arithmetic in a wide sense, being mathematical and physical simultaneously and thus overcoming the Cartesian dualism of “body” gapped from “mind” by an abyss. Then, the proper philosophical interpretation of gravitation to be the fundamental ontomathematical force or interaction overcomes the ridiculous belief of the Big Bang wrongly alleged to be a scientific theory. Ontomathematical gravitation suggests an omnipresent and omnitemporal medium of “God’s” creation “ex nihilo” following only the natural necessity of quantum-information conservation particularly and locally manifested as energy conservation. (shrink)

Sufficient conditions for first-order-based sequent calculi to admit cut elimination by a Schütte–Tait style cut elimination proof are established. The worst case complexity of the cut elimination is analysed. The obtained upper bound is parameterized by a quantity related to the calculus. The conditions are general enough to be satisfied by a wide class of sequent calculi encompassing, among others, some sequent calculi presentations for the first order and the propositional versions of classical and intuitionistic logic, classical and intuitionistic (...) modal logic S4, and classical and intuitionistic linear logic and some of its fragments. Moreover the conditions are such that there is an algorithm for checking if they are satisfied by a sequent calculus. (shrink)

A common misconception among logicians is to think that intuitionism is necessarily tied-up with single conclusion calculi. Single conclusion calculi can be used to model intuitionism and they are convenient, but by no means are they necessary. This has been shown by such influential textbook authors as Kleene, Takeuti and Dummett, to cite only three. If single conclusions are not necessary, how do we guarantee that only intuitionistic derivations are allowed? Traditionally one insists on restrictions on particular rules: implication right, (...) negation right and universal quantification right are required to be single conclusion rules. In this note we show that instead of a cardinality restriction such as one-conclusion-only, we can use a notion of dependency between formulae to enforce the constructive character of derivations. The system we obtain, called FIL for full intuitionistic logic, satisfies basic properties such as soundness, completeness and cut elimination. We present two motivating applications of FIL and discuss some future work. (shrink)

The paper addresses Leon Hen.kin's proposition as a " lighthouse", which can elucidate a vast territory of knowledge uniformly: logic, set theory, information theory, and quantum mechanics: Two strategies to infinity are equally relevant for it is as universal and t hus complete as open and thus incomplete. Henkin's, Godel's, Robert Jeroslow's, and Hartley Rogers' proposition are reformulated so that both completeness and incompleteness to be unified and thus reduced as a joint property of infinity and of all infinite (...) sets. However, only Henkin's proposition equivalent to an internal position to infinity is consistent . This can be retraced back to set theory and its axioms, where that of choice is a key. Quantum mechanics is forced to introduce infinity implicitly by Hilbert space, on which is founded its formalism. One can demonstrate that some essential properties of quantum information, entanglement, and quantum computer originate directly from infinity once it is involved in quantum mechanics. Thus, these phenomena can be elucidated as both complete and incomplete, after which choice is the border between them. A special kind of invariance to the axiom of choice shared by quantum mechanics is discussed to be involved that border between the completeness and incompleteness of infinity in a consistent way. The so-called paradox of Albert Einstein, Boris Podolsky, and Nathan Rosen is interpreted entirely in the same terms only of set theory. Quantum computer can demonstrate especially clearly the privilege of the internal position, or " observer'' , or "user" to infinity implied by Henkin's proposition as the only consistent ones as to infinity. An essential area of contemporary knowledge may be synthesized from a single viewpoint. (shrink)

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.

By quoting extensively from unpublished letters written by John von Neumann to Garret Birkhoff during the preparatory phase (in 1935) of their ground-breaking 1936 paper that established quantum logic, the main steps in the thought process leading to the 1936 Birkhoff–von Neumann paper are reconstructed. The reconstruction makes it clear why Birkhoff and von Neumann rejected the notion of quantum logic as the projection lattice of an infinite dimensional complex Hilbert space and why they postulated in their (...) 1936 paper that the quantum propositional system should be isomorphic to an abstract projective geometry. Looking at the paper now I see, that I forgot to say this, which should be said somewhere in the first §: That while common logics did apply to quantum mechanics, if the notion of simultaneous measurability is introduced as an auxiliary notion, we wished to construct a logical system, which applies directly to quantum mechanics – without any extraneous secondary notions like simultaneous measurability. And in order to have such a consequent, one-piece system of logics, we must change the classical class calculus of logics. (J. von Neumann to G. Birkhoff, November 21, 1935). (shrink)

Following Birkhoff and von Neumann, quantum logic has traditionally been based on the lattice of closed linear subspaces of some Hilbert space, or, more generally, on the lattice of projections in a von Neumann algebra A. Unfortunately, the logical interpretation of these lattices is impaired by their nondistributivity and by various other problems. We show that a possible resolution of these difficulties, suggested by the ideas of Bohr, emerges if instead of single projections one considers elementary propositions to (...) be families of projections indexed by a partially ordered set \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}(A)}$$\end{document} of appropriate commutative subalgebras of A. In fact, to achieve both maximal generality and ease of use within topos theory, we assume that A is a so-called Rickart C*-algebra and that \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}(A)}$$\end{document} consists of all unital commutative Rickart C*-subalgebras of A. Such families of projections form a Heyting algebra in a natural way, so that the associated propositional logic is intuitionistic: distributivity is recovered at the expense of the law of the excluded middle. Subsequently, generalizing an earlier computation for n × n matrices, we prove that the Heyting algebra thus associated to A arises as a basis for the internal Gelfand spectrum (in the sense of Banaschewski–Mulvey) of the “Bohrification” \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\underline A}$$\end{document} of A, which is a commutative Rickart C*-algebra in the topos of functors from \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal{C}A}$$\end{document} to the category of sets. We explain the relationship of this construction to partial Boolean algebras and Bruns–Lakser completions. Finally, we establish a connection between probability measures on the lattice of projections on a Hilbert space H and probability valuations on the internal Gelfand spectrum of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\underline A}$$\end{document} for A = B(H). (shrink)

This paper is based on a semantic foundation of quantum logic which makes use of dialog-games. In the first part of the paper the dialogic method is introduced and under the conditions of quantum mechanical measurements the rules of a dialog-game about quantum mechanical propositions are established. In the second part of the paper the quantum mechanical dialog-game is replaced by a calculus of quantum logic. As the main part of the paper we show that (...) the calculus of quantum logic is complete and consistent with respect to the dialogic semantics. Since the dialoggame does not involve the 'excluded middle' the calculus represents a calculus of effective (intuitionistic) quantum logic. In a forthcoming paper it is shown that this calculus is equivalent to a calculus of sequents and more interestingly to a calculus of propositions. With the addition of the 'excluded middle' the latter calculus is a model for the lattice of subspaces of a Hilbert space. (shrink)

The main object of this article is to give two novel proofs of the admissibility of Ackermann’s rule (γ) for the propositional relevant logic R. The results are established as corollaries of cut elimination for systems of tableaux for R. Cut elimination, in turn, is established both nonconstructively (as a corollary of completeness) and constructively (using Gentzen-like methods). The extensibility of the techniques is demonstrated by showing that (γ) is admissible for RQ* (R with constant domain quantifiers). The status (...) of the admissibility of (γ) for RQ* was, to the best of the author’s knowledge, an open problem. Further extensions of these results will be explored in the sequel(s). (shrink)

This paper develops in certain directions the work of Meyer in [3], [4], [5] and [6]. In those works, Peano’s axioms for arithmetic were formulated with a logical base of the relevant logic R, and it was proved finitistically that the resulting arithmetic, called R♯, was absolutely consistent. It was pointed out that such a result escapes incau- tious formulations of Goedel’s second incompleteness theorem, and provides a basis for a revived Hilbert programme. The absolute consistency result used as (...) a model arithmetic modulo two. Modulo arithmetics are not or- dinarily thought of as an extension of Peano arithmetic, since some of the propositions of the latter, such as that zero is the successor of no number, fail in the former. Consequently a logical base which, unlike classical logic, tolerates contradictory theories was used for the model. The logical base for the model was the three-valued logic RM3, which has the advantage that while it is an extension of R, it is finite valued and so easier to handle. The resulting model-theoretic structure is interesting in its own right in that the set of sentences true therein consti- tutes a negation inconsistent but absolutely consistent arithmetic which is an extension of R♯. In fact, in the light of the result of [6], it is an extension of Peano arithmetic with a base of a classical logic, P♯. A generalisation of the structure is to modulo arithmetics with the same logical base RM3, but with varying moduli. We first study the properties of these arithmetics in this paper. The study is then generalised by vary- ing the logical base, to give the arithmetics RMni, of logical base RMn and modulus i. Not all of these exist, however, as arithmetical properties and logical properties interact, as we will show. The arithmetics RMni give rise, on intersection, to an inconsistent arithmetic RMω which is not of modulo i for any i. We also study its properties, and, among other results, we show by finitistic means that the more natural relevant arithmetics R♯ and R♯♯ are incomplete. In the rest of the paper we apply these techniques to several topics, particularly relevant quantum arithmetic in which we are able to show that the law of distribution remains unprovable. Aside from its intrinsic interest, we regard the present exercise as a demonstration that inconsistent theories and models are of mathematical worth and interest. (shrink)

We introduce a Gentzen style formulation of Basic Propositional Calculus(BPC), the logic that is interpreted in Kripke models similarly tointuitionistic logic except that the accessibility relation of eachmodel is not necessarily reflexive. The formulation is presented as adual-context style system, in which the left hand side of a sequent isdivided into two parts. Giving an interpretation of the sequents inKripke models, we show the soundness and completeness of the system withrespect to the class of Kripke models. The cut-elimination theorem (...) isproved in a syntactic way by modifying Gentzen's method. Thisdual-context style system exemplifies the effectiveness of dual-contextformulation in formalizing various non-classical logics. (shrink)

The paper is a continuation of another paper published as Part I. Now, the case of “n=3” is inferred as a corollary from the Kochen and Specker theorem (1967): the eventual solutions of Fermat’s equation for “n=3” would correspond to an admissible disjunctive division of qubit into two absolutely independent parts therefore versus the contextuality of any qubit, implied by the Kochen – Specker theorem. Incommensurability (implied by the absence of hidden variables) is considered as dual to quantum contextuality. (...) The relevant mathematical structure is Hilbert arithmetic in a wide sense, in the framework of which Hilbert arithmetic in a narrow sense and the qubit Hilbert space are dual to each other. A few cases involving set theory are possible: (1) only within the case “n=3” and implicitly, within any next level of “n” in Fermat’s equation; (2) the identification of the case “n=3” and the general case utilizing the axiom of choice rather than the axiom of induction. If the former is the case, the application of set theory and arithmetic can remain disjunctively divided: set theory, “locally”, within any level; and arithmetic, “globally”, to all levels. If the latter is the case, the proof is thoroughly within set theory. Thus, the relevance of Yablo’s paradox to the statement of Fermat’s last theorem is avoided in both cases. The idea of “arithmetic mechanics” is sketched: it might deduce the basic physical dimensions of mechanics (mass, time, distance) from the axioms of arithmetic after a relevant generalization, Furthermore, a future Part III of the paper is suggested: FLT by mediation of Hilbert arithmetic in a wide sense can be considered as another expression of Gleason’s theorem in quantum mechanics: the exclusions about (n = 1, 2) in both theorems as well as the validity for all the rest values of “n” can be unified after the theory of quantum information. The availability (respectively, non-availability) of solutions of Fermat’s equation can be proved as equivalent to the non-availability (respectively, availability) of a single probabilistic measure as to Gleason’s theorem. (shrink)

With a certain graphic interpretation in mind, we say that a function whose value at every point in its domain is a nonempty set of real numbers is an Abacus. It is shown that to every collection C of abaci there corresponds a logic, called an abacus logic, i.e., a certain set of propositions partially ordered by generalized implication. It is also shown that to every collection C of abaci there corresponds a theory JC in a classical propositional calculus (...) such that the abacus logic determined by C is isomorphic to the poset of JC. Two examples are given. In both examples abacus logic is a lattice in which there happens to be an operation of orthocomplementation. In the first example abacus logic turns out to be the Lindenbaum algebra of JC. In the second example abacus logic is a lattice isomorphic to the ortholattice of subspaces of a Hilbert space. Thus quantum logic can be regarded as an abacus logic. Without suggesting "hidden variables" it is finally shown that the Lindenbaum algebra of the theory in the second example is a subalgebra of the abacus logic B of the kind studied in example 1. It turns out that the "classical observables" associated with B and the "quantum observables" associated with quantum logic are not unrelated. The value of a classical observable contains, in coded form, information about the "uncertainty" of a quantum observable. This information is retrieved by decoding the value of the corresponding classical observable. (shrink)

We study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their propositional structure. This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

This paper develops in certain directions the work of Meyer in [3], [4], [5] and [6] (see also Routley [10] and Asenjo [11]). In those works, Peano’s axioms for arithmetic were formulated with a logical base of the relevant logic R, and it was proved finitistically that the resulting arithmetic, called R♯, was absolutely consistent. It was pointed out that such a result escapes incau- tious formulations of Goedel’s second incompleteness theorem, and provides a basis for a revived Hilbert (...) programme. The absolute consistency result used as a model arithmetic modulo two. Modulo arithmetics are not or- dinarily thought of as an extension of Peano arithmetic, since some of the propositions of the latter, such as that zero is the successor of no number, fail in the former. Consequently a logical base which, unlike classical logic, tolerates contradictory theories was used for the model. The logical base for the model was the three-valued logic RM3 (see e.g. [1] or [8]), which has the advantage that while it is an extension of R, it is finite valued and so easier to handle. The resulting model-theoretic structure (called in this paper RM32) is interesting in its own right in that the set of sentences true therein consti- tutes a negation inconsistent but absolutely consistent arithmetic which is an extension of R♯. In fact, in the light of the result of [6], it is an extension of Peano arithmetic with a base of a classical logic, P♯. A generalisation of the structure is to modulo arithmetics with the same logical base RM3, but with varying moduli (called RM3i here). We first study the properties of these arithmetics in this paper. The study is then generalised by vary- ing the logical base, to give the arithmetics RMni, of logical base RMn and modulus i. Not all of these exist, however, as arithmetical properties and logical properties interact, as we will show. The arithmetics RMni give rise, on intersection, to an inconsistent arithmetic RMω which is not of modulo i for any i. We also study its properties, and, among other results, we show by finitistic means that the more natural relevant arithmetics R♯ and R♯♯ are incomplete (whether or not consistent and recursively enumerable). In the rest of the paper we apply these techniques to several topics, particularly relevant quantum arithmetic in which we are able to show (unlike classical quantum arithmetic) that the law of distribution remains unprovable. Aside from its intrinsic interest, we regard the present exercise as a demonstration that inconsistent theories and models are of mathematical worth and interest. (shrink)

In this paper, we present a simple sequent calculus for the modal propositional logic S5. We prove that this sequent calculus is theoremwise equivalent to the Hilbert-style system S5, that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in a purely syntactic way.

Cut reductions are defined for a Kripke-style formulation of modal logic in terms of indexed systems of sequents. A detailed proof of the normalization (cutelimination) theorem is given. The proof is uniform for the propositional modal systems with all combinations of reflexivity, symmetry and transitivity for the accessibility relation. Some new transformations of derivations (compared to standard sequent formulations) are needed, and some additional properties are to be checked. The display formulations [1] of the systems considered can be presented (...) as encodings of Kripke-style formulations. (shrink)

In this paper we present a sequent calculus for the modal propositional logic GL (the logic of provability) obtained by means of the tree-hypersequent method, a method in which the metalinguistic strength of hypersequents is improved, so that we can simulate trees shapes. We prove that this sequent calculus is sound and complete with respect to the Hilbert-style system GL, that it is contraction free and cut free and that its logical and modal rules are invertible. No explicit (...) semantic element is used in the sequent calculus and all the results are proved in a purely syntactic way. (shrink)

In this note we compare propositional logics for closed substitutions and propositional logics for open substitutions in constructive arithmetical theories. We provide a strong example where these logics diverge in an essential way. We prove that for Markov's Arithmetic, that is, Heyting's Arithmetic plus Markov's principle plus Extended Church's Thesis, the logic of closed and the logic of open substitutions are the same.