Switch to: References

Add citations

You must login to add citations.
  1. Non-transitive Correspondence Analysis.Yaroslav Petrukhin & Vasily Shangin - 2023 - Journal of Logic, Language and Information 32 (2):247-273.
    The paper’s novelty is in combining two comparatively new fields of research: non-transitive logic and the proof method of correspondence analysis. To be more detailed, in this paper the latter is adapted to Weir’s non-transitive trivalent logic \({\mathbf{NC}}_{\mathbf{3}}\). As a result, for each binary extension of \({\mathbf{NC}}_{\mathbf{3}}\), we present a sound and complete Lemmon-style natural deduction system. Last, but not least, we stress the fact that Avron and his co-authors’ general method of obtaining _n_-sequent proof systems for any _n_-valent logic (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Herbrand complexity and the epsilon calculus with equality.Kenji Miyamoto & Georg Moser - 2023 - Archive for Mathematical Logic 63 (1):89-118.
    The $$\varepsilon $$ -elimination method of Hilbert’s $$\varepsilon $$ -calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert’s $$\varepsilon $$ -calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Efficient elimination of Skolem functions in $$\text {LK}^\text {h}$$ LK h.Ján Komara - 2022 - Archive for Mathematical Logic 61 (3):503-534.
    We present a sequent calculus with the Henkin constants in the place of the free variables. By disposing of the eigenvariable condition, we obtained a proof system with a strong locality property—the validity of each inference step depends only on its active formulas, not its context. Our major outcomes are: the cut elimination via a non-Gentzen-style algorithm without resorting to regularization and the elimination of Skolem functions with linear increase in the proof length for a subclass of derivations with cuts.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • A Simplified Proof of the Epsilon Theorems.Stefan Hetzl - forthcoming - Review of Symbolic Logic:1-16.
    We formulate Hilbert’s epsilon calculus in the context of expansion proofs. This leads to a simplified proof of the epsilon theorems by disposing of the need for prenexification, Skolemisation, and their respective inverse transformations. We observe that the natural notion of cut in the epsilon calculus is associative.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Epsilon theorems in intermediate logics.Matthias Baaz & Richard Zach - 2022 - Journal of Symbolic Logic 87 (2):682-720.
    Any intermediate propositional logic can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s $\varepsilon $ -calculus. The first and second $\varepsilon $ -theorems for classical logic establish conservativity of the $\varepsilon $ -calculus over its classical base logic. It is well known that the second $\varepsilon $ -theorem fails for the intuitionistic $\varepsilon $ -calculus, as prenexation is impossible. The paper investigates the effect of adding critical $\varepsilon $ - (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • The number of axioms.J. P. Aguilera, M. Baaz & J. Bydžovský - 2022 - Annals of Pure and Applied Logic 173 (5):103078.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•
  • Determinate logic and the Axiom of Choice.J. P. Aguilera - 2020 - Annals of Pure and Applied Logic 171 (2):102745.
    Takeuti introduced an infinitary proof system for determinate logic and showed that for transitive models of Zermelo-Fraenkel set theory with the Axiom of Dependent Choice that contain all reals, the cut-elimination theorem is equivalent to the Axiom of Determinacy, and in particular contradicts the Axiom of Choice. We consider variants of Takeuti's theorem without assuming the failure of the Axiom of Choice. For instance, we show that if one removes atomic formulae of infinite arity from the language of Takeuti's proof (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
    		•