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…
>Failure to be completely expressive about a paradigm is not itself a paradigm. Its just faulty reasoning.
I am being as expressive as my expressivity allows!
for x in all-entities-in-universe: SOMETIMES(x = x)
Here is an example in Python:
class A: pass
class B:
def __eq__(self, other): return False
a = A()
b = B()
assert (a = a)
assert not (b = b)
Would you be willing to lead by example and be completely expressive about the paradigm in which fault() is a meaningful function?
Don't moralise about my reasoning, when you are done implementing fault() we can pass my function as an input to yours. That will settle the matter without ceremony.
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.)
Technically no because there is only one instance of Peter Parker or Spider-man that have the same physical boundaries at their time of existence.
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...
>If you can't substitute Peter Parker for Spider-Man, then they are by definition not equal... This is too reductionist. Can you substitute Peter Parker(before the lab accident) for Spider-Man ?
Nope, and that's why many logical systems are talking about what is at a given time and fail in practice. There are logical systems that take time into account to solve those issues (look at something called referent tracking).
>If you can't substitute Peter Parker for Spider-Man, then they are by definition not equal... This is too reductionist. Can you substitute Peter Parker(before the lab accident) for Spider-Man ?
Nope, and that's why many logical systems are talking about what is at a given time and fail in practice. There are logical systems that take time into account to solve those issues (look at something called referent tracking).
I am aware ;) The question was calculated.
It's obvious that you can't substitute Peter Parker (before the accident) for Spider-man.
The Mathematical idea of equality-as-substitution ignores time. Which is why I called it "reductionist"
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
> Instead, coercions are used to emulate some of the advantages of subtyping. Maybe I missed it in the article, but what does subtyping give you that coercions don't?
Economy of thought.
In my opinion, subtyping declares a "is" relationship, and coercions declare a "can be viewed as" relationship. You would want both in Practal. Subtyping is more tricky than coercions in the sense that if done wrongly, it can introduce inconsistencies, while coercions cannot (they just may fail to be unique).
For example, ℕ should be a subtype of ℝ. Because a natural number IS a real number. Let's say you have the theorem `∀ x : ℝ. P x` for some predicate `P`. With subtyping, also the theorem `P n` holds for any `n : ℕ`. With coercions, only the theorem `P (c n)` holds, where `c : ℕ → ℝ` is the coercion. Now you have an additional constant `c` in your theorem. It makes things more complicated than they have to be. Sure, some pretty printing and nifty automation can help you a lot here, but why would you want to deal with that added coercion tax in the first place for cases where you don't have to?
Nope, and that's why many logical systems are talking about what is at a given time and fail in practice. There are logical systems that take time into account to solve those issues (look at something called referent tracking).
I am aware ;) The question was calculated. It's obvious that you can't substitute Peter Parker (before the accident) for Spider-man. The Mathematical idea of equality-as-substitution ignores time. Which is why I called it "reductionist" https://en.wikipedia.org/wiki/Becoming_(philosophy)
Mathematics have other ways to talk about equivalence than just equality that allow to handle such cases though.
I am aware ;) The question was calculated. It's obvious that you can't substitute Peter Parker (before the accident) for Spider-man. The Mathematical idea of equality-as-substitution ignores time. Which is why I called it "reductionist" https://en.wikipedia.org/wiki/Becoming_(philosophy)
Mathematics have other ways to talk about equivalence than just equality that allow to handle such cases though.
Yeah, but there's an epistemic/cultural issue at play. There's an entire thread below where Mathematicians are aggressively objecting to me demonstrating some of those alternative notions to the point of calling the realizations of my designs "wrong" even though the reification is equivalent to the design.
But in the extreme case you can also construct universes which only speak of inequalities (total order) as a rejection of the identity axiom.
In that universe Peter Parker and Spider Man are different entities, and so what you can and can't say about them is entirely down to judgment.
The most important question is WHY do you want to say anything about anything and who do you want to say it to?
It's difficult to encode any information in language without knowing who is going to be decoding it.
> Instead, coercions are used to emulate some of the advantages of subtyping. Maybe I missed it in the article, but what does subtyping give you that coercions don't?
While I'm not sure it's impossible (though if it's possible I doubt it would be pretty or non-fragile), I've at least never seen anybody emulate generic intersection/union types using coercions. Dependent intersections like in Cedille are definitely impossible.
…and yes I think that challenging one’s suppositions ought to be the first task of any aspiring philosopher. Isn’t that the whole idea?
Having read a few philosophers, I don't really see any fundamental difference between Feser's approach and those of other philosophers. All philosophers have their positions and try to construct arguments to support those constructions. Feser's positions are traditional Roman Catholic positions, but your average atheist philosopher (such as Graham Oppy or J. L. Mackie) is doing the same basic thing. I feel like your…
Good point: perhaps I have an unrealistic, dumb, ill-educated or otherwise malformed ideal/view that philosophers should somehow be constantly challenging their own ideas, using their writing/discourse as an instrument to help them reach better conclusions through statement/contradiction (something like constructing an academic essay using thesis/antithesis/synthesis I guess?) and disputing them internally… Actually, as you suggest, the ‘correct’ approach to philosophy, or at least the only realistically possible approach, is to repeatedly state prior beliefs in the most persuasive way possible and then presumably to defend your a priori views from any challenges by others - only ‘testing’ those ideas in reaction by engaging in external debate rather than an internal one… I wonder though, doesn’t the outcome/process of that debate have to register internally somehow, for one side at least, for it to have any point? …for an evolution of the thinkers involved’s ideas to take place, is it not necessary for one/both sides in a debate to have at least a somewhat open mind, even as they strongly debate their particular ‘side’? …to allow one side to change its mind when the arguments put forward by the opposition are significantly strong - otherwise the debate would inevitably become stale, never-changing and circular? If one side is fixed in its beliefs, why would the other side bother debating them at all? If they were interested in adopting those ideas they should merely ‘receive’ them, rather than engage in an inevitably fruitless debate? I suppose if you have an unshakable belief that there exists an eternal and ever-present truth that you are inalterably sure of, and others who don’t agree with you are simply less enlightened, then you may feel that you should never have cause to change your mind - why should you, as you are already privy to the ultimate truth? Your task then, if you are communicative/evangelical/missionary in some way at least, is only to expound that truth to others? Your writing becomes a vehicle to promote your ‘truth’ - truth informed by mystically or intuitively received wisdom, never conjecture… Your debate/writing etc. is not a way to clarify your own ideas, but rather to show others the folly of contrary thoughts?
So is Thomism(/forms of Neo-Thomism) the be-all-and-end-all of philosophical enquiry then? If an argument is based on unexamined prior positions how can it be considered sound? (I suppose there is a problem of infinite regress here/some form of ‘Russell’s teapot’ or something! :) Thomas Aquinas was/is an extremely influential and interesting thinker (especially for his time!), but I find that sadly I don’t necessaril…
Why don't you stop soapboxing and address the comment you're replying to?
Ok - please forgive/correct/help me out here if I’ve got the sticky end of the stick, but both the premise and conclusion, very clumsily put, seem to me to be: ‘formal or classical systems of logic are more limited/not as rigorous/less useful/less challenging than some people believe them to be, especially when applied to
Aristotelean/Thomist philosophy/conceptions, because of their ‘merely’ relational syntax/nature and because they cannot adequately express/encapsulate concepts/‘things’ that the author holds to be true or self-evident features of his perceived reality/received wisdom/everyday utility/a priori metaphysics. The author concedes its usefulness in certain contexts: particularly when combined/in conjunction with his favoured philosophical ideas, or used in support of them, but that it does not present a challenge/undermine the author’s ideas/beliefs in ways that presumably some prior/present critics might suggest.’