Related

Contents
3037 found
Order:
1 — 50 / 3037
  1. Some proof theoretical remarks on quantification in ordinary language.Michele Abrusci & Christian Retoré - manuscript
    This paper surveys the common approach to quantification and generalised quantification in formal linguistics and philosophy of language. We point out how this general setting departs from empirical linguistic data, and give some hints for a different view based on proof theory, which on many aspects gets closer to the language itself. We stress the importance of Hilbert's oper- ator epsilon and tau for, respectively, existential and universal quantifications. Indeed, these operators help a lot to construct semantic representation close to (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  2. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.Sara Ayhan - manuscript
    In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  3. Computational reverse mathematics and foundational analysis.Benedict Eastaugh - manuscript
    Reverse mathematics studies which subsystems of second order arithmetic are equivalent to key theorems of ordinary, non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of different foundations for mathematics in a formally precise manner. This paper gives a detailed account of the motivations and methodology of foundational analysis, which have heretofore been largely left implicit in the practice. It then shows how this account can be fruitfully applied in the (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  4. The Power of Naive Truth.Hartry Field - manuscript
    While non-classical theories of truth that take truth to be transparent have some obvious advantages over any classical theory that evidently must take it as non-transparent, several authors have recently argued that there's also a big disadvantage of non-classical theories as compared to their “external” classical counterparts: proof-theoretic strength. While conceding the relevance of this, the paper argues that there is a natural way to beef up extant internal theories so as to remove their proof-theoretic disadvantage. It is suggested that (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  5. Harmony, Normality and Stability.Nils Kurbis - manuscript
    The paper begins with a conceptual discussion of Michael Dummett's proof-theoretic justification of deduction or proof-theoretic semantics, which is based on what we might call Gentzen's thesis: 'the introductions constitute, so to speak, the "definitions" of the symbols concerned, and the eliminations are in the end only consequences thereof, which could be expressed thus: In the elimination of a symbol, the formula in question, whose outer symbol it concerns, may only "be used as that which it means on the basis (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  6. A Decision Procedure for Herbrand Formulas without Skolemization.Timm Lampert - manuscript
    This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  7. Cut elimination for systems of transparent truth with restricted initial sequents.Carlo Nicolai - manuscript
    The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  8. On the notion of validity for the bilateral classical logic.Ukyo Suzuki & Yoriyuki Yamagata - manuscript
    This paper considers Rumfitt’s bilateral classical logic (BCL), which is proposed to counter Dummett’s challenge to classical logic. First, agreeing with several authors, we argue that Rumfitt’s notion of harmony, used to justify logical rules by a purely proof theoretical manner, is not sufficient to justify coordination rules in BCL purely proof-theoretically. For the central part of this paper, we propose a notion of proof-theoretical validity similar to Prawitz for BCL and proves that BCL is sound and complete respect to (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  9. Involutive Commutative Residuated Lattice without Unit: Logics and Decidability.Yiheng Wang, Hao Zhan, Yu Peng & Zhe Lin - manuscript
    We investigate involutive commutative residuated lattices without unit, which are commutative residuated lattice-ordered semigroups enriched with a unary involutive negation operator. The logic of this structure is discussed and the Genzten-style sequent calculus of it is presented. Moreover, we prove the decidability of this logic.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  10. One-pass tableaux for computation tree logic.Rajeev Gore - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  11. Classical modal display logic in the calculus of structures and minimal cut-free deep inference calculi for S.Rajeev Gore - manuscript
    Remove from this list  
     
    Export citation  
     
    Bookmark   3 citations  
  12. A cut-free sequent calculus for bi-intuitionistic logic.Rajeev Gore - manuscript
    Remove from this list  
     
    Export citation  
     
    Bookmark   6 citations  
  13. On cut elimination for subsystems of second-order number theory.William Tait - manuscript
    To appear in the Proceedings of Logic Colloquium 2006. (32 pages).
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  14. Proof theory and meaning: On second order logic.Author unknown - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  15. Natural deduction and semantic models of justification logic in the proof assistant Coq.Jesús Mauricio Andrade Guzmán & Francisco Hernández Quiroz - forthcoming - Logic Journal of the IGPL.
    The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  16. Proof-Theoretic Aspects of Paraconsistency with Strong Consistency Operator.Victoria Arce Pistone & Martín Figallo - forthcoming - Studia Logica:1-38.
    In order to develop efficient tools for automated reasoning with inconsistency (theorem provers), eventually making Logics of Formal inconsistency (_LFI_) a more appealing formalism for reasoning under uncertainty, it is important to develop the proof theory of the first-order versions of such _LFI_s. Here, we intend to make a first step in this direction. On the other hand, the logic _Ciore_ was developed to provide new logical systems in the study of inconsistent databases from the point of view of _LFI_s. (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  17. Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations.Sara Ayhan - forthcoming - Journal of Logic and Computation.
    In this paper I will develop a lambda-term calculus, lambda-2Int, for a bi-intuitionistic logic and discuss its implications for the notions of sense and denotation of derivations in a bilateralist setting. Thus, I will use the Curry-Howard correspondence, which has been well-established between the simply typed lambda-calculus and natural deduction systems for intuitionistic logic, and apply it to a bilateralist proof system displaying two derivability relations, one for proving and one for refuting. The basis will be the natural deduction system (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  18. How Much Propositional Logic Suffices for Rosser’s Essential Undecidability Theorem?Guillermo Badia, Petr Cintula, Petr Hajek & Andrew Tedder - forthcoming - Review of Symbolic Logic:1-18.
    In this paper we explore the following question: how weak can a logic be for Rosser's essential undecidability result to be provable for a weak arithmetical theory? It is well known that Robinson's Q is essentially undecidable in intuitionistic logic, and P. Hajek proved it in the fuzzy logic BL for Grzegorczyk's variant of Q which interprets the arithmetic operations as non-total non-functional relations. We present a proof of essential undecidability in a much weaker substructural logic and for a much (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  19. Halin’s infinite ray theorems: Complexity and reverse mathematics.James S. Barnes, Jun Le Goh & Richard A. Shore - forthcoming - Journal of Mathematical Logic.
    Halin in 1965 proved that if a graph has [Formula: see text] many pairwise disjoint rays for each [Formula: see text] then it has infinitely many pairwise disjoint rays. We analyze the complexity of this and other similar results in terms of computable and proof theoretic complexity. The statement of Halin’s theorem and the construction proving it seem very much like standard versions of compactness arguments such as König’s Lemma. Those results, while not computable, are relatively simple. They only use (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  20. Peirce’s Triadic Logic and Its (Overlooked) Connexive Expansion.Alex Belikov - forthcoming - Logic and Logical Philosophy:1.
    In this paper, we present two variants of Peirce’s Triadic Logic within a language containing only conjunction, disjunction, and negation. The peculiarity of our systems is that conjunction and disjunction are interpreted by means of Peirce’s mysterious binary operations Ψ and Φ from his ‘Logical Notebook’. We show that semantic conditions that can be extracted from the definitions of Ψ and Φ agree (in some sense) with the traditional view on the semantic conditions of conjunction and disjunction. Thus, we support (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  21. The subformula property of natural deduction derivations and analytic cuts.Mirjana Borisavljević - forthcoming - Logic Journal of the IGPL.
    In derivations of a sequent system, $\mathcal{L}\mathcal{J}$, and a natural deduction system, $\mathcal{N}\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\mathcal{N}\mathcal{J}$ and $\mathcal{L}\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\mathcal{N}\mathcal{J}$-derivation is normal $\Longleftrightarrow $ it has the subformula property based on trails $\Longleftrightarrow $ its $g$-image in $\mathcal{L}\mathcal{J}$ is without maximum cuts $\Longrightarrow $ that $g$-image has the subformula property based (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  22. Simplified gentzenizations for contraction-less logics.Ross T. Brady - forthcoming - Logique Et Analyse.
    Remove from this list  
     
    Export citation  
     
    Bookmark   4 citations  
  23. Transmission of Verification.Ethan Brauer & Neil Tennant - forthcoming - Review of Symbolic Logic:1-16.
    This paper clarifies, revises, and extends the account of the transmission of truthmakers by core proofs that was set out in chap. 9 of Tennant. Brauer provided two kinds of example making clear the need for this. Unlike Brouwer’s counterexamples to excluded middle, the examples of Brauer that we are dealing with here establish the need for appeals to excluded middle when applying, to the problem of truthmaker-transmission, the already classical metalinguistic theory of model-relative evaluations.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  24. Categorical Quantification.Constantin C. Brîncuș - forthcoming - Bulletin of Symbolic Logic:1-27.
    Due to Gӧdel’s incompleteness results, the categoricity of a sufficiently rich mathematical theory and the semantic completeness of its underlying logic are two mutually exclusive ideals. For first- and second-order logics we obtain one of them with the cost of losing the other. In addition, in both these logics the rules of deduction for their quantifiers are non-categorical. In this paper I examine two recent arguments –Warren (2020), Murzi and Topey (2021)– for the idea that the natural deduction rules for (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  25. Inferential Quantification and the ω-rule.Constantin C. Brîncuș - forthcoming - In Antonio D’Aragona (ed.), Perspectives on Deduction.
    Logical inferentialism maintains that the formal rules of inference fix the meanings of the logical terms. The categoricity problem points out to the fact that the standard formalizations of classical logic do not uniquely determine the intended meanings of its logical terms, i.e., these formalizations are not categorical. This means that there are different interpretations of the logical terms that are consistent with the relation of logical derivability in a logical calculus. In the case of the quantificational logic, the categoricity (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  26. Non-reflexive Nonsense: Proof-Theory for Paracomplete Weak Kleene Logic.Bruno da Re, Damian Szmuc & M. Ines Corbalan - forthcoming - Studia Logica.
    Our aim is to provide a sequent calculus whose external consequence relation coincides with the three-valued paracomplete logic `of nonsense' introduced by Dmitry Bochvar and, independently, presented as the weak Kleene logic K3W by Stephen C. Kleene. The main features of this calculus are (i) that it is non-reflexive, i.e., Identity is not included as an explicit rule (although a restricted form of it with premises is derivable); (ii) that it includes rules where no variable-inclusion conditions are attached; and (iii) (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  27. Normal Proofs and Tableaux for the Font-Rius Tetravalent Modal Logic.Marcelo E. Coniglio & Martin Figallo - forthcoming - Logic and Logical Philosophy:1-33.
    Tetravalent modal logic (TML) was introduced by Font and Rius in 2000. It is an expansion of the Belnap-Dunn four-valued logic FOUR, a logical system that is well-known for the many applications found in several fields. Besides, TML is the logic that preserves degrees of truth with respect to Monteiro’s tetravalent modal algebras. Among other things, Font and Rius showed that TML has a strongly adequate sequent system, but unfortunately this system does not enjoy the cut-elimination property. However, in a (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  28. Intuitionistic Logic is a Connexive Logic.Davide Fazio, Antonio Ledda & Francesco Paoli - forthcoming - Studia Logica:1-45.
    We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic ($$\textrm{CHL}$$ CHL ), hereby introduced as an example of a strongly connexive logic with an intuitive semantics. We use the reverse algebraisation paradigm: $$\textrm{CHL}$$ CHL is presented as the assertional logic of a point regular variety (whose structure theory is examined in detail) that turns out to be term equivalent to the variety of Heyting algebras. We provide Hilbert-style and Gentzen-style proof systems for $$\textrm{CHL}$$ CHL ; moreover, we (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  29. A Poly-Connexive Logic.Nissim Francez - forthcoming - Logic and Logical Philosophy:1.
    The paper introduces a variant of connexive logic in which connexivity is extended from the interaction of negation with implication to the interaction of negation also with conjunction and disjunction. The logic is presented by two deductively equivalent methods: an axiomatic one and a natural-deduction one. Both are shown to be complete for a four-valued model theory.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  30. Comparing Calculi for First-Order Infinite-Valued Łukasiewicz Logic and First-Order Rational Pavelka Logic.Alexander S. Gerasimov - forthcoming - Logic and Logical Philosophy:1-50.
    We consider first-order infinite-valued Łukasiewicz logic and its expansion, first-order rational Pavelka logic RPL∀. From the viewpoint of provability, we compare several Gentzen-type hypersequent calculi for these logics with each other and with Hájek’s Hilbert-type calculi for the same logics. To facilitate comparing previously known calculi for the logics, we define two new analytic calculi for RPL∀ and include them in our comparison. The key part of the comparison is a density elimination proof that introduces no cuts for one of (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  31. The Truth Table Formulation of Propositional Logic.Tristan Grøtvedt Haze - forthcoming - Teorema: International Journal of Philosophy.
    Developing a suggestion of Wittgenstein, I provide an account of truth tables as formulas of a formal language. I define the syntax and semantics of TPL (the language of Tabular Propositional Logic), and develop its proof theory. Single formulas of TPL, and finite groups of formulas with the same top row and TF matrix (depiction of possible valuations), are able to serve as their own proofs with respect to metalogical properties of interest. The situation is different, however, for groups of (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  32. Fregean Description Theory in Proof-Theoretical Setting.Andrzej Indrzejczak - forthcoming - Logic and Logical Philosophy:1.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  33. A Natural Deduction System for Orthomodular Logic.Andre Kornell - forthcoming - Review of Symbolic Logic:1-38.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  34. The Turing Degrees and Keisler’s Order.Maryanthe Malliaris & Saharon Shelah - forthcoming - Journal of Symbolic Logic:1-11.
    There is a Turing functional $\Phi $ taking $A^\prime $ to a theory $T_A$ whose complexity is exactly that of the jump of A, and which has the property that $A \leq _T B$ if and only if $T_A \trianglelefteq T_B$ in Keisler’s order. In fact, by more elaborate means and related theories, we may keep the complexity at the level of A without using the jump.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35. Ontological Purity for Formal Proofs.Robin Martinot - forthcoming - Review of Symbolic Logic:1-40.
    Purity is known as an ideal of proof that restricts a proof to notions belonging to the ‘content’ of the theorem. In this paper, our main interest is to develop a conception of purity for formal (natural deduction) proofs. We develop two new notions of purity: one based on an ontological notion of the content of a theorem, and one based on the notions of surrogate ontological content and structural content. From there, we characterize which (classical) first-order natural deduction proofs (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  36. Paraconsistent logic and query answering in inconsistent databases.C. A. Middelburg - forthcoming - Journal of Applied Non-Classical Logics:1-22.
    This paper concerns the paraconsistent logic LPQ⊃,F and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among other things the definition of a consistent answer to a query with respect to a possibly inconsistent database without resort to database (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  37. Binary Kripke Semantics for a Strong Logic for Naive Truth.Ben Middleton - forthcoming - Review of Symbolic Logic:1-25.
    I show that the logic $\textsf {TJK}^{d+}$, one of the strongest logics currently known to support the naive theory of truth, is obtained from the Kripke semantics for constant domain intuitionistic logic by dropping the requirement that the accessibility relation is reflexive and only allowing reflexive worlds to serve as counterexamples to logical consequence. In addition, I provide a simplified natural deduction system for $\textsf {TJK}^{d+}$, in which a restricted form of conditional proof is used to establish conditionals.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  38. Natural deduction and normal form for intuitionistic linear logic.S. Negri - forthcoming - Archive for Mathematical Logic.
    Remove from this list  
     
    Export citation  
     
    Bookmark   3 citations  
  39. A Note on the Sequent Calculi G3[mic]=.F. Parlamento & F. Previale - forthcoming - Review of Symbolic Logic:1-18.
  40. The Elimination of Atomic Cuts and the Semishortening Property for Gentzen’s Sequent Calculus with Equality.F. Parlamento & F. Previale - forthcoming - Review of Symbolic Logic:1-32.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  41. The first-order logic of CZF is intuitionistic first-order logic.Robert Passmann - forthcoming - Journal of Symbolic Logic:1-23.
    We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42. Dialogue Games for Minimal Logic.Alexandra Pavlova - forthcoming - Logic and Logical Philosophy:1.
    In this paper, we define a class of dialogue games for Johansson’s minimal logic and prove that it corresponds to the validity of minimal logic. Many authors have stated similar results for intuitionistic and classical logic either with or without actually proving the correspondence. Rahman, Clerbout and Keiff [17] have already specified dialogues for minimal logic; however, they transformed it into Fitch-style natural deduction only. We propose a different specification for minimal logic with the proof of correspondence between the existence (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  43. Is Cantor’s Theorem a Dialetheia? Variations on a Paraconsistent Approach to Cantor’s Theorem.Uwe Petersen - forthcoming - Review of Symbolic Logic:1-18.
    The present note was prompted by Weber’s approach to proving Cantor’s theorem, i.e., the claim that the cardinality of the power set of a set is always greater than that of the set itself. While I do not contest that his proof succeeds, my point is that he neglects the possibility that by similar methods it can be shown also that no non-empty set satisfies Cantor’s theorem. In this paper unrestricted abstraction based on a cut free Gentzen type sequential calculus (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  44. Logical metatheorems for accretive and (generalized) monotone set-valued operators.Nicholas Pischke - forthcoming - Journal of Mathematical Logic.
    Accretive and monotone operator theory are central branches of nonlinear functional analysis and constitute the abstract study of certain set-valued mappings between function spaces. This paper deals with the computational properties of these accretive and (generalized) monotone set-valued operators. In particular, we develop (and extend) for this field the theoretical framework of proof mining, a program in mathematical logic that seeks to extract computational information from prima facie “non-computational” proofs from the mainstream literature. To this end, we establish logical metatheorems (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  45. Logics of upsets of De Morgan lattices.Adam Přenosil - forthcoming - Mathematical Logic Quarterly.
    We study logics determined by matrices consisting of a De Morgan lattice with an upward closed set of designated values, such as the logic of non‐falsity preservation in a given finite Boolean algebra and Shramko's logic of non‐falsity preservation in the four‐element subdirectly irreducible De Morgan lattice. The key tool in the study of these logics is the lattice‐theoretic notion of an n‐filter. We study the logics of all (complete, consistent, and classical) n‐filters on De Morgan lattices, which are non‐adjunctive (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  46. Substructural Logics.Greg Restall - forthcoming - Stanford Encyclopedia of Philosophy.
    summary of work in relevant in the Anderson– tradition.]; Mares Troestra, Anne, 1992, Lectures on , CSLI Publications [A quick, easy-to.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  47. Against Harmony.Ian Rumfitt - forthcoming - In Bob Hale, Crispin Wright & Alexander Miller (eds.), The Blackwell Companion to the Philosophy of Language. Blackwell.
    Many prominent writers on the philosophy of logic, including Michael Dummett, Dag Prawitz, Neil Tennant, have held that the introduction and elimination rules of a logical connective must be ‘in harmony ’ if the connective is to possess a sense. This Harmony Thesis has been used to justify the choice of logic: in particular, supposed violations of it by the classical rules for negation have been the basis for arguments for switching from classical to intuitionistic logic. The Thesis has also (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  48. Proof-Theoretic Semantics.Peter Schroeder-Heister - forthcoming - Stanford Encyclopedia of Philosophy.
  49. Almost Theorems of Hyperarithmetic Analysis.Richard A. Shore - forthcoming - Journal of Symbolic Logic:1-33.
    Theorems of hyperarithmetic analysis (THAs) occupy an unusual neighborhood in the realms of reverse mathematics and recursion theoretic complexity. They lie above all the fixed (recursive) iterations of the Turing Jump but below ATR $_{0}$ (and so $\Pi _{1}^{1}$ -CA $_{0}$ or the hyperjump). There is a long history of proof theoretic principles which are THAs. Until Barnes, Goh, and Shore [ta] revealed an array of theorems in graph theory living in this neighborhood, there was only one mathematical denizen. In (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  50. Natural formalization: Deriving the Cantor-Bernstein theorem in zf.Wilfried Sieg & Patrick Walsh - forthcoming - Review of Symbolic Logic:1-44.
    Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
1 — 50 / 3037