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

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.

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

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.

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.

Isn't this the problem with cynical criticism in general? It's an intellectual dead end, by definition.

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.

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

I don't know, because you didn't engage with the content of the article at all. You merely casted nasty aspersions on its author.

> I am not attacking the guy personally

Yes, you are.

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.

So not only do you throw around unsubstantiated aspersions, but you are also dishonest.

> the author has started from his prior positions and then constructed an argument that reinforces them

There are two ways to interpret this:

1. You're accusing the author of making an argument that is circular. If so, describe the argument, including its premises and conclusion, and specify which premise is the conclusion.

2. You're merely attacking the author for arguing their position. Hardly objectionable and also a red herring, since the soundness of an argument is independent of the author's "prior positions".

Furthermore, I see nothing controversial about the statement you quoted. It is indisputably true, and would be true for any other author.

> I think that sometimes being overly opinionated and incapable of changing your mind is potentially harmful to others, yes… Is it not potentially dangerous to advocate for various political realities based solely on unexamined/individual opinion-based constructs?

How can I disagree with this? Yes there is hazard in advocating for anything. Moreover, there is hazard in doing anything. But I see what you're getting at. There is some line we draw in our own minds between philosophy, that is the pursuit of truth, and political - the realm of opinions.

Where is the line? Most would say that it is when the philosopher argues in good or bad faith. Thus, we are in the realm of the unknowable, the motivations of all around us. Also, not to comment on the notions of whether it's possible for an individual's to be "good" or "bad", but I don't want to digress.

To return, I think you're saying that making statements result in harm to individuals is bad. I agree, but this is a political question, not a philosophical one. Thus providing a philosophical justification or contradiction for your statement is moot.

As in literally asking the question: What is Philosophy about?

The only answer we can give is political.

I feel like your expectations for how philosophers ought to behave aren't based on any significant familiarity with the work of actual philosophers, just your suppositions about how philosophy ought to be done.

Philosophy is a conversation, and valid argumentation is that starting point of any treatise. The work of contending philosophers is to challenge one another, so there should be no hesitation in using less-than-certain (that is to say, all) presuppositions.

Moreover, Feser does comment on his presuppositions in this very article.

> I would qualify this by saying that metaphysics is prior to logic if “logic” is understood in sense (b) described above, though not if understood in sense (a). Naturally, we have to presuppose certain canons of reasoning when reasoning about anything, including metaphysics. But it doesn’t follow that we have to presuppose the codification enshrined in some particular formal system – such as, for example, modern propositional and predicate logic rather than traditional Aristotelian logic, or rather than some system that tries to capture the best of both worlds (such as that of Fred Sommers).

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

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.

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.

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

That is, these two things are different: EXISTS(X): BELIEVES(AUNT-MAY, FIGHTS-CRIME(X)) AND BELIEVES(AUNT-MAY, NAME-OF(X, "SPIDER-MAN")) and BELIEVES(AUNT-MAY, EXISTS(X): FIGHTS-CRIME(X) AND NAME-OF(X, "SPIDER-MAN")), and the second seems to me like a better translation of "Aunt May believes that Spider-Man fights crime", at least for some of the states of affairs you might summarize with that sentence.

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

For materialists, it is not difficult to see that the brain of Aunt May believing only "Spider-Man fights crime" would be in a different state than if she also believed "Peter Parker fights crime", as going from the former to the latter would require some physical change.

This is too reductionist.

Can you substitute Peter Parker(before the lab accident) for Spider-Man ?

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)

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

  A = Time.now
  A != Time.now
  A == A

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)

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

    now != now

    a := now(T0)
    a != a

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

So "now" is a trickery to hide the fact you're really saying "now(Ti)", for varying i.

I'm not tripping over syntax, but I think you are:

You think you're saying

    A != A

    A1 != A2

    now(t0) != now(t1)

And of course the second form is unsurprising.

All impure functions have an implicit dependency on (some subset of) the state of the universe when they execute; in mathematics and logic something with this kind of dependency is typically noted by parameterizing it by time when the actual precise nature of the dependency is outside of the scope of the immediate analysis (because a dependency on the state of the universe at the time of execution is equivalent to a dependency on the time of execution with a hidden function mapping time to state of the universe.)

That impure functions methods are in many programming languages syntactically not distinguished from pure ones does not change the logic here.

That Time.now(at time t0) is distinct from Time.now(at time t1) is... unsurprising, and not an example of A != A in logical terms.

Parameters ARE inputs. Results ARE outputs. Renaming them to something else is just obscuring the fact that you are still talking about a function with side-effects.

