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

21–30 of 114 posts

Re: The metaphysical presuppositions of formal logic

#21

Post by cjfd »

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

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

Re: The metaphysical presuppositions of formal logic

#22

Post by practal »

cjfd wrote: post #21
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

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

I 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

Re: The metaphysical presuppositions of formal logic

#23

Post by gjm11 »

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

Peter Parker = Spider-Man, but "Peter Parker" != "Spider-Man".

It may or may not be true that 12345x54321 = 670592745. (I either put in the correct number there, or changed one digit in the middle at random.)

Let's suppose I didn't change it, and that you haven't yet checked. Then those two things are, really truly, equal -- they are two names for the exact same number -- but you don't know that they are equal. So the _meanings_ of "12345x54321" and "670592745" are not exactly the same, even though if "=" belongs anywhere it belongs between those things.

Philosophers call the thing that's the same the "extension" and the thing that's different the "intension" (not to be confused with "intention" which is an ordinary non-technical word). Sometimes you can safely substitute one thing for another whenever the extensions match -- e.g., when doing algebra. Sometimes you can't -- e.g., when talking about someone's beliefs.

I am not a fan of Edward Feser and I think this article is pretty wrongheaded, but there isn't anything specifically wrong with what he says about Peter Parker and Spider-Man.

Re: The metaphysical presuppositions of formal logic

#24

Post by logical_proof »

ukj wrote: post #9
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...

There are different kinds of "equality", beyond the one you are invoking: 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

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.

Re: The metaphysical presuppositions of formal logic

#25

Post by tgflynn »

gjm11 wrote: post #23
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...

Peter Parker = Spider-Man, but "Peter Parker" != "Spider-Man". It may or may not be true that 12345x54321 = 670592745. (I either put in the correct number there, or changed one digit in the middle at random.) Let's suppose I didn't change it, and that you haven't yet checked. Then those two things are, really truly, equal -- they are two names for the exact same number -- but you don't know that they are equal. So th…

My impression of this as a programmer is that if one is modelling a system in which different people may have different beliefs then one must design the model accordingly, otherwise there will be bugs.

But that doesn't mean there's anything wrong with logic itself. Whatever model you come up with is still going to be based on classical logic so at some point you still need to assume that that remains valid in order to do anything at all. And I've never heard of a case where this could fail, at least not within the finite worlds one can in practice model.

Re: The metaphysical presuppositions of formal logic

#26

Post by ukj »

logical_proof wrote: post #24
ukj wrote: post #9

Earlier quoted context omitted.

There are different kinds of "equality", beyond the one you are invoking: 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

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 English. Now is not now. It is trivially true.

When I use a word, Humpty Dumpty said in rather a scornful tone, it means just what I choose it to mean — neither more nor less

Re: The metaphysical presuppositions of formal logic

#27

Post by ukj »

joshuak wrote: post #20
ukj wrote: post #19

Earlier quoted context omitted.

So you are telling me that I can't choose to declare that A = A is false? Telling me what I can and can't do is an imperative statement...

You certainly may define your own symbology. But if you want to communicate with others you’ll need to agree on your symbology. In the common mathematical understanding A != A is defined as a false statement. In any example that one can contemplate it would become a true statement then you are replacing one of the ‘A’ symbols with something that is not ‘A’ in your mind. Which is to say you are using the wrong symbols…

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 false then they can exclude themselves from any formal or informal conversation about time on the basis of incomensurability of our paradigms

Re: The metaphysical presuppositions of formal logic

#28

Post by TheOtherHobbes »

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

Spider-Man is a subclass of Peter Parker with a different API and an added "fights_crime" method.

Aunt May has not been given the documentation that explains this, which is probably an intern's fault.

Metaphysically Peter Parker, Spider-Man, Aunt May, and the intern are all mocks anyway. So you can't use them for anything real.

(Except maybe entertainment, distraction, and metacognition.)

Re: The metaphysical presuppositions of formal logic

#29

Post by momentoftop »

cjfd wrote: post #21
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

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

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

Re: The metaphysical presuppositions of formal logic

#30

Post by joshuak »

ukj wrote: post #27
joshuak wrote: post #20

Earlier quoted context omitted.

You certainly may define your own symbology. But if you want to communicate with others you’ll need to agree on your symbology. In the common mathematical understanding A != A is defined as a false statement. In any example that one can contemplate it would become a true statement then you are replacing one of the ‘A’ symbols with something that is not ‘A’ in your mind. Which is to say you are using the wrong symbols…

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' to mean things not exclusively 'A' is unnecessarily ambiguous. This makes it not only useless for communication between people but also makes it useless for forming any meaningful conclusions.

Failure to be completely expressive about a paradigm is not itself a paradigm. Its just faulty reasoning.

Post reply on HN