Results for 'proof tree transformation'

970 found
Order:
  1.  95
    Some general results about proof normalization.Marc Aiguier & Delphine Longuet - 2010 - Logica Universalis 4 (1):1-29.
    In this paper, we provide a general setting under which results of normalization of proof trees such as, for instance, the logicality result in equational reasoning and the cut-elimination property in sequent or natural deduction calculi, can be unified and generalized. This is achieved by giving simple conditions which are sufficient to ensure that such normalization results hold, and which can be automatically checked since they are syntactical. These conditions are based on basic properties of elementary combinations of inference (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  2.  39
    On transformations of constant depth propositional proofs.Arnold Beckmann & Sam Buss - 2019 - Annals of Pure and Applied Logic 170 (10):1176-1187.
    This paper studies the complexity of constant depth propositional proofs in the cedent and sequent calculus. We discuss the relationships between the size of tree-like proofs, the size of dag-like proofs, and the heights of proofs. The main result is to correct a proof construction in an earlier paper about transformations from proofs with polylogarithmic height and constantly many formulas per cedent.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  89
    Socratic Trees.Dorota Leszczyńska-Jasion, Mariusz Urbański & Andrzej Wiśniewski - 2013 - Studia Logica 101 (5):959-986.
    The method of Socratic proofs (SP-method) simulates the solving of logical problem by pure questioning. An outcome of an application of the SP-method is a sequence of questions, called a Socratic transformation. Our aim is to give a method of translation of Socratic transformations into trees. We address this issue both conceptually and by providing certain algorithms. We show that the trees which correspond to successful Socratic transformations—that is, to Socratic proofs—may be regarded, after a slight modification, as Gentzen-style (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  4.  19
    Proof Systems for Two-Way Modal Mu-Calculus.Bahareh Afshari, Sebastian Enqvist, Graham E. Leigh, Johannes Marti & Yde Venema - forthcoming - Journal of Symbolic Logic:1-50.
    We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  5.  76
    A compact representation of proofs.Dale A. Miller - 1987 - Studia Logica 46 (4):347 - 370.
    A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cut-free sequential proofs. A theorem prover which (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  6.  90
    The deduction rule and linear and near-linear proof simulations.Maria Luisa Bonet & Samuel R. Buss - 1993 - Journal of Symbolic Logic 58 (2):688-709.
    We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  7.  27
    Separation results for the size of constant-depth propositional proofs.Arnold Beckmann & Samuel R. Buss - 2005 - Annals of Pure and Applied Logic 136 (1-2):30-55.
    This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  8.  46
    Syntactical results on the arithmetical completeness of modal logic.Paolo Gentilini - 1993 - Studia Logica 52 (4):549 - 564.
    In this paper the PA-completeness of modal logic is studied by syntactical and constructive methods. The main results are theorems on the structure of the PA-proofs of suitable arithmetical interpretationsS of a modal sequentS, which allow the transformation of PA-proofs ofS into proof-trees similar to modal proof-trees. As an application of such theorems, a proof of Solovay's theorem on arithmetical completeness of the modal system G is presented for the class of modal sequents of Boolean combinations (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  9. Partial proof trees as building blocks for a categorial grammar.Aravind K. Joshi & Seth Kulick - 1997 - Linguistics and Philosophy 20 (6):637-667.
    We describe a categorial system (PPTS) based on partial proof trees(PPTs) as the building blocks of the system. The PPTs are obtained byunfolding the arguments of the type that would be associated with a lexicalitem in a simple categorial grammar. The PPTs are the basic types in thesystem and a derivation proceeds by combining PPTs together. We describe theconstruction of the finite set of basic PPTs and the operations forcombining them. PPTS can be viewed as a categorial system incorporating (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  10.  13
    Extracting information from resolution proof trees.David Luckham & Nils J. Nilsson - 1971 - Artificial Intelligence 2 (1):27-54.
  11.  71
    Second-order abstract categorial grammars as hyperedge replacement grammars.Makoto Kanazawa - 2010 - Journal of Logic, Language and Information 19 (2):137-161.
    Second-order abstract categorial grammars (de Groote in Association for computational linguistics, 39th annual meeting and 10th conference of the European chapter, proceedings of the conference, pp. 148–155, 2001) and hyperedge replacement grammars (Bauderon and Courcelle in Math Syst Theory 20:83–127, 1987; Habel and Kreowski in STACS 87: 4th Annual symposium on theoretical aspects of computer science. Lecture notes in computer science, vol 247, Springer, Berlin, pp 207–219, 1987) are two natural ways of generalizing “context-free” grammar formalisms for string and (...) languages. It is known that the string generating power of both formalisms is equivalent to (non-erasing) multiple context-free grammars (Seki et al. in Theor Comput Sci 88:191–229, 1991) or linear context-free rewriting systems (Weir in Characterizing mildly context-sensitive grammar formalisms, University of Pennsylvania, 1988). In this paper, we give a simple, direct proof of the fact that second-order ACGs are simulated by hyperedge replacement grammars, which implies that the string and tree generating power of the former is included in that of the latter. The normal form for tree-generating hyperedge replacement grammars given by Engelfriet and Maneth (Graph transformation. Lecture notes in computer science, vol 1764. Springer, Berlin, pp 15–29, 2000) can then be used to show that the tree generating power of second-order ACGs is exactly the same as that of hyperedge replacement grammars. (shrink)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  12.  32
    Self-knowledge at the margins.Hannah Trees - 2022 - Dissertation, University of Texas at Austin
    This dissertation is a collection of three papers – “Knowing Oneself for Others,” “Stereotype Threat and the Value of Self-Knowledge,” and “Self-Knowledge, Epistemic Work, and Injustice” – in which I address the connections between self-knowledge production and social inequality. I explain, using a variety of contemporary political and cultural examples, that marginalized individuals are more likely to be required to know certain things about themselves than socially privileged individuals, especially about those aspects of their lives and identities which are essential (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  13.  98
    Logic and Knowledge.Emiliano Ippoliti, Carlo Cellucci & Emily Grosholz (eds.) - 2011 - Newcastle upon Tyne: Cambridge Scholar Publishing.
    Logic and Knowledge -/- Editor: Carlo Cellucci, Emily Grosholz and Emiliano Ippoliti Date Of Publication: Aug 2011 Isbn13: 978-1-4438-3008-9 Isbn: 1-4438-3008-9 -/- The problematic relation between logic and knowledge has given rise to some of the most important works in the history of philosophy, from Books VI–VII of Plato’s Republic and Aristotle’s Prior and Posterior Analytics, to Kant’s Critique of Pure Reason and Mill’s A System of Logic, Ratiocinative and Inductive. It provides the title of an important collection of papers (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  41
    Ramsey-type graph coloring and diagonal non-computability.Ludovic Patey - 2015 - Archive for Mathematical Logic 54 (7-8):899-914.
    A function is diagonally non-computable if it diagonalizes against the universal partial computable function. D.n.c. functions play a central role in algorithmic randomness and reverse mathematics. Flood and Towsner asked for which functions h, the principle stating the existence of an h-bounded d.n.c. function implies Ramsey-type weak König’s lemma. In this paper, we prove that for every computable order h, there exists an ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\omega}$$\end{document} -model of h-DNR which is not a not (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  15. Automating Reasoning with Standpoint Logic via Nested Sequents.Tim Lyon & Lucía Gómez Álvarez - 2018 - In Michael Thielscher, Francesca Toni & Frank Wolter (eds.), Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR2018). pp. 257-266.
    Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics---proof systems that manipulate trees whose nodes are multisets of formulae---and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  16. Logiki drzew derywacyjnych.Wojciech Krysztofiak - 2007 - Filozofia Nauki 2.
    The paper presents the construction of a new class of logics, which are called logics of derivational trees. The presentation comprises three sections: (i) intuitive psychological motivations for these logics stemming from some results of developmental psycho-linguistics (Piaget, Chomsky), (ii) the construction of formal calculus with help of algorithmic tools, and (iii) the construction of set-theoretic semantic model for our logic. They determine criteria of valid deriving and transforming structures which are usually described in the literature as derivational trees. These (...)
     
    Export citation  
     
    Bookmark  
  17.  37
    Torsion-free abelian groups with optimal Scott families.Alexander G. Melnikov - 2018 - Journal of Mathematical Logic 18 (1):1850002.
    We prove that for any computable successor ordinal of the form α = δ + 2k there exists computable torsion-free abelian group that is relatively Δα0 -categorical and not Δα−10 -categorical. Equivalently, for any such α there exists a computable TFAG whose initial segments are uniformly described by Σαc infinitary computable formulae up to automorphism, and there is no syntactically simpler family of formulae that would capture these orbits. As far as we know, the problem of finding such optimal examples (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  18.  36
    Phenomenology and Transcendental Argument in Mathematics: The Case of Brouwer's Bar Theorem.Mark van Atten - unknown
    On the intended interpretation of intuitionistic logic, Heyting's Proof Interpretation, a proof of a proposition of the form p -> q consists in a construction method that transforms any possible proof of p into a proof of q. This involves the notion of the totality of all proofs in an essential way, and this interpretation has therefore been objected to on grounds of impredicativity (e.g. Gödel 1933). In fact this hardly ever leads to problems as in (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  19.  23
    Tree-Like Proof Systems for Finitely-Many Valued Non-deterministic Consequence Relations.Pawel Pawlowski - 2020 - Logica Universalis 14 (4):407-420.
    The main goal of this paper is to provide an abstract framework for constructing proof systems for various many-valued logics. Using the framework it is possible to generate strongly complete proof systems with respect to any finitely valued deterministic and non-deterministic logic. I provide a couple of examples of proof systems for well-known many-valued logics and prove the completeness of proof systems generated by the framework.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  20. L'etica moderna. Dalla Riforma a Nietzsche.Sergio Cremaschi - 2007 - Roma RM, Italia: Carocci.
    This book tells the story of modern ethics, namely the story of a discourse that, after the Renaissance, went through a methodological revolution giving birth to Grotius’s and Pufendorf’s new science of natural law, leaving room for two centuries of explorations of the possible developments and implications of this new paradigm, up to the crisis of the Eighties of the eighteenth century, a crisis that carried a kind of mitosis, the act of birth of both basic paradigms of the two (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  21.  28
    Tree of Letters, “Tree of Life:” How a Letter of the Torah Can Transform (the Human Being Made in) the Image of God1.Charlotte Berkowitz - 2005 - The European Legacy 10 (7):703-716.
    Venerable tradition allies the Torah with Wisdom, a “tree of life.”2 The tree of life is an ancient mythic symbol of the earth mother. This essay demonstrates the capacity of the Torah to facilitate a reintegrative return to the mother when, as now, the religious narratives falter that once seemed to ensure the unity of man made in the image of God conceived only as the Father. Participating in the process of this return one discovers beneath the Torah's (...)
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  22.  23
    (1 other version)Premiss tree proofs and logic of contradiction.Zvonimir Šikić - 1990 - Mathematical Logic Quarterly 36 (3):273-280.
    Direct download  
     
    Export citation  
     
    Bookmark  
  23.  13
    Proofs of tree identities.Ewa Graczynska - 2000 - Bulletin of the Section of Logic 29 (1/2):31-41.
    Direct download  
     
    Export citation  
     
    Bookmark  
  24. Meillassoux’s Virtual Future.Graham Harman - 2011 - Continent 1 (2):78-91.
    continent. 1.2 (2011): 78-91. This article consists of three parts. First, I will review the major themes of Quentin Meillassoux’s After Finitude . Since some of my readers will have read this book and others not, I will try to strike a balance between clear summary and fresh critique. Second, I discuss an unpublished book by Meillassoux unfamiliar to all readers of this article, except those scant few that may have gone digging in the microfilm archives of the École normale (...)
     
    Export citation  
     
    Bookmark   2 citations  
  25.  72
    Toward A Visual Proof System: Lewis Carroll’s Method of Trees.Francine F. Abeles - 2012 - Logica Universalis 6 (3-4):521-534.
    In the period 1893–1897 Charles Dodgson, writing as Lewis Carroll, published two books and two articles on logic topics. Manuscript material first published in 1977 together with letters and diary entries provide evidence that he was working toward a visual proof system for complex syllogistic propositional logic based on a mechanical tree method that he devised.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  26.  17
    The ‘civic-transformative’ value of urban street trees.Oliver Harrison - 2024 - Environmental Values 33 (4):363-379.
    Urban street trees (USTs) have a range of values – some of which are easier to quantify than others. Focusing specifically on the UK context and using the Sheffield Tree Protests (2012–) as a case study, whilst confirming existing research as to the variety of values associated with their specifically ‘cultural’ services, the article argues that USTs have an additional potential form – what I call ‘civic-transformative value’. This form of value has at least three key characteristics. Firstly, it (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27.  18
    Exact unprovability results for compound well-quasi-ordered combinatorial classes.Andrey Bovykin - 2009 - Annals of Pure and Applied Logic 157 (2-3):77-84.
    In this paper we prove general exact unprovability results that show how a threshold between provability and unprovability of a finite well-quasi-orderedness assertion of a combinatorial class is transformed by the sequence-construction, multiset-construction, cycle-construction and labeled-tree-construction. Provability proofs use the asymptotic pigeonhole principle, unprovability proofs use Weiermann-style compression techniques and results from analytic combinatorics.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  28.  53
    Trees and finite satisfiability: proof of a conjecture of Burgess.George Boolos - 1984 - Notre Dame Journal of Formal Logic 25 (3):193-197.
  29. The Proof That the Standard Transformations of E and B Are Not the Lorentz Transformations.Tomislav Ivezić - 2003 - Foundations of Physics 33 (9):1339-1347.
    In this paper it is exactly proved that the standard transformations of the three-dimensional (3D) vectors of the electric and magnetic fields E and B are not relativistically correct transformations. Thence the 3D vectors E and B are not well-defined quantities in the 4D space-time and, contrary to the general belief, the usual Maxwell equations with the 3D E and B are not in agreement with the special relativity. The 4-vectors E a and B a , as well-defined 4D quantities, (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  30.  10
    A game‐theoretic proof of Shelah's theorem on labeled trees.Trevor M. Wilson - 2020 - Mathematical Logic Quarterly 66 (2):190-194.
    We give a new proof of a theorem of Shelah which states that for every family of labeled trees, if the cardinality κ of the family is much larger (in the sense of large cardinals) than the cardinality λ of the set of labels, more precisely if the partition relation holds, then there is a homomorphism from one labeled tree in the family to another. Our proof uses a characterization of such homomorphisms in terms of games.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  31.  48
    The Proof that Maxwell Equations with the 3D E and B are not Covariant upon the Lorentz Transformations but upon the Standard Transformations: The New Lorentz Invariant Field Equations.Tomislav Ivezić - 2005 - Foundations of Physics 35 (9):1585-1615.
    In this paper the Lorentz transformations (LT) and the standard transformations (ST) of the usual Maxwell equations (ME) with the three-dimensional (3D) vectors of the electric and magnetic fields, E and B, respectively, are examined using both the geometric algebra and tensor formalisms. Different 4D algebraic objects are used to represent the usual observer dependent and the new observer independent electric and magnetic fields. It is found that the ST of the ME differ from their LT and consequently that the (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  32.  59
    Tree proofs for syllogistic.Peter M. Simons - 1989 - Studia Logica 48 (4):539 - 554.
    This paper presents a tree method for testing the validity of inferences, including syllogisms, in a simple term logic. The method is given in the form of an algorithm and is shown to be sound and complete with respect to the obvious denotational semantics. The primitive logical constants of the system, which is indebted to the logical works of Jevons, Brentano and Lewis Carroll, are term negation, polyadic term conjunction, and functors affirming and denying existence, and use is also (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  33.  70
    Barking Up the Wrong Tree: On Control, Transformative Experiences, and Turning Over a New Leaf.Marcela Herdova - 2020 - The Monist 103 (3):278-293.
    I argue that we do not intentionally and rationally shape our character and values in major ways. I base this argument on the nature of transformative experiences, that is, those experiences which are transformative from personal and epistemological points of view. The argument is roughly this. First, someone who undergoes major changes in her character or values thereby undergoes a transformative experience. Second, if she undergoes such an experience, her reasons for changing in a major way are inaccessible to her (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  34.  11
    The B∗ tree search algorithm: A best-first proof procedure.Hans Berliner - 1979 - Artificial Intelligence 12 (1):23-40.
  35. The proof that Maxwell equations with the 3D E and B are not covariant upon the Lorentz transformations but upon the standart transformations: the new Lorentz invariant field equations.Ivezic Tomislav - 2005 - Foundations of Physics 35:1585.
     
    Export citation  
     
    Bookmark  
  36. (2 other versions)Constrained by reason, transformed by love: Murdoch on the standard of proof.Carla Bagnoli - 2018 - In Gary Browning (ed.), Murdoch on Truth and Love. Cham: Springer Verlag. pp. 2021, 63-88.
    According to Iris Murdoch, the chief experience in morality is loving attention. Her view calls into question the Kantian account of the standard of moral authority, and ultimately denies that reason might provide moral discernment, validate moral experience or drive us toward moral progress. Like Kant, Murdoch defines the moral experience as the subjective experience of freedom, which resists any reductivist approach. Unlike Kant, she thinks that this free agency is unprincipled. Some of her arguments are based on an oversimplified (...)
     
    Export citation  
     
    Bookmark   1 citation  
  37.  69
    (1 other version)A direct independence proof of Buchholz's Hydra Game on finite labeled trees.Masahiro Hamano & Mitsuhiro Okada - 1998 - Archive for Mathematical Logic 37 (2):67-89.
    We shall give a direct proof of the independence result of a Buchholz style-Hydra Game on labeled finite trees. We shall show that Takeuti-Arai's cut-elimination procedure of $(\Pi^{1}_{1}-CA) + BI$ and of the iterated inductive definition systems can be directly expressed by the reduction rules of Buchholz's Hydra Game. As a direct corollary the independence result of the Hydra Game follows.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  38. A calculus for Belnap's logic in which each proof consists of two trees.Stefan Wintein & Reinhard Muskens - 2012 - Logique Et Analyse 220:643-656.
    In this paper we introduce a Gentzen calculus for (a functionally complete variant of) Belnap's logic in which establishing the provability of a sequent in general requires \emph{two} proof trees, one establishing that whenever all premises are true some conclusion is true and one that guarantees the falsity of at least one premise if all conclusions are false. The calculus can also be put to use in proving that one statement \emph{necessarily approximates} another, where necessary approximation is a natural (...)
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  39.  87
    Quantified propositional logic and the number of lines of tree-like proofs.Alessandra Carbone - 2000 - Studia Logica 64 (3):315-321.
    There is an exponential speed-up in the number of lines of the quantified propositional sequent calculus over Substitution Frege Systems, if one considers proofs as trees. Whether this is true also for the number of symbols, is still an open problem.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  40.  40
    Program Transformation and Proof Transformation.Wilfried Sieg & Stanley S. Wainer - unknown
    Wilfred Sieg and Stanley S. Wainer. Program Transformation and Proof Transformation.
    No categories
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  41.  70
    Tableaux and Dual Tableaux: Transformation of Proofs.Joanna Golińska-Pilarek & Ewa Orłowska - 2007 - Studia Logica 85 (3):283-302.
    We present two proof systems for first-order logic with identity and without function symbols. The first one is an extension of the Rasiowa-Sikorski system with the rules for identity. This system is a validity checker. The rules of this system preserve and reflect validity of disjunctions of their premises and conclusions. The other is a Tableau system, which is an unsatisfiability checker. Its rules preserve and reflect unsatisfiability of conjunctions of their premises and conclusions. We show that the two (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  42.  72
    Proof-theoretic modal PA-Completeness III: The syntactic proof.Paolo Gentilini - 1999 - Studia Logica 63 (3):301-310.
    This paper is the final part of the syntactic demonstration of the Arithmetical Completeness of the modal system G; in the preceding parts [9] and [10] the tools for the proof were defined, in particular the notion of syntactic countermodel. Our strategy is: PA-completeness of G as a search for interpretations which force the distance between G and a GL-LIN-theorem to zero. If the GL-LIN-theorem S is not a G-theorem, we construct a formula H expressing the non G-provability of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  43.  44
    Proof-theoretic modal PA-Completeness II: The syntactic countermodel.Paolo Gentilini - 1999 - Studia Logica 63 (2):245-268.
    This paper is the second part of the syntactic demonstration of the Arithmetical Completeness of the modal system G, the first part of which is presented in [9]. Given a sequent S so that ⊢GL-LIN S, ⊬G S, and given its characteristic formula H = char(S), which expresses the non G-provability of S, we construct a canonical proof-tree T of ~ H in GL-LIN, the height of which is the distance d(S, G) of S from G. T is (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  44.  17
    The tree property at the two immediate successors of a singular cardinal.James Cummings, Yair Hayut, Menachem Magidor, Itay Neeman, Dima Sinapova & Spencer Unger - 2021 - Journal of Symbolic Logic 86 (2):600-608.
    We present an alternative proof that from large cardinals, we can force the tree property at $\kappa ^+$ and $\kappa ^{++}$ simultaneously for a singular strong limit cardinal $\kappa $. The advantage of our method is that the proof of the tree property at the double successor is simpler than in the existing literature. This new approach also works to establish the result for $\kappa =\aleph _{\omega ^2}$.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  45.  45
    Proof-theoretic modal pa-completeness I: A system-sequent metric.Paolo Gentilini - 1999 - Studia Logica 63 (1):27-48.
    This paper is the first of a series of three articles that present the syntactic proof of the PA-completeness of the modal system G, by introducing suitable proof-theoretic objects, which also have an independent interest. We start from the syntactic PA-completeness of modal system GL-LIN, previously obtained in [7], [8], and so we assume to be working on modal sequents S which are GL-LIN-theorems. If S is not a G-theorem we define here a notion of syntactic metric d(S, (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  46.  26
    Phyloreferences: Tree-Native, Reproducible, and Machine-Interpretable Taxon Concepts.Nico Cellinese, Stijn Conix & Hilmar Lapp - 2022 - Philosophy, Theory, and Practice in Biology 14 (8).
    Evolutionary and organismal biology have become inundated with data. At the same rate, we are experiencing a surge in broader evolutionary and ecological syntheses for which tree-thinking is the staple for a variety of post-tree analyses. To fully take advantage of this wealth of data to discover and understand large-scale evolutionary and ecological patterns, computational data integration, i.e., the use of machines to link data at large scale, is crucial. The most common shared entity by which evolutionary and (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  47.  60
    Perfect trees and elementary embeddings.Sy-David Friedman & Katherine Thompson - 2008 - Journal of Symbolic Logic 73 (3):906-918.
    An important technique in large cardinal set theory is that of extending an elementary embedding j: M → N between inner models to an elementary embedding j*: M[G] → N[G*] between generic extensions of them. This technique is crucial both in the study of large cardinal preservation and of internal consistency. In easy cases, such as when forcing to make the GCH hold while preserving a measurable cardinal (via a reverse Easton iteration of α-Cohen forcing for successor cardinals α), the (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  48.  84
    Proofs and Countermodels in Non-Classical Logics.Sara Negri - 2014 - Logica Universalis 8 (1):25-60.
    Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   15 citations  
  49.  32
    Other Proofs of Old Results.Henryk Kotlarski - 1998 - Mathematical Logic Quarterly 44 (4):474-480.
    We transform the proof of the second incompleteness theorem given in [3] to a proof-theoretic version, avoiding the use of the arithmetized completeness theorem. We give also new proofs of old results: The Arithmetical Hierarchy Theorem and Tarski's Theorem on undefinability of truth; the proofs in which the construction of a sentence by means of diagonalization lemma is not needed.
    Direct download  
     
    Export citation  
     
    Bookmark   6 citations  
  50. A new basic set of proof transformations.Anjolina G. de Oliveira & Rjgb de Queiroz - 1997 - Bulletin of Symbolic Logic 3 (1):124-126.
1 — 50 / 970