Results for 'formal proof'

998 found
Order:
  1. Deductively Sound Formal Proofs.P. Olcott - manuscript
    Could the intersection of [formal proofs of mathematical logic] and [sound deductive inference] specify formal systems having [deductively sound formal proofs of mathematical logic]? All that we have to do to provide [deductively sound formal proofs of mathematical logic] is select the subset of conventional [formal proofs of mathematical logic] having true premises and now we have [deductively sound formal proofs of mathematical logic].
    Download  
     
    Export citation  
     
    Bookmark  
  2. A Pre-formal Proof of Why No Planar Map Needs More Than Four Colours.Bhupinder Singh Anand - manuscript
    Although the Four Colour Theorem is passe, we give an elementary pre-formal proof that transparently illustrates why four colours suffice to chromatically differentiate any set of contiguous, simply connected and bounded, planar spaces; by showing that there is no minimal 4-coloured planar map M. We note that such a pre-formal proof of the Four Colour Theorem highlights the significance of differentiating between: (a) Plato's knowledge as justified true belief, which seeks a formal proof in (...)
    Download  
     
    Export citation  
     
    Bookmark  
  3. An Elementary, Pre-formal, Proof of FLT: Why is x^n+y^n=z^n solvable only for n<3?Bhupinder Singh Anand - manuscript
    Andrew Wiles' analytic proof of Fermat's Last Theorem FLT, which appeals to geometrical properties of real and complex numbers, leaves two questions unanswered: (i) What technique might Fermat have used that led him to, even if only briefly, believe he had `a truly marvellous demonstration' of FLT? (ii) Why is x^n+y^n=z^n solvable only for n<3? In this inter-disciplinary perspective, we offer insight into, and answers to, both queries; yielding a pre-formal proof of why FLT can be treated (...)
    Download  
     
    Export citation  
     
    Bookmark  
  4. Formal logic: Classical problems and proofs.Luis M. Augusto - 2019 - London, UK: College Publications.
    Not focusing on the history of classical logic, this book provides discussions and quotes central passages on its origins and development, namely from a philosophical perspective. Not being a book in mathematical logic, it takes formal logic from an essentially mathematical perspective. Biased towards a computational approach, with SAT and VAL as its backbone, this is an introduction to logic that covers essential aspects of the three branches of logic, to wit, philosophical, mathematical, and computational.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  98
    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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  6. Proof Theory of Finite-valued Logics.Richard Zach - 1993 - Dissertation, Technische Universität Wien
    The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of (...)
    Download  
     
    Export citation  
     
    Bookmark   17 citations  
  7. Truth, Proof and Gödelian Arguments: A Defence of Tarskian Truth in Mathematics.Markus Pantsar - 2009 - Dissertation, University of Helsinki
    One of the most fundamental questions in the philosophy of mathematics concerns the relation between truth and formal proof. The position according to which the two concepts are the same is called deflationism, and the opposing viewpoint substantialism. In an important result of mathematical logic, Kurt Gödel proved in his first incompleteness theorem that all consistent formal systems containing arithmetic include sentences that can neither be proved nor disproved within that system. However, such undecidable Gödel sentences can (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  8. A formalization of kant’s transcendental logic.Theodora Achourioti & Michiel van Lambalgen - 2011 - Review of Symbolic Logic 4 (2):254-289.
    Although Kant (1998) envisaged a prominent role for logic in the argumentative structure of his Critique of Pure Reason, logicians and philosophers have generally judged Kantgeneralformaltranscendental logics is a logic in the strict formal sense, albeit with a semantics and a definition of validity that are vastly more complex than that of first-order logic. The main technical application of the formalism developed here is a formal proof that Kants logic is after all a distinguished subsystem of first-order (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  9. Pregeometry, Formal Language and Constructivist Foundations of Physics.Xerxes D. Arsiwalla, Hatem Elshatlawy & Dean Rickles - manuscript
    How does one formalize the structure of structures necessary for the foundations of physics? This work is an attempt at conceptualizing the metaphysics of pregeometric structures, upon which new and existing notions of quantum geometry may find a foundation. We discuss the philosophy of pregeometric structures due to Wheeler, Leibniz as well as modern manifestations in topos theory. We draw attention to evidence suggesting that the framework of formal language, in particular, homotopy type theory, provides the conceptual building blocks (...)
    Download  
     
    Export citation  
     
    Bookmark  
  10. Proofs, necessity and causality.Srećko Kovač - 2019 - In Enrique Alonso, Antonia Huertas & Andrei Moldovan (eds.), Aventuras en el Mundo de la Lógica: Ensayos en Honor a María Manzano. College Publications. pp. 239-263.
    There is a long tradition of logic, from Aristotle to Gödel, of understanding a proof from the concepts of necessity and causality. Gödel's attempts to define provability in terms of necessity led him to the distinction of formal and absolute (abstract) provability. Turing's definition of mechanical procedure by means of a Turing machine (TM) and Gödel's definition of a formal system as a mechanical procedure for producing formulas prompt us to understand formal provability as a mechanical (...)
    Download  
     
    Export citation  
     
    Bookmark  
  11. Formalization and infinity.André Porto - 2008 - Manuscrito 31 (1):25-43.
    This article discusses some of Chateaubriand’s views on the connections between the ideas of formalization and infinity, as presented in chapters 19 and 20 of Logical Forms. We basically agree with his criticisms of the standard construal of these connections, a view we named “formal proofs as ultimate provings”, but we suggest an alternative way of picturing that connection based on some ideas of the late Wittgenstein.
    Download  
     
    Export citation  
     
    Bookmark  
  12. Proof phenomenon as a function of the phenomenology of proving.Inês Hipólito - 2015 - Progress in Biophysics and Molecular Biology 119:360-367.
    Kurt Gödel wrote (1964, p. 272), after he had read Husserl, that the notion of objectivity raises a question: “the question of the objective existence of the objects of mathematical intuition (which, incidentally, is an exact replica of the question of the objective existence of the outer world)”. This “exact replica” brings to mind the close analogy Husserl saw between our intuition of essences in Wesensschau and of physical objects in perception. What is it like to experience a mathematical proving (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  13. Co-constructive logic for proofs and refutations.James Trafford - 2014 - Studia Humana 3 (4):22-40.
    This paper considers logics which are formally dual to intuitionistic logic in order to investigate a co-constructive logic for proofs and refutations. This is philosophically motivated by a set of problems regarding the nature of constructive truth, and its relation to falsity. It is well known both that intuitionism can not deal constructively with negative information, and that defining falsity by means of intuitionistic negation leads, under widely-held assumptions, to a justification of bivalence. For example, we do not want to (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  14. Cantor’s Proof in the Full Definable Universe.Laureano Luna & William Taylor - 2010 - Australasian Journal of Logic 9:10-25.
    Cantor’s proof that the powerset of the set of all natural numbers is uncountable yields a version of Richard’s paradox when restricted to the full definable universe, that is, to the universe containing all objects that can be defined not just in one formal language but by means of the full expressive power of natural language: this universe seems to be countable on one account and uncountable on another. We argue that the claim that definitional contexts impose restrictions (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  15. Proofs are Programs: 19th Century Logic and 21st Century Computing.Philip Wadler - manuscript
    As the 19th century drew to a close, logicians formalized an ideal notion of proof. They were driven by nothing other than an abiding interest in truth, and their proofs were as ethereal as the mind of God. Yet within decades these mathematical abstractions were realized by the hand of man, in the digital stored-program computer. How it came to be recognized that proofs and programs are the same thing is a story that spans a century, a chase with (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  16. A Henkin-style completeness proof for the modal logic S5.Bruno Bentzen - 2021 - In Pietro Baroni, Christoph Benzmüller & Yì N. Wáng (eds.), Logic and Argumentation: Fourth International Conference, CLAR 2021, Hangzhou, China, October 20–22. Springer. pp. 459-467.
    This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to that of Hughes and Cresswell, but the system, based on a different choice of axioms, is better described as a Mendelson system augmented with axiom schemes for K, T, S4, and B, and the necessitation rule as a rule of inference. The language has the false and implication as the only (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  17. Formal Background for the Incompleteness and Undefinability Theorems.Richard Kimberly Heck - manuscript
    A teaching document I've used in my courses on truth and on incompleteness. Aimed at students who have a good grasp of basic logic, and decent math skills, it attempts to give them the background they need to understand a proper statement of the classic results due to Gödel and Tarski, and sketches their proofs. Topics covered include the notions of language and theory, the basics of formal syntax and arithmetization, formal arithmetic (Q and PA), representability, diagonalization, and (...)
    Download  
     
    Export citation  
     
    Bookmark  
  18. Expressing Truth directly within a formal system with no need for model theory.Pete Olcott - manuscript
    Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to deductive conclusions without any need for other representations.
    Download  
     
    Export citation  
     
    Bookmark  
  19. Truth and Proof without Models: A Development and Justification of the Truth-valuational Approach (2nd edition).Hanoch Ben-Yami - manuscript
    I explain why model theory is unsatisfactory as a semantic theory and has drawbacks as a tool for proofs on logic systems. I then motivate and develop an alternative, the truth-valuational substitutional approach (TVS), and prove with it the soundness and completeness of the first order Predicate Calculus with identity and of Modal Propositional Calculus. Modal logic is developed without recourse to possible worlds. Along the way I answer a variety of difficulties that have been raised against TVS and show (...)
    Download  
     
    Export citation  
     
    Bookmark  
  20. Sense and Proof.Carlo Penco & Daniele Porello - 2010 - In M. D'agostino, G. Giorello, F. Laudisa, T. Pievani & C. Sinigaglia (eds.), New Essays in Logic and Philosophy of Science,. College Publicationss.
    In this paper we give some formal examples of ideas developed by Penco in two papers on the tension inside Frege's notion of sense (see Penco 2003). The paper attempts to compose the tension between semantic and cognitive aspects of sense, through the idea of sense as proof or procedure – not as an alternative to the idea of sense as truth condition, but as complementary to it (as it happens sometimes in the old tradition of procedural semantics).
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  21. Eliminating Undecidability and Incompleteness in Formal Systems.Pete Olcott - manuscript
    To eliminate incompleteness, undecidability and inconsistency from formal systems we only need to convert the formal proofs to theorem consequences of symbolic logic to conform to the sound deductive inference model. -/- Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) thus unlike the formal proofs of symbolic logic provability cannot diverge from truth.
    Download  
     
    Export citation  
     
    Bookmark  
  22. Wittgenstein on Gödelian 'Incompleteness', Proofs and Mathematical Practice: Reading Remarks on the Foundations of Mathematics, Part I, Appendix III, Carefully.Wolfgang Kienzler & Sebastian Sunday Grève - 2016 - In Sebastian Sunday Grève & Jakub Mácha (eds.), Wittgenstein and the Creativity of Language. Basingstoke, UK: Palgrave Macmillan. pp. 76-116.
    We argue that Wittgenstein’s philosophical perspective on Gödel’s most famous theorem is even more radical than has commonly been assumed. Wittgenstein shows in detail that there is no way that the Gödelian construct of a string of signs could be assigned a useful function within (ordinary) mathematics. — The focus is on Appendix III to Part I of Remarks on the Foundations of Mathematics. The present reading highlights the exceptional importance of this particular set of remarks and, more specifically, emphasises (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  23. Halting Problem Proof from Finite Strings to Final States.Pete Olcott - manuscript
    If there truly is a proof that shows that no universal halt decider exists on the basis that certain tuples: (H, Wm, W) are undecidable, then this very same proof (implemented as a Turing machine) could be used by H to reject some of its inputs. When-so-ever the hypothetical halt decider cannot derive a formal proof from its input strings and initial state to final states corresponding the mathematical logic functions of Halts(Wm, W) or Loops(Wm, W), (...)
    Download  
     
    Export citation  
     
    Bookmark  
  24. Proof that Wittgenstein is correct about Gödel.P. Olcott - manuscript
    The conventional notion of a formal system is adapted to conform to the sound deductive inference model operating on finite strings. Finite strings stipulated to have the semantic property of Boolean true provide the sound deductive premises. Truth preserving finite string transformation rules provide valid the deductive inference. Conclusions of sound arguments are derived from truth preserving finite string transformations applied to true premises.
    Download  
     
    Export citation  
     
    Bookmark  
  25. ‘Sometime a paradox’, now proof: Yablo is not first order.Saeed Salehi - 2022 - Logic Journal of the IGPL 30 (1):71-77.
    Interesting as they are by themselves in philosophy and mathematics, paradoxes can be made even more fascinating when turned into proofs and theorems. For example, Russell’s paradox, which overthrew Frege’s logical edifice, is now a classical theorem in set theory, to the effect that no set contains all sets. Paradoxes can be used in proofs of some other theorems—thus Liar’s paradox has been used in the classical proof of Tarski’s theorem on the undefinability of truth in sufficiently rich languages. (...)
    Download  
     
    Export citation  
     
    Bookmark  
  26. On Stage One of Feser's 'Aristotelian Proof'.Graham Oppy - 2021 - Religious Studies 57:491-502.
    Feser (2017) presents and defends five proofs of the existence of God. Each proof is in two stages: the first stage proves the existence of something which, in the second stage, is shown to possess an appropriate range of divine attributes. Each proof is given two presentations, one informal and one formal. In this paper, I critically examine two premises from one of Feser's five first stage proofs. I provide reasons for thinking that naturalists reject both of (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  27. Modal collapse in Gödel's ontological proof.Srećko Kovač - 2012 - In Miroslaw Szatkowski (ed.), Ontological Proofs Today. Ontos Verlag. pp. 50--323.
    After introductory reminder of and comments on Gödel’s ontological proof, we discuss the collapse of modalities, which is provable in Gödel’s ontological system GO. We argue that Gödel’s texts confirm modal collapse as intended consequence of his ontological system. Further, we aim to show that modal collapse properly fits into Gödel’s philosophical views, especially into his ontology of separation and union of force and fact, as well as into his cosmological theory of the nonobjectivity of the lapse of time. (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  28. The Non-categoricity of Logic (I). The Problem of a Full Formalization (in Romanian).Constantin C. Brîncuș - 1956 - In Henri Wald & Academia Republicii Populare Romîne (eds.), Probleme de Logica. Editura Academiei Republicii Populare Romîne. pp. 137-156.
    A system of logic usually comprises a language for which a model-theory and a proof-theory are defined. The model-theory defines the semantic notion of model-theoretic logical consequence (⊨), while the proof-theory defines the proof- theoretic notion of logical consequence (or logical derivability, ⊢). If the system in question is sound and complete, then the two notions of logical consequence are extensionally equivalent. The concept of full formalization is a more restrictive one and requires in addition the preservation (...)
    Download  
     
    Export citation  
     
    Bookmark  
  29. Purity in Arithmetic: some Formal and Informal Issues.Andrew Arana - 2014 - In Godehard Link (ed.), Formalism and Beyond: On the Nature of Mathematical Discourse. Boston: De Gruyter. pp. 315-336.
    Over the years many mathematicians have voiced a preference for proofs that stay “close” to the statements being proved, avoiding “foreign”, “extraneous”, or “remote” considerations. Such proofs have come to be known as “pure”. Purity issues have arisen repeatedly in the practice of arithmetic; a famous instance is the question of complex-analytic considerations in the proof of the prime number theorem. This article surveys several such issues, and discusses ways in which logical considerations shed light on these issues.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  30. The Notion of Truth in Natural and Formal Languages.Pete Olcott - manuscript
    For any natural (human) or formal (mathematical) language L we know that an expression X of language L is true if and only if there are expressions Γ of language L that connect X to known facts. -/- By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that evaluate to neither True nor False.
    Download  
     
    Export citation  
     
    Bookmark  
  31. forall x: Calgary. An Introduction to Formal Logic (4th edition).P. D. Magnus, Tim Button, Robert Trueman, Richard Zach & Aaron Thomas-Bolduc - 2023 - Calgary: Open Logic Project.
    forall x: Calgary is a full-featured textbook on formal logic. It covers key notions of logic such as consequence and validity of arguments, the syntax of truth-functional propositional logic TFL and truth-table semantics, the syntax of first-order (predicate) logic FOL with identity (first-order interpretations), symbolizing English in TFL and FOL, and Fitch-style natural deduction proof systems for both TFL and FOL. It also deals with some advanced topics such as modal logic, soundness, and functional completeness. Exercises with solutions (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  32. Philosophy of Logic – Reexamining the Formalized Notion of Truth.Pete Olcott - manuscript
    Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to true conclusions without any need for other representations such as model theory.
    Download  
     
    Export citation  
     
    Bookmark  
  33. Philosophy of Logic – Reexamining the Formalized Notion of Truth.Pete Olcott - manuscript
    Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language. -/- The only thing required to eliminate incompleteness, undecidability and inconsistency from formal systems is transforming the formal proofs of symbolic logic to use the sound deductive inference model.
    Download  
     
    Export citation  
     
    Bookmark  
  34. Two Types of Ontological Frame and Gödel’s Ontological Proof.Sergio Galvan - 2012 - European Journal for Philosophy of Religion 4 (2):147--168.
    The aim of this essay is twofold. First, it outlines the concept of ontological frame. Secondly, two models are distinguished on this structure. The first one is connected to Kant’s concept of possible object and the second one relates to Leibniz’s. Leibniz maintains that the source of possibility is the mere logical consistency of the notions involved, so that possibility coincides with analytical possibility. Kant, instead, argues that consistency is only a necessary component of possibility. According to Kant, something is (...)
    Download  
     
    Export citation  
     
    Bookmark  
  35. starting rational reconstruction of Spinoza's metaphysics by "a formal analogy to elements of 'de deo' (E1)".Friedrich Wilhelm Grafe - 2020 - Archive.Org.
    We aim to compile some means for a rational reconstruction of a named part of the start-over of Baruch (Benedictus) de Spinoza's metaphysics in 'de deo' (which is 'pars prima' of the 'ethica, ordine geometrico demonstrata' ) in terms of 1st order model theory. In so far, as our approach will be judged successful, it may, besides providing some help in understanding Spinoza, also contribute to the discussion of some or other philosophical evergreen, e.g. 'ontological commitment'. For this text we (...)
    Download  
     
    Export citation  
     
    Bookmark  
  36. forall x: An introduction to formal logic.P. D. Magnus - 2005 - Victoria, BC, Canada: State University of New York Oer Services.
    An introduction to sentential logic and first-order predicate logic with identity, logical systems that significantly influenced twentieth-century analytic philosophy. After working through the material in this book, a student should be able to understand most quantified expressions that arise in their philosophical reading. -/- This books treats symbolization, formal semantics, and proof theory for each language. The discussion of formal semantics is more direct than in many introductory texts. Although forall x does not contain proofs of soundness (...)
    Download  
     
    Export citation  
     
    Bookmark  
  37. Does the Principle of Compositionality Explain Productivity? For a Pluralist View of the Role of Formal Languages as Models.Ernesto Perini-Santos - 2017 - Contexts in Philosophy 2017 - CEUR Workshop Proceedings.
    One of the main motivations for having a compositional semantics is the account of the productivity of natural languages. Formal languages are often part of the account of productivity, i.e., of how beings with finite capaci- ties are able to produce and understand a potentially infinite number of sen- tences, by offering a model of this process. This account of productivity con- sists in the generation of proofs in a formal system, that is taken to represent the way (...)
    Download  
     
    Export citation  
     
    Bookmark  
  38. Deepening the Automated Search for Gödel's Proofs.Adam Conkey - unknown
    Gödel's incompleteness theorems establish the stunning result that mathematics cannot be fully formalized and, further, that any formal system containing a modicum of number or set theory cannot establish its own consistency. Wilfried Sieg and Clinton Field, in their paper Automated Search for Gödel's Proofs, presented automated proofs of Gödel's theorems at an abstract axiomatic level; they used an appropriate expansion of the strategic considerations that guide the search of the automated theorem prover AProS. The representability conditions that allow (...)
    Download  
     
    Export citation  
     
    Bookmark  
  39. How to Say Things with Formalisms.David Auerbach - 1992 - In Michael Detlefsen (ed.), Proof, Logic, and Formalization. Routledge. pp. 77--93.
    Recent attention to "self-consistent" (Rosser-style) systems raises anew the question of the proper interpretation of the Gödel Second Incompleteness Theorem and its effect on Hilbert's Program. The traditional rendering and consequence is defended with new arguments justifying the intensional correctness of the derivability conditions.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  40. What is Mathematical Rigor?John Burgess & Silvia De Toffoli - 2022 - Aphex 25:1-17.
    Rigorous proof is supposed to guarantee that the premises invoked imply the conclusion reached, and the problem of rigor may be described as that of bringing together the perspectives of formal logic and mathematical practice on how this is to be achieved. This problem has recently raised a lot of discussion among philosophers of mathematics. We survey some possible solutions and argue that failure to understand its terms properly has led to misunderstandings in the literature.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  41. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark  
  42. The Faithfulness Problem.Mario Bacelar Valente - 2022 - Principia: An International Journal of Epistemology 26 (3):429-447.
    When adopting a sound logical system, reasonings made within this system are correct. The situation with reasonings expressed, at least in part, with natural language is much more ambiguous. One way to be certain of the correctness of these reasonings is to provide a logical model of them. To conclude that a reasoning process is correct we need the logical model to be faithful to the reasoning. In this case, the reasoning inherits, so to speak, the correctness of the logical (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  43. Propositional Logic – A Primer.Leslie Allan - manuscript
    This tutorial is for beginners wanting to learn the basics of propositional logic; the simplest of the formal systems of logic. Leslie Allan introduces students to the nature of arguments, validity, formal proofs, logical operators and rules of inference. With many examples, Allan shows how these concepts are employed through the application of three different methods for proving the formal validity of arguments.
    Download  
     
    Export citation  
     
    Bookmark  
  44. Working Backwards with Copi's Inference Rules.Robert Allen - 1996 - American Philosophical Association Journal on Teaching Philosophy 95 (Spring):103-104.
    In their Introduction to Logic, Copi and Cohen suggest that students construct a formal proof by "working backwards from the conclusion by looking for some statement or statements from which it can be deduced and then trying to deduce those intermediate statements from the premises. What follows is an elaboration of this suggestion. I describe an almost mechanical procedure for determining from which statement(s) the conclusion can be deduced and the rules by which the required inferences can be (...)
    Download  
     
    Export citation  
     
    Bookmark  
  45. The Prolog Inference Model refutes Tarski Undefinability.Pete Olcott - manuscript
    The generalized conclusion of the Tarski and Gödel proofs: All formal systems of greater expressive power than arithmetic necessarily have undecidable sentences. Is not the immutable truth that Tarski made it out to be it is only based on his starting assumptions. -/- When we reexamine these starting assumptions from the perspective of the philosophy of logic we find that there are alternative ways that formal systems can be defined that make undecidability inexpressible in all of these (...) systems. (shrink)
    Download  
     
    Export citation  
     
    Bookmark  
  46. Aggregating sets of judgments: An impossibility result.Christian List & Philip Pettit - 2002 - Economics and Philosophy 18 (1):89-110.
    Suppose that the members of a group each hold a rational set of judgments on some interconnected questions, and imagine that the group itself has to form a collective, rational set of judgments on those questions. How should it go about dealing with this task? We argue that the question raised is subject to a difficulty that has recently been noticed in discussion of the doctrinal paradox in jurisprudence. And we show that there is a general impossibility theorem that that (...)
    Download  
     
    Export citation  
     
    Bookmark   237 citations  
  47. Reconciling Rigor and Intuition.Silvia De Toffoli - 2020 - Erkenntnis 86 (6):1783-1802.
    Criteria of acceptability for mathematical proofs are field-dependent. In topology, though not in most other domains, it is sometimes acceptable to appeal to visual intuition to support inferential steps. In previous work :829–842, 2014; Lolli, Panza, Venturi From logic to practice, Springer, Berlin, 2015; Larvor Mathematical cultures, Springer, Berlin, 2016) my co-author and I aimed at spelling out how topological proofs work on their own terms, without appealing to formal proofs which might be associated with them. In this article, (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  48. Some Thoughts on the JK-Rule1.Martin Smith - 2012 - Noûs 46 (4):791-802.
    In ‘The normative role of knowledge’ (2012), Declan Smithies defends a ‘JK-rule’ for belief: One has justification to believe that P iff one has justification to believe that one is in a position to know that P. Similar claims have been defended by others (Huemer, 2007, Reynolds, forthcoming). In this paper, I shall argue that the JK-rule is false. The standard and familiar way of arguing against putative rules for belief or assertion is, of course, to describe putative counterexamples. My (...)
    Download  
     
    Export citation  
     
    Bookmark   14 citations  
  49. Verified completeness in Henkin-style for intuitionistic propositional logic.Huayu Guo, Dongheng Chen & Bruno Bentzen - 2023 - In Bruno Bentzen, Beishui Liao, Davide Liga, Reka Markovich, Bin Wei, Minghui Xiong & Tianwen Xu (eds.), Logics for AI and Law: Joint Proceedings of the Third International Workshop on Logics for New-Generation Artificial Intelligence and the International Workshop on Logic, AI and Law, September 8-9 and 11-12, 2023, Hangzhou. College Publications. pp. 36-48.
    This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional (...)
    Download  
     
    Export citation  
     
    Bookmark  
  50. Big-Oh Notations, Elections, and Hyperreal Numbers: A Socratic Dialogue.Samuel Alexander & Bryan Dawson - 2023 - Proceedings of the ACMS 23.
    We provide an intuitive motivation for the hyperreal numbers via electoral axioms. We do so in the form of a Socratic dialogue, in which Protagoras suggests replacing big-oh complexity classes by real numbers, and Socrates asks some troubling questions about what would happen if one tried to do that. The dialogue is followed by an appendix containing additional commentary and a more formal proof.
    Download  
     
    Export citation  
     
    Bookmark  
1 — 50 / 998