Search

We introduce a logic for a class of probabilistic Kripke structures that we call type structures, as they are inspired by Harsanyi type spaces. The latter structures are used in theoretical economics and game theory. A strong completeness theorem for an associated infinitary propositional logic with probabilistic operators was proved by Meier. By simplifying Meier’s proof, we prove that our logic is strongly complete with respect to the class of type structures. In order to do that, we define a canonical model (in the sense of modal logics), which turns out to be a terminal object in a suitable category. Furthermore, we extend some standard model-theoretic constructions to type structures and we prove analogues of first-order results for those constructions.

We study a modal extension of the Continuous First-Order Logic of Ben Yaacov and Pedersen (J Symb Logic 75(1):168–190, 2010). We provide a set of axioms for such an extension. Deduction rules are just Modus Ponens and Necessitation. We prove that our system is sound with respect to a Kripke semantics and, building on Ben Yaacov and Pedersen (2010), that it satisfies a number of properties similar to those of first-order predicate logic. Then, by means of a canonical model construction, we get that every consistent set of formulas is satisfiable. From the latter result we derive an Approximated Strong Completeness Theorem, in the vein of Continuous Logic, and a Compactness Theorem.

We study a real valued propositional logic with unbounded positive and negative truth values that we call R-valued logic. Such logic slightly extends continuous propositional logic which, in turn, builds on Lukasiewicz many-valued logic. After presenting the deduction machinery and the semantics of R-valued logic, we prove a completeness theorem for finite theories. Then we define unital and Archimedean theories, in accordance with the theory of Riesz spaces. In the unital setting, we prove the equivalence of consistency and satisfiability and an approximated completeness theorem similar to the one that holds for continuous propositional logic. Eventually, among unital theories, we characterize Archimedean theories as those for which strong completeness holds. We also point out that R-valued logic provides alternative calculi for Lukasiewicz and for propositional continuous logic.

We introduce a natural deduction system for the until-free subsystem of the branching time logic Although we work with labelled formulas, our system differs conceptually from the usual labelled deduction systems because we have no relational formulas. Moreover, no deduction rule embodies semantic features such as properties of accessibility relation or similar algebraic properties. We provide a suitable semantics for our system and prove that it is sound and weakly complete with respect to such semantics.

We provide some consequences of a Quantifier Elimination Property and related properties previously introduced (see [4]) in the setting of Banach space structures. We further consider some applications of quantifierfree definability, such as strict convexity via the definability of certain mapping and the continuity of definable functions.

The Eberlein-Smulian theorem on the equivalence of weak compactness and the finite intersection property of bounded closed convex sets is given a short elementary proof by applying Abraham Robinson's nonstandard characterization of compactness.

We study a modal extension of the Continuous First-Order Logic of Ben Yaacov and Pedersen (J Symb Logic 75(1):168–190, 2010). We provide a set of axioms for such an extension. Deduction rules are just Modus Ponens and Necessitation. We prove that our system is sound with respect to a Kripke semantics and, building on Ben Yaacov and Pedersen (2010), that it satisfies a number of properties similar to those of first-order predicate logic. Then, by means of a canonical model construction, we get that every consistent set of formulas is satisfiable. From the latter result we derive an Approximated Strong Completeness Theorem, in the vein of Continuous Logic, and a Compactness Theorem.

We introduce the notion of generalized invertibility, a weak notion of invertibility that makes sense in the nonstandard hull of a Banach algebra. We show that a standard algebra is the closure of its invertible elements exactly when all the elements of its nonstandard hull are generalized invertible. For commutative algebras, we relate the problem of liftability of homomorphisms to the property of approximately multiplicative functionals being near to multiplicative functionals (AMNM property) and we prove a nonstandard characterization of the latter property. Finally we show that a standard superreflexive Banach algebra has the the AMNM property exactly when its nonstandard hull does.

We investigate the consequences of removing the infinitary axiom and rules from a previously defined proof system for a fragment of propositional metric temporal logic over dense time (see [1]). (© 2006 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)

The action of environmental loads such as wind and waves on offshore steel structures is locally emphasized by complex tubular connections, giving place to high stress concentration in correspondence of welds between pipe elements. This phenomenon, which heavily influences the fatigue life of the joint and, as a consequence, the operability of the whole platform, can be quantified by the Stress Concentration Factor. SCF can be determined either by experimental approach, numerical analysis and parametrical formulas developed mainly in the seventies-eighties by specialized authors like Kuang, Wordsworth, Smedley and Efthymiou. Even though these formulas, quoted as reference in the main world recognized rules, represented for a long time a useful tool for the designers of most projects, some discrepancies have been found to exist among them. A research has then been jointly promoted by University of Genoa and RINA Industry in order to compare the results of the parametric formulas with those coming from a finite element analysis performed on very refined numerical models made of brick elements. In this investigation attention has been focused on Y/T type joints; a wide range of configurations has been analysed by varying the most important parameters defining the geometry of the joint. Each configuration has been loaded by axial force and in/out of plane bending moment.Copyright © 2005 by ASME

The aim of this paper is to provide a way of extracting the constructive content of a certain family of classical proofs directly from the proofs themselves. The paper itself is written in a purely constructive style. Our work is inspired by the game interpretations of classical logic due to Novikov (1943) and Coquand (1995). These interpretations date back to Gentzen (1969) and Bernays (1970) and were recently studied by Coquand (1995) who made use of technical tools developed by Novikov (1943). We will introduce an interpretation which is a short and compact description of the meaning assigned to classical formulas by Coquand’s interpretation. Contrary to Coquand, we will completely avoid any game terminology, by making use of the intuitionistic notion of continuous computation. A posteriori, our interpretation turns out to be related to Kreisel’s no-counterexample interpretation (Kreisel 1957) but, compared with his, it provides simpler constructive proofs. The reader is referred to Baratella and Berardi (1997) for a number of examples of constructive proofs provided by our interpretation that can be used for a comparison. Indeed, our interpretation is a fragment of Coquand’s that can be easily expanded to a variant of his. However, we claim that our interpretation suffices as long as we are only interested in the constructive meaning of classical formulas (whilst we need Coquand’s if we are interested in computations lying behind the constructive meaning). We will support this claim by proving, as the main result, that our interpretation is intuitionistically complete, in the same way as Coquand’s (Herbelin 1995). That is, we will intuitionistically prove that a formula is derivable in infmitary classical logic if and only if its interpretation holds. Since infinitary classical logic is classically complete, loosely speaking we can restate our result as follows: the classical truth of a classical formula is intuitionistically equivalent to the intuitionistic truth of the constructive interpretation of the formula. We also recall that Godel’s Dialectica interpretation is not intuitionistically complete (see section 7). In this regard, see also Berardi (1997). In addition, we point out that, contrary to the game interpretations, our interpretation is not a sort of reformulation of what is going on in the sequent calculus.