So using Python as my model of computation this is a pure function, but it does nothing:

   def f(): pass

   def g(): return True

   def h(x): pass

   def j(x): return x

   def k(): 2+2

You only want to talk about pure functions. I want to talk about ALL functions.

So lets define the function "pure" such that

  pure(f) -> True when f is a pure function
  pure(g) -> False when g is an impure function

https://en.wikipedia.org/wiki/Impredicativity

> "All impure functions have an implicit dependency on (some subset of) the state of the universe when they execute"

You wrote:

> "You only want to talk about pure functions. I want to talk about ALL functions."

Find the error.

   In [1]: class A:
   ...:     def __eq__(self, other):
   ...:         return False
   ...:
   In [2]: a = A()
   In [3]: assert a != a
   In [4]: assert a == a
   AssertionError

Will you now recognise my right to free speech and free thought, or must I fall in line?

Still waiting for you to implement equal() as a "pure" function.

We can discuss what you mean by "error" once we have a referent (that's not just in your head) to talk about.

Tell us more! I didn't believe in omniscience until now.

Time.now(t1) and Time.now(t2) is meaningless in this context because t1 and t2 are unbound variables. What are you passing to your function? Where is it coming from?

My function says you are overlooking something.

  [1] pry(main)> Time.now(t1)
  NameError: undefined local variable or method `t1' for main:Object from (pry):1:in `__pry__'
  [2] pry(main)> Time.now(1)
  ArgumentError: wrong number of arguments (given 1, expected 0) from (pry):2:in `now'

As for the rest: please provide the implementation of your Time.now function and I'll tell you its implicit parameters. If you're not talking about an actual function that can be run by a computer, then please tell me so and I'll drop it -- I'm not interested in hypothetical functions tautologically defined not to be equal to themselves.

You are missing the point about extensional and intensional properties of functions.

If you want to look "inside" my Time.now function then maybe you should also look "inside" your equality function and find its implicit parameters?

Here's some Python boiler plate - implement equality and make the assertions pass.

  def f():
    return 1

  def equal(x,y): 
    # Implement equality

  assert not equal(1,2)
  assert equal(1,1)
  assert equal(f, f)

As far as I can tell you are not talking about such a function either when you speak about equality, but I'll reserve judgment until you produce an implementation.

>I'm not interested in hypothetical functions tautologically defined not to be equal to themselves.

OK, but you are interested in hypothetical functions tautologically defined to be equal to themselves.

That's perfectly fine - we are interested in different tautologies.

You want to say equal(f,f) is true.

I want to say not equal(f,f) is true.

We want to say different things.

The expression A = A can be trivially re-written in another notation as equal(A,A). The reason you don't question the implementation of the equal() function is because it's declared as being true however it's implemented.

So, I declare f() != f() as being true. I also declare that f() takes no arguments. All I am doing is translating (transpiling?) English into Ruby.

"Now is not now" => "Time.now != Time.now"

Talking about function arguments is not even in point. What's the argument to now() in English?

Incorrectly.

> "Now is not now" => "Time.now != Time.now"

Sure, “Now (pointedly looks at watch) is not now (pointedly looks at watch)” is true, and the equivalent of the Ruby. Ruby expressions lack the implicit simultaneity that English sentences wthout some contextual signal of explicit time dependency have, and your mistranslation ignores this.

The English and Ruby terms map 1:1.

Now(Time.now) is not(!=) Now (Time.now)

Why do you call the correct "incorrect"?

Nowhere; that's the contextual signal that defeats the implicit simultaneity the English sentence would have without that body language.

The English sentence "Now is not Now" describes my thought process (1st person view), not my body language (3rd person view).

My thought process occurs over time. Exactly like the Ruby process.

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.

Telling me what I can and can't do is an imperative statement...

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 to represent the idea you intend to communicate.

  A != A 

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.

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

  x = “Time.now != Time.now”
  eval(x) == true

  f() != f()
  !( f() == f() )
  A != A
  Now is not now.

    f() != f()

Do note two things:

The notation f.call is the same as f(), i.e. function invocation. You're not comparing functions but invoking them and comparing their results.

I don't know the equivalent syntax in Ruby, but in other languages the following is always true:

    f == f

Note that the assertion "two things that are not the same might be different" is completely unsurprising. We're just letting syntax confuse us in this discussion.

   f == f

The evaluation strategy must come after we agree whether we're comparing values after invocation or definitions. If it's invocations, the evaluation strategy you pick can change the meaning of the program, so that we must discuss semantics.

In all of these cases,

    A == A

A straightforward way can be to simply compare the text of the functions, as written in your programming language of choice, in this case Ruby.

Just take the text of both functions, do a diff, and if it says they are the same, they are the same.

Another comparison could be more abstract, since we know there's more than one way to accomplish the same with a programming language: two functions are the same if, given the same input, they produce the same output. You can either prove this by extension, if the number of possible inputs is finite and small, or you can prove it logically. With some languages which enforce purity using types, you can even show two functions are the same just by looking at their signatures, no need to evaluate anything! (this is one advantage of some statically typed languages, by the way!)

> There are no implicit arguments to the function I have in mind. Passing an argument to the function I have in mind is an error.

Yes, there are implicit arguments. You don't see them because they are implicit! A function that returns the moment in time, "now", of course depends on an implicit argument: the current time! How else is it going to know the moment of "now", otherwise? Think about how such a function is implemented.

Indeed. I pointed this out and provided a link in my first post on this thread.

>You don't see them because they are implicit!

The fact that my function takes no arguments is implicit in the specification of my function. I know because I said the English sentence "The function that I have in mind takes no arguments".

You seem to be suggesting that I don't know what function I am thinking about but you do. This is a very peculiar hypothesis.

If you want to argue otherwise, you must provide this hypothetical implementation that complies with your specs. I'm telling you that your function effectively can't exist as you describe it. In order for your function to work it requires an implicit argument (the "world" if you want to be coarse, though in this case we know it's the time).

If you want to argue that

    magical function is not magical function

I don't know how to respond to this. Just observe the thing I am showing you. THAT is what I am talking about. It's right before your eyes - I took it from my head and made it real.

>If you want to argue that

I DON'T want to argue! All I am doing here is expressing myself - you are the one jumping down my throat.

This is me telling you that I am not interested in any social game of figuring out "who is right or who is wrong". If that's the game you are playing - I am happy to terminate the interaction.

What I mean by f() != f() in the abstract is precisely that Ruby program in the concrete. Nothing more - nothing less.

There is no room for "right" and "wrong" here. Those are moral judgments and I've committed no moral violation of any sort.

I don't need to know the implementation of the real function Time.now from Ruby because, without looking at its source code, I can tell you that it has implicit arguments.

How can I tell this? Because it's impossible for your Ruby program to tell the time without some kind of interaction with an external source (be it the computer clock, the internet or whatever); this source is your implicit parameter and it's why two invocations of your function don't return the same value. It is impossible for your function not to have this source of time, either implicitly or explicitly.

If you disagree, then please explain how your function tells time.

I don't need to know the implementation of the real function == from any programming language because, without looking at any source code I can tell you that it has implicit arguments: a tautology.

If you disagree, then please explain how equality functions.

Being a simple bear, so formal logic breaks my head, I agree.

Just a hunch:

These "impedance mismatches" are one root cause for our society's current epistemological crisis. Cases where we can't even agree to a shared base truth.

Further, "now is not now" is a bit like paradox, no? The ability to hold two contradictory thoughts in your head at the same time. A large fraction of people recoil from ambiguity. Also a source of endless strife.

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

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.

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.

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

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.

Your point that currently it is quite hard to do anything practical in all of the interactive theorem provers is very true, though.

[1]: https://link.springer.com/chapter/10.1007/11814771_27

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.

Maybe I missed it in the article, but what does subtyping give you that coercions don't?

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?

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.

Then it descends further into an unnecessarily jargon that can only be described as a debate about the sex of angels.

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.

> "Concerning the debate between eternalism and presentism, a typical physicist would say: 'who cares?'"

This is a great illustration that physics doesn’t care one way or another, or more properly, from the point of view of physics the question is meaningless.

Claiming that somehow physics has a biased view in a question it refuses to address altogether is weird.

For example: https://www.jstor.org/stable/1968621 And: https://en.wikipedia.org/wiki/The_Logic_of_Modern_Physics

But given that the first is from 1936 and the second from 1927, maybe that's out of fashion.

Some physicists are interested in quantum logic – that is very much a minority taste within the physics community though. Like interpretations of quantum physics in general, it straddles the boundary between physics and philosophy. (But unlike some more purely philosophical interpretations, it does have some mathematical meat to it.)

https://en.wikipedia.org/wiki/Quantum_logic

https://plato.stanford.edu/entries/qt-quantlog/

https://iep.utm.edu/qu-logic/

Don't some hypotheses in cosmology effectively presume eternalism? For example, the Hartle-Hawking state aka "no boundary proposal"?

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.