Any science of logic?

[wtf]

But HOTT, just like any branch of math, is a symbolic system. It says nothing about the universe.

This is where you are wrong.

Any system for which we have a state-space model is an example of Mathematics saying something about the universe. It predicts how the system is going to behave.

I'll let you join the dots between state-space and finite state machine.

The moment you mention "time" in a Mathematical model it becomes physics. And computer science.

We'll have to agree to disagree about that. Here's my argument.

Consider Euclidean geometry. For two thousand years everyone believed it described the universe.

In the 1840's Riemann and others showed how to make perfect mathematical sense of non-Euclidean geometry. Then in 1915 Einstein published his theory of general relativity, showing that Riemann's math better modeled the world we live in. It was then understood that math did not tell us the truth about the world. The best a mathematical theory could be was consistent and interesting.

Now you say the world is a computer. I disagree but for purposes of this post I'll stipulate to your view. And yet there can be theories of math that disagree with that view. You can have classical set theory with its many noncomputable numbers and functions. You can say it doesn't model the world, and that's fine. But you can't banish it from existence. Set theory is interesting in its own right. Set theory is simply the study of mathematical structures that satisfy the axioms of set theory, just as group theory is the study of all the models of the axioms for groups. No connection with reality is implied or expected. If it's consistent (and we set theory we can't even be sure!) and interesting, it's good pure math. If the physicists find a use for it, it's good applied math. It need not be "true" in any meaningful sense.

People have understood this since 1840. That's really when mathematicians started paying attention to foundations in the first place, once Riemann showed that math doesn't tell you what's true.

So whether the universe is or isn't a computer is one thing. And HOTT is another. You can't possibly claim that any given mathematical theory is the absolute truth of the world. Math doesn't do that.

[wtf]

I explained it in the very next paragraph! I explained that the sentence was targeted at my interlocutor's understanding.

That's interesting. In other words you made an explicit claim whose truth value and/or coherence depend on the reader. That is, if your interlocutor is reading it, it means one thing or has one truth value. And if I'm reading it, it has another. How can any other reader know which class they're in and how to understand what you wrote?

I'll leave the rest of this post uncommented on. You seem wedded to your ideas and I didn't find much in this post to grab onto in terms of mutual reality.

It's certainly an extraordinary claim that any formal symbolic system exactly describes the world. Let alone a system (HOTT) that's been in existence for only a few years and is far from finished, and whose leading light recently passed away in his prime. If that's your belief, I won't try to talk you out of it. Carl Sagan said that extraordinary claims require extraordinary evidence. In my opinion you have not provided evidence for your claim beyond your own passionate belief.

Today's bonus question. Without looking it up, can you state the univalence axiom and say in your own words what it's intended to mean?

[wtf]

Dammit I keep hitting Quote when I mean Edit. Double post. It says I can't delete posts in this forum. The moving finger having writ and all that.

[Univalence]

Consider Euclidean geometry. For two thousand years everyone believed it described the universe.

(....)

So whether the universe is or isn't a computer is one thing. And HOTT is another. You can't possibly claim that any given mathematical theory is the absolute truth of the world. Math doesn't do that.

When did we get to "absolute truths"? I think I rejected that notion on a number of occasion. I explicitly mentioned that utility is more important than truth - a stance you don't hold even for Mathematics.

It's a model. All models are wrong. Some are useful. Even the Standard MODEL of Physics.

But I already pointed you to model-dependent realism
It claims reality should be interpreted based upon these models, and where several models overlap in describing a particular subject, multiple, equally valid, realities exist. It claims that it is meaningless to talk about the "true reality" of a model as we can never be absolutely certain of anything. The only meaningful thing is the usefulness of the model.

[Univalence]

That's interesting. In other words you made an explicit claim whose truth value and/or coherence depend on the reader.

Yes. I did. Feynman understood why that matters. You don't?

That is, if your interlocutor is reading it, it means one thing or has one truth value. And if I'm reading it, it has another.

Yes! Because that is how interpretation/communication works! You can only interpret my words in the context/frame of your own understanding.
But that fact aside, you actually asked me to!

I'm not reading all the back and forth so it would be better if you just engage with me separately without assuming I'm up on all the other posts.

It's certainly an extraordinary claim that any formal symbolic system exactly describes the world

Strawman. We were talking about functionally equivalent MODELS of the mind. Not DESCRIPTIONS of the mind.

If we were into descriptions I could stop at saying "The mind computes".

[Univalence]

Without looking it up, can you state the univalence axiom

