Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The metaphysical presuppositions of formal logic

edwardfeser.blogspot.com

Post reply on HN
Print view View original

31–40 of 114 posts

Re: The metaphysical presuppositions of formal logic

#31

Post by myWindoonn »

Category 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.

Re: The metaphysical presuppositions of formal logic

#32

Post by User23 »

ukj wrote: post #4
drewcoo wrote: post #3

Earlier quoted context omitted.

Which 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.

The 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: Philosoph…

Does 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.

Re: The metaphysical presuppositions of formal logic

#33

Post by AnimalMuppet »

ukj wrote: post #8
xondono wrote: post #7

IMO 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 h…

But will a Physicist ever tell you whether time is continuous or discrete?

Once 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..."

Re: The metaphysical presuppositions of formal logic

#34

Post by AnimalMuppet »

myWindoonn wrote: post #31

Category 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…

Isn'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.

Re: The metaphysical presuppositions of formal logic

#35

Post by ImprobableTruth »

practal wrote: post #5

It'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

I'm not convinced that it's feasible to design a language that way because features and the underlying system generally seem to influence each other so much, so that I'd suspect starting with 'what you want' has a good chance of making the system unworkable due to breaking something like computationality or making classical logic unsound while making it very hard to notice (if it's not a theoretical property, then something more practical could also be problematic. Something like automation isn't a panacea either because a system needs to be amenable to it). Extending existing systems with something like intersection types seems already hard enough.

As an example, it's very hard for me to judge what it means for equality to not have a type without an underlying system to go along with it. Since it's still featured as part of types (such as your dom f = A ∧ cod f = B example), you still need a typing rule, but what would that look like? It's at the very least non-obvious to me that this doesn't potentially have some issues.

Or, what does extensionality for types cover that isn't done by subtypes? And should this just be a metatheoretic property, or also something that can be stated inside the system?

Besides that, the current items on the list are of course reasonable enough (though nil strikes me as a regression from option types and paraconsistent logic strikes me as totally unusable in the general case as you'd lose A \/ B, ~A |- B, which is absolutely essential.)

Re: The metaphysical presuppositions of formal logic

#36

Post by ukj »

joshuak wrote: post #30
ukj wrote: post #27

Earlier quoted context omitted.

Indeed I want to communicate with others, but I do not insist on communicating with Mathematicians in particular. I want to communicate with anybody who wants to talk to me about the nature of time. And when we converse about time I want to be able to say the obvious: now is not now. If we get more serious about this time business we might even want to formally express that: A != A If anybody insist that the above is…

The above is a false statement because if we say A is "true" then the statement becomes "true != true" which is obviously a false statement. In fact if we put anything in the place of A the results are the same. If, however, you wish to communicate the evaluation of a function such as "now()", then you would express that as two invocations of that function now() != now() or t != t' or simply A != B So simply using 'A…

I am not looking for an a debate; or to be “set straight”.

I am telling you that in my model what I am saying is true . Yes I am talking about function invocation. In Ruby:

  a = lambda { Time.now }
  a.call != a.call
Or…

  x = “Time.now != Time.now”
  eval(x) == true
Not to get bogged down in any particular notation/syntax… I am expressing the same thing in different ways.

  f() != f()
  !( f() == f() )
  A != A
  Now is not now.
If you disagree with this - you are welcome to disengage me.

Re: The metaphysical presuppositions of formal logic

#37

Post by practal »

ImprobableTruth wrote: post #35
practal wrote: post #5

It'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

I'm not convinced that it's feasible to design a language that way because features and the underlying system generally seem to influence each other so much, so that I'd suspect starting with 'what you want' has a good chance of making the system unworkable due to breaking something like computationality or making classical logic unsound while making it very hard to notice (if it's not a theoretical property, then so…

You don't need a rule system to understand what equality is.

Yes, it is not computational for sure. It's a logic, not a programming language.

Nil is the way undefinedness is handled in Practal. It is the most elegant way I can think of. You can still have your option type, just as you can have Kleene logic operators, but these are more suitable for doing program verification work in Practal, not so much for doing general mathematics in Practal. You really want (T ∪ Nil) ∪ Nil = T ∪ Nil here, while in programming you usually don't want Option[Option[T]] to be the same as Option[T].

I am not saying it is easy to make all of this work, and to make it work soundly. But less just doesn't cut it.

With a kernel-based approach, you have a chance to get it right. If you find an inconsistency, fix the kernel, and move on. Automation works just on top of it, and doesn't affect soundness. This is the great thing about automation in kernel-based ITP: If it finds some solution or counter-example, great. Otherwise, no harm done.

Re: The metaphysical presuppositions of formal logic

#38

Post by techbrobane »

User23 wrote: post #32
ukj wrote: post #4

Earlier quoted context omitted.

The 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: Philosoph…

Does 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 monothe…

> 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.

Re: The metaphysical presuppositions of formal logic

#39

Post by lisper »

continuational wrote: post #6

This 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...

I wrote my master's thesis on this exact topic back in 1989. The answer IMHO (which is due to Bertrand Russel [1]) is that the correct rendering of "Aunt May believes that spider man fights crime" is not BELIEVES(AUNT-MAY, FIGHTS-CRIME(SPIDER-MAN)), it is EXISTS(X): BELIEVES(AUNT-MAY, FIGHTS-CRIME(X)) AND BELIEVES(AUNT-MAY, NAME-OF(X, "SPIDER-MAN"))

and then you can also throw in BELIEVES(AUNT-MAY, NOT(NAME-OF(X, "PETER-PARKER"))) if you like.

[1] https://en.wikipedia.org/wiki/Theory_of_descriptions

Re: The metaphysical presuppositions of formal logic

#40

Post by the_af »

ukj wrote: post #26
logical_proof wrote: post #24

Earlier quoted context omitted.

I think you just made an equivocation as those Time.now’s are not the same A = Time.now A != Time.now A == A Just because Time.now looks like the same symbol it is not as it is an impure function that never returns the same result.

We are not talking about the same computation. What you think I mean is [1]. What I actually mean is [2]. [1] pry(main)> eval("a != a") NameError: undefined local variable or method `a' for main:Object from (pry):1:in `eval' [2] pry(main)> eval("Time.now != Time.now") => true I am not assigning the function to a variable - I am lazy-evaluating it. It's not equivocation because [2] is expressed exactly the same way in…

I disagree, because in both programming languages and in natural language, "now" is not a constant: it's a function that returns a different value depending on when it's called.

While the syntax is "now", what you're really saying is now(Ti) for some i.

So the sentence, in both natural language and most programming languages becomes:

    now(T0) != now(T1)
Which is easier to understand, with all arguments made explicit.

Now, some "clever" programming language might automatically translate this from

    now != now
To

    a := now(T0)
    a != a
Which will be surprising to the programmer in most cases (but might be what's desired in others).

The important thing is that "now" is not a comstant, but a function.

Post reply on HN