Search

We extend classical first-order logic with a family of weak probability quantifiers, which we call submeasure quantifiers. Formulas are finitary, but infinitary deduction rules are needed. We consider first-order structures that are equipped with a countable family of submeasures (hence the name of the new quantifiers). We prove that every consistent set of sentences in the resulting logic is satisfiable in some structure as above. Then we restrict the set of formulas by requiring that no submeasure quantifier occurs within the scope of some classical quantifier. By suitably extending the deduction rules, we prove that every consistent set of sentences from the restricted class of formulas is satisfiable in some structure whose submeasures are actually outer measures. To perform the last step, we apply nonstandard techniques à la A. Robinson.

We introduce a propositional many-valued modal logic which is an extension of the Continuous Propositional Logic to a modal system. Otherwise said, we extend the minimal modal logic to a Continuous...

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 show how to extend the Continuous Propositional Logic by means of an infinitary rule in order to achieve a Strong Completeness Theorem. Eventually we investigate how to recover a weak version of the Deduction 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.

Quantum Coherent Spaces were introduced by Girard as a quantum framework where to interpret the exponential-free fragment of Linear Logic. Aim of this paper is to extend Girard's interpretation to a subsystem of linear logic with bounded exponentials. We provide deduction rules for the bounded exponentials and, correspondingly, we introduce the novel notion of bounded exponentials of Quantum Coherent Spaces. We show that the latter provide a categorical model of our system. In order to do that, we first study properties of the category of Quantum Coherent Spaces.

We introduce a complete and cut-free proof system for a sufficiently expressive fragment of Metric Temporal Logic over dense time domains in which a schema of induction is provable. So doing we extend results previously obtained by Montagna et al. to unbounded temporal operators. (© 2004 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)

We introduce an extension of natural deduction that is suitable for dealing with modal operators and induction. We provide a proof reduction system and we prove a strong normalization theorem for an intuitionistic calculus. As a consequence we obtain a purely syntactic proof of consistency. We also present a classical calculus and we relate provability in the two calculi by means of an adequate formula translation.

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 study conditions for structures based on Banach spaces having the property that each set definable by neocompact formula (certain infinitary formula) is equivalent to the countable intersection of sets definable by quantifier-free formulas. We show that this property is invariant with respect to different nonstandard hull constructions and it is the same as Henson's Quantifier Elimination in sufficiently saturated nonstandard hulls of internal Banach spaces.

For arbitrary finite group $G$ and countable Dedekind domain $R$ such that the residue field $R/P$ is finite for every maximal $R$ -ideal $P$ , we show that the localizations at every maximal ideal of two $RG$ -lattices are isomorphic if and only if the two lattices satisfy the same first order sentences. Then we investigate generalizations of the above results to arbitrary $R$ -torsion-free $RG$ -modules and we apply the previous results to show the decidability of the theory of ${\vec Z}C(2)^2$ -lattices. Eventually, we show that ${\vec Z} [i] C(2)^2$ -lattices have undecidable theory.

We describe the constructive content of proofs in a fragment of propositional Infinitary Linear Logic in terms of strategies for a suitable class of games. Such strategies interpret linear proofs as parallel algorithms as long as the asymmetry of the connectives ? and ! allows it.

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.

In this paper, we prove completeness of SLDNF resolution and NAF rule for the class of allowed and locally stratified programs satisfying the further condition of well-behavedness. Well-behavedness imposes a computational restriction on programs whose aim is to ensure that the 3- and 2-valued consequences of Clark's completion of a program belonging to the above-mentioned class do coincide. Then one can apply Kunen's 3-valued completeness theorem in order to get a 2-valued completeness result

Aim of this paper is to provide an alternative proof of consistency for the completion of a semi-strict program. Furthermore, we prove the continuity of the immediate consequence map associated to a locally call-consistent program with respect to any preinterpretation that is a model of the equality theory of its Clark’s completion.

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.