15 ms·
The metaphysical presuppositions of formal logic
- ukj 5y agoThis article does a great deal to point out the problem, but then just kicks the can down the road. Yes, metaphysics comes before Logic but metametaphysics comes before metaphysics. Ad infinitum. All this does is shift the discussion from the laws of logic to the laws of metaphysics - it is turtles all the way down. There is no way to get off this hamster wheel without a shift of perspective, but computer scientists should feel right at home anywhere recursion arises. Focus on the laws and the lawmaker. What are laws? Why do we create laws? What do we use laws for? How effective are we at encoding these laws in language? When we think of laws as designed rather than discovered we become more conscientious in our own inventions.
- drewcoo 5y agoWhich assumes a designer, so now we've compounded the presuppostions. And I don't see how more presuppositions means were more conscientious of them. Or conscious of them, if that was your meaning.
- ukj 5y agoThe designer is not assumed. I am it. I design formal systems. Formal systems are human inventions. Any expression or description of the “laws of thought” are subject to the limits of self-expression and the expressive power of your formal language. The “laws of thought” are rules of thumb. Useful Heuristics - not universal authorities. I recommend Luciano Floridi’s recent work in “The Logic of information: Philosophy as conceptual design.” https://ndpr.nd.edu/reviews/the-logic-of-information-a-theory-of-philosophy-as-conceptual-design/ https://ndpr.nd.edu/reviews/the-logic-of-information-a-theor...
- User23 5y agoDoes the universe have a designer then? It’s a pretty bold metaphysical assumption that the universe is undesigned and purposeless, but it somehow gave rise to an environment where intelligent beings can design formal systems that accurately describe the design of a system with no designer. This is part of the appeal of the simulationist philosophy, it allows intelligent design, but without the assumptions of monotheism. Naturally like everything else in this space it in turn introduces new difficulties.
- techbrobane 5y ago> It’s a pretty bold metaphysical assumption that the universe is undesigned and purposeless Nah, IMO it's much more "bold" to assume that the universe is designed and has a purpose.
- ukj 5y agoNone of our formal systems “accurately describe the design”. They all have domains of applicability - operational parameters. The appeal of the simulation hypothesis is that IF our formalisms could actually explain all of reality THEN it follows by logical implication that reality can be simulated. This logical implication is true because formal languages are Turing-recognizable. You can “explain” a formalism to a computer. You can program the computer with the Theory of Everything therefore universe can be run on a computer. This is ALL in the abstract. Unfortunately humans have the propensity to commit the mind-projection fallacy.
- voxl 5y agoIts not turtles all the way down, because there is a preexisting substrate that allows the discussion to happen in the first place. It is not a presupposition, because to merely state the _possibility_ of it being a presupposition necessitates its existence. There has to be some kind of preexisting substrate that enables thought. A recursive function can't run without a machine to run it.
- ukj 5y agoYou mean like the entity which invents/designs/defines the concepts of "substrate", "possibility","necessity" and "existence" ? The entity which measures and then captures regularities in "the substrate" in the forms of Mathematical equations (formal languages) - that which we call "laws of physics"? Even though physicists haven't yet solved the measurement problem. The entity that is trying to understand what it is made of and how it works? The entity that is trying to define itself? The function is running, alright and it's trying to reverse-engineer its runtime. The question is whether the function is recursive. Most functions refer to themselves as "I".
- krona 5y agoThis article does a great deal to point out the problem, but then just kicks the can down the road Isn't this the problem with cynical criticism in general? It's an intellectual dead end, by definition.
- practal 5y agoIt's important to sometimes step back and think about whether what you are doing actually makes sense. There are some assumptions about how formal logic is done in ITP (interactive theorem proving) systems that should be challenged. Here is my opinion about that: https://doi.org/10.47757/practal.1 https://doi.org/10.47757/practal.1
- cjfd 5y agoWhat you state about subtypes is not really true. HOL Light has subtypes baked into the kernel of the system. See https://github.com/jrh13/hol-light/blob/master/fusion.ml https://github.com/jrh13/hol-light/blob/master/fusion.ml lines 600-637. Coq has sig in the standard library which is not quite it but becomes a lot closer when one assumes proof irrelevance. Also, a COC-based prover can easily be given subsets with a few easy axioms. Your point that currently it is quite hard to do anything practical in all of the interactive theorem provers is very true, though.
- practal 5y agoI know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot add subtypes to a COC prover easily. [1]: https://link.springer.com/chapter/10.1007/11814771_27 https://link.springer.com/chapter/10.1007/11814771_27
- momentoftop 5y agoHOL Light doesn't have subtyping. If the type system had subtyping, there would be terms that are assigned two different types, where one type is a subtype of the other. So, in a truly subtyped system, you would have it that 3 has both type N and type R, with N being a subtype of R. Instead, in HOL Light, there is a total function from N to R, and a partial function from R to N. HOL Light allows you to carve out new types of existing types using a predicate filter, and this is baked into the kernel in `fusion.ml`. But this doesn't introduce subtyping relations. Importantly, the kernel rule gives you abstraction and representation functions to move between elements of the new type and the original type, but, unlike in a subtyping system, the terms of the newly defined type are not simultaneously elements of the larger type.
- continuational 5y agoThis seems too vague to me, like a lot of philosophical posts out there. > For example, if it is true that Aunt May believes that Spider-Man fights crime, then even though Spider-Man = Peter Parker, it does not follow that Aunt May believes that Peter Parker fights crime. If you can't substitute Peter Parker for Spider-Man, then they are by definition not equal...
- ukj 5y agoThere are different kinds of "equality", beyond the one you are invoking: https://ncatlab.org/nlab/show/equality#DifferentKinds https://ncatlab.org/nlab/show/equality#DifferentKinds The most obvious example of A != A being true I can think of is the evaluation of this expression in any programming language: Time.now == Time.now
- practal 5y agoGood example why programming and logic are related, but not the same.
- ukj 5y agoYes well.. Any two objects are the same, except for their differences. Any two objects are different, except for their similarities. "Sameness" and "difference" are abstract assertions. So in saying that you are doing programming; or maybe I am doing fuzzy logic. From my perspective it seems like you are evaluating this expression: same?(Logic, Programming) -> False But a different Oracle machine might produce a different answer :)
- joshuak 5y agoThese are imperative commands to execute, as apposed to a declarative statement comparing a value to itself. You can’t switch between symbolic representations to use the meaning of one to make statements about the other because the meaning of the symbols also switch.
- 5y ago
- xondono 5y agoIMO This article is a mess. Starts with an interesting premise, the foundations of logic (or rather, what people are taught as the foundations of logic) introduces unspoken assumptions. Then it goes on to illustrate with the worst example I can think off. modern physics’ mathematical representations [...] tend to insinuate an eternalist rather than presentist conception of time. I don't know which modern physicists he talks about, but pretty much any physicist will tell you time has a starting point, and none will make any claims to the existence or non-existence of an ending point. If anything, the lesson from modern physics is to enjoy the (relatively) brief period of time our planet is hospitable to humans. Then it descends further into an unnecessarily jargon that can only be described as a debate about the sex of angels.
- ukj 5y agoBut will a Physicist ever tell you whether time is continuous or discrete?
- AnimalMuppet 5y agoOnce a physicist has experimental proof one way or the other, sure. Until then, they may say "I think..." or "I suspect...", but they won't say "It is..."
- momentoftop 5y ago"Eternalism" refers to the static "block universe" conception of spacetime, where all events exist simultaneously, past, present and future. "Presentists", by contrast, hold that the past no longer exists, the future does not yet exist and only the present moment exists. Neither are positions about whether there is/was a first moment of time. I just finished reading the physicist Sean Carroll's book "From Eternity to Here", which is mostly about the thermodynamic arrow of time and big bang cosmology. He briefly discusses presentism and eternalism, before writing: "Concerning the debate between eternalism and presentism, a typical physicist would say: 'who cares?'" To be fair to Feser, I don't think he's commenting on the attitudes of contemporary physicists, but on a particular presentation of physics and logic. I doubt any working physicist cares one jot about this presentation, or formal predicate logic in general. Philosophers may well care, and Feser might just be noticing that his colleagues take formal logic far more seriously than it deserves.
- myWindoonn 5y agoCategory theory would help them. Yoneda's lemma tells us that elements of collections are uniquely isomorphic to the transformations which create those elements. This explains the butterfly effect where seemingly-unrelated parts of logical statements are causally connected. This post would have had bite 70 years ago, before we had "formally formal" theories of categories which can subsume any possible set theory. But now the door is closed. Interestingly, the transformations seem to be more important than the elements; whether a logic is e.g. reversible is a property of transformations and not collections.
- AnimalMuppet 5y agoIsn't that a bit recursive? Don't you use formal logic in creating category theory? Then using category theory to create formal logic is circular.
- myWindoonn 5y agoSets are 0-categories, so this critique would also suggest that 0-category theories, set theories, are circular too. But we actually place formal logic before sets, and then use sets to reflectively study formal logic without infinite regress. This is a version of the general pattern that there are no informal justifications for formal reasoning. Once a person tastes formality, then they can judge for themselves whether to adopt it, but there's no self-sustaining proof statement.
- Cybotron5000 5y agoEdward Feser doesn’t seem to me to be genuinely interested in challenging his own presuppositions through metaphysics or philosophy, or in communicating the work of others to a wider audience. If the posts that appear on this site are anything to go by, he seems to specialize in a specious species of polemic and obfuscation designed solely to justify and promulgate his political and religious views. If it lends a sense of purpose to his life, makes him a living or gives him a feeling of self-importance/bolsters his worth among his peers, who am I to criticize? Perhaps it is actually a deep satire with some ulterior motive. As an agnostic, one can only hope that a capital punishment for more catholic thinkers is never re-introduced. https://en.m.wikipedia.org/wiki/Edward_Feser https://en.m.wikipedia.org/wiki/Edward_Feser
- pfortuny 5y agoSo you’ve just ad-hominemed him in a suspiciously suspect subscribed text. And by sheer coincidence, catholicism. Great.
- Cybotron5000 5y ago…catholic with a small ‘c’: https://www.thefreedictionary.com/catholic https://www.thefreedictionary.com/catholic (…sorry I couldn’t resist the pun…). Personally I think there have been many wondrous, uplifting and glorious achievements of the Catholic church/its followers …and, I’m sure you would agree, some not so much, as is the case with many human institutions… What is it I’m subscribed to? Edward Feser may be a wonderful fellow in person for all I know - I would like to think at least that he is a decent, upstanding, law-abiding, moral etc. citizen - he certainly comes across as erudite and indefatigable in his writing… I just get the feeling that the two blog posts I have read of his that have been posted on this site were both designed solely to reinforce his particular presuppositions? Perhaps I am judging him unfairly - would you recommend something else of his that I should read instead? As I say, if his philosophy/faith works for him, gives him meaning and hope and joy etc. and he genuinely believes in those ideas, I wish him all the best… I worry a little about (perhaps less enlightened) people wanting to apply those ideas to society at large though... You must surely also be aware of examples from history where things have not gone so well? (not least for Catholics at various points in time - incl. ancestors of my own). What do you think?
- tunesmith 5y agoIt's difficult to engage with the content of the article head-on because it's pretty dense with concepts, but it made me think of two points - First, when trying to put together a chain of truth-functional syllogisms, if-then logic doesn't really suit the requirements. For propagating boolean truth through the network, digital AND gates are a better fit. If two propositions are false, you really do want the conclusion to be false, not true. If one of the propositions are false, you want the conclusion to be false, regardless of whether the first or second propositions are false. Also, in this case, truth is more an intuitionist concept than a classical concept; where the truth value represents provability - false means "it is false that this conclusion is proven true", not "the semantic meaning of this conclusion is false". Second, I'm not too familiar with the differences of materialist logic, but it seems that the goal of trying to nail down the semantic meaning of every statement is a goal that will never be met. It seems a more tractable goal to have your machinery reflect the form-validity rather than the content-validity - fully judging the semantic content is something that ultimately is better judged by the people experiencing the content.
- benlivengood 5y agoEssentialists are map-makers eternally searching for a map that exactly matches the territory, and will forever be disappointed. Some of the metaphysical problems with logic that the article tries to approach do exist, but in my opinion they are the domain of decision theory, not philosophy.
- alentist 5y agoThat's incorrect. Essentialism is more like the claim that there is a territory in the first place.
- skissane 5y ago> This has some notoriously odd results (known as the “paradoxes of material implication”) > You’ll still get weird results (known as the “paradoxes of strict implication”) This is obviously building up to the concept of relevance logic (called "relevant logic" in the UK and Australia) – https://plato.stanford.edu/entries/logic-relevance/ https://plato.stanford.edu/entries/logic-relevance/ – and no doubt Feser knows about it, but isn't taking the reader there. It seems to me an odd omission. A lot of his argument is actually against classical logic, not formal logic. Many philosophers and logicians agree that classical formal logic is deeply flawed, and have proposed various non-classical formal logics in response (relevance logic, constructivist/intuitionistic logic, paraconsistent logic, among others). But in this blog post he doesn't interact with or mention any of that work. > To show that the eternalist conclusion really follows, and does not merely falsely appear to do so, would require independent metaphysical argumentation I've never understood how Feser manages to believe in both presentism and divine eternity. In my mind they are mutually exclusive propositions. Atheism and process theism / open theism both go well with presentism. But the eternal God of classical theism, who knows all of time as one single moment, seems to me to have an eternalist approach to time as an inevitable consequence.