8 found
Order:
  1.  28
    Decidability of ∀*∀‐Sentences in Membership Theories.Eugenio G. Omodeo, Franco Parlamento & Alberto Policriti - 1996 - Mathematical Logic Quarterly 42 (1):41-58.
    The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the ∀*∀ class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented.
    Direct download  
     
    Export citation  
     
    Bookmark   6 citations  
  2.  28
    A note on the sequent calculi.Franco Parlamento & Flavio Previale - forthcoming - Review of Symbolic Logic:1-15.
    We show that the replacement rule of the sequent calculi ${\bf G3[mic]}^= $ in [8] can be replaced by the simpler rule in which one of the principal formulae is not repeated in the premiss.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  45
    Expressing infinity without foundation.Franco Parlamento & Alberto Policriti - 1991 - Journal of Symbolic Logic 56 (4):1230-1235.
    The axiom of infinity can be expressed by stating the existence of sets satisfying a formula which involves restricted universal quantifiers only, even if the axiom of foundation is not assumed.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  21
    (1 other version)The decision problem for restricted universal quantification in set theory and the axiom of foundation.Franco Parlamento & Alberto Policriti - 1992 - Mathematical Logic Quarterly 38 (1):143-156.
    The still unsettled decision problem for the restricted purely universal formulae 0-formulae) of the first order set-theoretic language based over =, ∈ is discussed in relation with the adoption or rejection of the axiom of foundation. Assuming the axiom of foundation, the related finite set-satisfiability problem for the very significant subclass of the 0-formulae consisting of the formulae involving only nested variables of level 1 is proved to be semidecidable on the ground of a reflection property over the hereditarily finite (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  5.  38
    (1 other version)The Decidability of the Class and the Axiom of Foundation.Dorella Bellè & Franco Parlamento - 2001 - Notre Dame Journal of Formal Logic 42 (1):41-53.
    We show that the Axiom of Foundation, as well as the Antifoundation Axiom AFA, plays a crucial role in determining the decidability of the following problem. Given a first-order theory T over the language , and a sentence F of the form with quantifier-free in the same language, are there models of T in which F is true? Furthermore we show that the Extensionality Axiom is quite irrelevant in that respect.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark  
  6.  37
    Decidability and Completeness for Open Formulas of Membership Theories.Dorella Bellè & Franco Parlamento - 1995 - Notre Dame Journal of Formal Logic 36 (2):304-318.
    We establish the decidability, with respect to open formulas in the first order language with equality =, the membership relation , the constant for the empty set, and a binary operation w which, applied to any two sets x and y, yields the results of adding y as an element to x, of the theory NW having the obvious axioms for and w. Furthermore we establish the completeness with respect to purely universal sentences of the theory , obtained from NW (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  19
    Absorbing the structural rules in the sequent calculus with additional atomic rules.Franco Parlamento & Flavio Previale - 2020 - Archive for Mathematical Logic 59 (3-4):389-408.
    We show that if the structural rules are admissible over a set \ of atomic rules, then they are admissible in the sequent calculus obtained by adding the rules in \ to the multisuccedent minimal and intuitionistic \ calculi as well as to the classical one. Two applications to pure logic and to the sequent calculus with equality are presented.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8.  18
    Cut Elimination for Gentzen's Sequent Calculus with Equality and Logic of Partial Terms.Franco Parlamento & Flavio Previale - 2013 - In Kamal Lodaya (ed.), Logic and Its Applications. Springer. pp. 161--172.
    Direct download  
     
    Export citation  
     
    Bookmark