What is this? A high-school exam?
The axiom is here: https://github.com/UniMath/UniMath/blob ... nceAxiom.v

It says what it says and it does what it does. If you want to understand it you need empiricism - run it on your own computer and study it.
Dive deeper into the implementation details.

DO some science.

and say in your own words what it's intended to mean?

In my own words it's just another axiom. An input to a Turing machine. And it means what it DOES. And it DOES what it says in the 300 lines of code above.

2. You are still looking at this from the Mathematical perspective.

computational trinitarianism

The central dogma of computational trinitarianism holds that Logic, Languages, and Categories are but three manifestations of one divine notion of computation. There is no preferred route to enlightenment: each aspect provides insights that comprise the experience of computation in our lives.

Computational trinitarianism entails that any concept arising in one aspect should have meaning from the perspective of the other two. If you arrive at an insight that has importance for logic, languages, and categories, then you may feel sure that you have elucidated an essential concept of computation–you have made an enduring scientific discovery.

There is even a Rosetta stone for you to map the jargon from one paradigm into the other.

But really. The answer you probably wanted to hear is probably something like this: It promises us that functionally equivalent mathematical objects can be trivially identified. It promises solving the Entscheidungsproblem up to an equivalence (except for Girard's paradox). It says this right here.

Code: Select all

Definition univalenceStatement := ∏ X Y:UU, isweq (@eqweqmap X Y).

It allows for trivially determining if any two (seemingly different) mathematical objects are "the same".

Or from a programmer's perspective. it allows for defining what "success" looks like (expected output) before writing the implementation.
Which is the same as saying as "start with the solution and work backwards" (but the notion of Equifinality went over your head last time).

Which is on-topic for this thread! Since we are talking about the functional equivalence between the human mind and any model of it we could ever conjure up.

Now if we could just agree on the (metaphorical) identity type then we would have defined what it means for a Mind to be "functionally equivalent" to a Model-Mind.
We would have ourselves a testable hypothesis.

[Univalence]

Consider Euclidean geometry. For two thousand years everyone believed it described the universe.

In the 1840's Riemann and others showed how to make perfect mathematical sense of non-Euclidean geometry. Then in 1915 Einstein published his theory of general relativity, showing that Riemann's math better modeled the world we live in.

Precisely. Thanks for making my argument for model-dependent realism.
Computer science is the science of model-construction. Lego for your mind.
The limits of computation are the limits of model-construction/model execution are the limits of human knowledge.

It was then understood that math did not tell us the truth about the world.

In so far as all truth is just a model, your claim is demonstrably wrong. This is the Standard Model of Physics. It sure looks like math.


But perhaps you are using models all wrong? They aren't tools for SAYING anything about the world.
Models are tools for UNDERSTANDING the world. They are (and will always be) as good as their ability to predict things.
If you want to tell stories - English works better.

The best a mathematical theory could be was consistent and interesting.

It doesn't even have to be consistent

[Univalence]

So here's an idea perhaps?

Godel told us that we can't prove the consistency of any particular system WITHIN the system itself.
But Univalence allows us to trivially detect inconsistencies. So instead of chasing our own tail, how about we use 'number of inconsistencies' as a metric for how badly a Mathematic sucks?

Univalence sucks 1 (Girard's paradox).
How much does ZFC suck?

[Speakpigeon]

Any inconsistency makes a system 100% illogical.
Aristotle's syllogistic is logical.
ZFC isn't logic at all. At best, it's a crude approximation.
So, your metrics could be understood as the distance from a given system to logic proper.
EB

[Univalence]

Any inconsistency makes a system 100% illogical.

No it doesn't. There are logics which can tolerate some inconsistencies.

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

Computer scientists understand the process as Exception handling.

[Speakpigeon]

Any inconsistency makes a system 100% illogical.

No it doesn't. There are logics which can tolerate some inconsistencies.

That's a re-definition of logic, hence, it's equivocation.
Here is Aristotle's definition of a syllogism and hence of logical validity and of deductive logic itself:

A syllogism is discourse in which, certain things being stated, something other than what is stated follows of necessity from their being so. I mean by the last phrase that they produce the consequence, and by this, that no further term is required from without in order to make the consequence necessary.
Prior Analytics, Book I, Translated by A. J. Jenkinson, published by eBooks@Adelaide, The University of Adelaide Library, University of Adelaide https://ebooks.adelaide.edu.au/a/aristo ... book1.html

That's the reference. We all understand this definition and we all reason on this basis when we think logically. Outside of that, it's no longer logic. Mathematics, yes, logic, no. Mathematical "logic" doesn't make human logic disappear. There's no point to this discussion since clearly we will be forever talking about different things. Me about human logic, you about mathematical logic, and I really don't care about mathematical logic since we don't even know what it is supposed to represent.
This thread is about human logic, though.
EB

[Univalence]

That's a re-definition of logic, hence, it's equivocation.

You can't re-define something you never defined to begin with.

Here is Aristotle's definition of a syllogism and hence of logical validity and of deductive logic itself

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

[Univalence]

Mathematical "logic" doesn't make human logic disappear.

When I reject the law of excluded middle and double-negation, and I replace identity with identity types. What's left no longer resembles Aristotelian logic.

From https://philpapers.org/archive/ALVLIM-3.pdf
A difference in metaphysics demands a difference in logic.
The intuitionists, constructivist mathematicians, where the first who understood that
rejection of realism entails rejection of classical logic.

Although 'rejection of realism' is a bit strong. I would happily describe myself as a model-dependent realist

Me about human logic, you about mathematical logic

That's a great way to dehumanize me.

I am human. I use logic. I chose a different logic to you.

Perhaps I use logic differently than you do?

I really don't care about mathematical logic since we don't even know what it is supposed to represent.

I know what it represents. The structure of my own mind. The structure I constructed.

It represents my map, not the territory. I know myself. I can't say the same about reality...

[wtf]

When did we get to "absolute truths"?

When you said the world is a computer. That's a metaphysical claim. A claim of absolute truth about the world. It's something that's unknown and possibly unknowable yet you insist on it.

You are the one claiming knowledge of an absolute truth.

I think I rejected that notion on a number of occasion. I explicitly mentioned that utility is more important than truth - a stance you don't hold even for Mathematics.

I could be misunderstanding you. Perhaps when you say the world is computer you DON'T mean to be making a claim that your statement is true about the world? Now you have me totally confused.

Yes you are correct that I regard interestingness and mathematical beauty as the only criteria for worthwhile math. And if the physicists and shopkeepers find math useful, so much the better. Hardy had that view, that the most beautiful math was by definition the most useless. His field was number theory, which was regarded as supremely useless. Then in our own times number theory has become the basis of public key cryptography, underlying all internet security and all cryptocurrencies. What would Hardy think to come back and find that his belovedly useless number theory has been sullied by application!

It's a model. All models are wrong. Some are useful. Even the Standard MODEL of Physics.

So are you now admitting that your idea that the world is a computer is only a model and not metaphysical truth? Perhaps I've been misunderstanding you. Can you please clarify this point once and for all?

But I already pointed you to model-dependent realism
It claims reality should be interpreted based upon these models, and where several models overlap in describing a particular subject, multiple, equally valid, realities exist. It claims that it is meaningless to talk about the "true reality" of a model as we can never be absolutely certain of anything. The only meaningful thing is the usefulness of the model.

So you don't claim the world is a computer? Please advise.

[wtf]

What is this? A high-school exam?
The axiom is here: https://github.com/UniMath/UniMath/blob ... nceAxiom.v

It says what it says and it does what it does.

Here's the problem.

Earlier you claimed to be studying Homotopy Type Theory, or HOTT. I found that interesting since I'm studying a related discipline, category theory. I asked you if you knew about category theory and you claimed you did. I probed that by asking you what a universal property was. Your completely off-topic response convinced me that not only don't you know any category theory, but you are someone who claims to understand things rather than simply admit they don't.

And now I ask you what's a homotopy, and you have no idea. So you're not actually studying HOTT. And YOU are the one who chose Univalence as your handle, and you don't even know what the word means or what is its significance in modern alternative approaches to math foundations.

I'm perfectly justified in calling you out on your bluster. If you clearly don't know what you're talking about regarding subjects I'm familiar with, then that causes me to doubt that you know what you're talking about on subjects I don't know anything about but that you claim to.

Yes I do see you managed to regurgitate some stuff you just hurriedly looked up. You simply have not convinced me.

As an example, when I pointed out that I learned that the lambda calculus is an example of a Cartesian closed category, I expected that you might say something like, "Cool, can you tell me more about what that means?" Or, "Thanks but I'm not interested in that." What I did NOT expect was for you to pretend to understand the remark when it's so painfully obvious that you don't. That's where I'm losing my enthusiasm for this conversation.


I'll leave your other two posts to me unanswered. I just don't get where you're coming from. First you claim the world is a computer and then you say that you are NOT claiming any absolute truths. I can not make sense of the conjunction of those two statements.