Hacker News new | past | comments | ask | show | jobs | submit login
Logic is Metaphysics (2011) [pdf] (philpapers.org)
100 points by lainon 9 months ago | hide | past | web | favorite | 60 comments

>Does the number seven exist? Does the red color exist? What evidence do we have to answer these questions? What are the truth conditions for ∃x P(x) when P(x) stands for a number or a property? To respond to these questions is to set an ontology, and setting an ontology is to do metaphysics. This is exactly what Quine does when he states some reasons to include numbers and to exclude properties from the domain of our variables.

Good paper.

Seems like from that it's just framework construction. It may have the same internal structure as an ontology, but to say the statements have any external correspondence (to the metaphysical; I'm using 'external' loosely) would require an extra step.

I can set an ontology where `thingamajiggers` are the only entity (so I guess the only truth condition for '∃x P(x)' is that P(x) is a thingamajigger), and I guess if you want to you can say I'm doing metaphysics at that point, though it does seem a little pointless to do so.

>Does the number seven exist? Does the red color exist?

those ones seem to be easy. There is no number seven. I mean there seven trees, seven stones, yet there is no number seven. It is only our mental construct (note: the construct itself, ie. neuron circuits and firing sequences do exist. It is like a map of non-existent land - the map exists while the land doesn't). The same is red color. There are EM waves of different frequencies. Color is mental construct triggered by perception of EM frequencies in specific range. Slightly different for different people. Completely missing for cats if i remember correctly. Like the number seven which is probably missing for cats too, and is known to be missing by various indigenous tribes separated from our civilization - people in this tribes know seven arrows, seven boats, ... yet completely don't understand just seven.

> There is no number seven. I mean there seven trees, seven stones, yet there is no number seven.

There aren't trees or stones any more than there is the number seven: objects (other than elementary particles, maybe) are as much mental constructs as numbers.

Why stop at elementary particles? All objects are mental constructs of consistencies our brains detect in data that our senses pick up.

Humans have a great advantage in picking up on what I'd call meta-consistencies (which is basically what abstraction is) - creating a new mental construct by detecting consistencies not only in what the senses pick up, but detecting consistencies in those consistencies, or "thoughts about thoughts" if you will. This gives you numbers and other abstract concepts that enable far more powerful manipulation.

>those ones seem to be easy. There is no number seven.

That's a very definitive answer for a complex question. It is not immediately clear at all that there is no number 7.

There are a few accounts for how numbers could exist. Let's break down each account:

* formalism - Mathematics is a formalized activity undertaken by humans, but is ultimately a language game. This approach is problematic because no formal system is capable of enumerating all truths about Mathematics. Hence, Mathematics is not a formal activity undertaken by humans, because otherwise the methods of its formalism would allow us to enumerate each true statement.

* intuitionism - Mathematics is a psychological artifact of minds, but is not a "natural" phenomenon. This approach has problems because it fails to account for (1) the remarkable consistency and success of Mathematics, and (2) leads us to Godel's disjunction. Godel's disjunction states that either there is no algorithm capable of enumerating all true statements that a human mind enumerates, or there are some Mathematical truths that can not be decided. If there is no algorithm capable of enumerating all true statements that a mind enumerates, then the mind is not a computational system -- meaning it can not be reduced to a mathematical model of neurons communicating -- and so the meaning of a psychological artifact needs reappraised. Specifically, numbers being a psychological artifact does not imply that they do not exist naturally. However, if a human mind is a computational entity, then intutionism doesn't work for the same reasons why formalism doesn't work.

* Realism - Mathematical objects exist. Given the problems of formalism and intuitionism, this actually is among the most probable of hypotheses.

Many Mathematicians fall into the Realist category, and there are good reasons why.

> there is no number seven

There is cardinality. There is ordinality. The "number seven" is a label for specific points in the cardinality and ordinality spaces.

> Color is mental construct triggered by perception of EM frequencies in specific range

You're conflating stimulus and sensation here

> There is no number seven. I mean there seven trees, seven stones, yet there is no number seven. It is our mental construct.

Crows, horses, and dolphins all have well documented[1] abilities to count numbers therefore as inconvenient and suggestive as it may be, the "number seven" most definitely exists somewhere outside human mental constructs and likely originates inside the abstract fuzzy designs that produce elementary consciousness.

1 - https://www.scientificamerican.com/article/how-animals-have-...

>likely originates inside the abstract fuzzy designs that produce elementary consciousness.

that sounds pretty close to what i'm saying - similar brains (and i do think that many animals' brains are much closer to us than we casually think they are) given similar experience (seeing seven stones, seven birds) produce similar constructs (incl. an aggregation/averaging of some aspects of that experience). That doesn't necessarily mean though the real existence of that aggregation/averaging (ie. what we call "number seven"), only the neuron config/sequence what actually encodes it is real.

Whether or not you should say they exist depends on the particular meaning of the term "exist" you are using. And that in turn depends on what are your motives and purposes for asking the question.

Of course, if you are a Platonist then you will believe that there is a single, perfect meaning for the term that everyone should use.

Logic is metaphysics, only when one smuggles in one's intuitions as definitionally true; otherwise, it is not so: "If we look more closely how it comes about that these existential statements are logical truths in these logical systems we see that it is only so because, by definition, a model for (standard) first order logic has to have a non-empty domain. It is possible to allow for models with an empty domain as well (where nothing exists), but models with an empty domain are excluded, again, by definition from the (standard) semantics in first order logic. Thus (standard) first order logic is sometimes called the logic of first order models with a non-empty domain. If we allow an empty domain as well we will need different axioms or rules of inference to have a sound proof system, but this can be done." (From Hofweber, Thomas, "Logic and Ontology" https://plato.stanford.edu/archives/sum2018/entries/logic-on...)

I am not sure whether I really understand what the author argues for, probably because I read the paper in a rush. Does he argue that [the choice of] a logic is in some sense equivalent to [a choice of] what kind of entities exist?

If that is indeed the case, I would tend to disagree. While we often think of logic as a provider of undisputable truth, I am not sure that this is justified. There is more than one type of logic and they lead to different conclusions or contradict each other in the general case. Therefore it seems to me that the obvious thing to say is that logic is a human construct we use to reason about the world, it does not reflect universal truths but was invented and constructed in a way to be useful to deal with our world.

In consequence it is obviously very likely that logic and metaphysics are strongly correlated, but that would hardly be any deep insight but just a consequence of the way we constructed or choose the logic we use. If the logic I use to deal with the world makes a prediction about the world, for example the existence of a certain entity, then that entity might actually exist if may logic is a good match for the world, but I see no reason why the entity would have to exists, my logic could just be a bad choice.

What I took away:

If you want to say 'Santa Claus doesn't exist', you can't write a formula ~E x. x=Santa Claus. Because then you are conceding in your logic that some object Santa Claus exists.

So there is some connection between the structure of sentences we can construct in our logic and metaphysical claims. We should then try to understand differences in metaphysical claims by finding differences in logics.

The author then tries to show this for the metaphysical claim, 'Statements are true or false independent of whether they can be verified.' Instead of arguing about what is truth, what does it mean for a proposition to be verified. We can instead as about the differences in the logic. Because to even talk about truth and existence we need a logic first.

So don't think there is a claim that choice of logic forces claims about real world existence. I think is the more subtle connection, that choice of logic forces a choice about rules of inference.

Real world claims would need to be based on introducing propositions (which are independent of the logic?) and then using rules of inference (which are dependent on the logic).

So this is a bit of a tangent, but your Santa Claus example really clarified something I've been reading about recently. I'm reading Lloyd's "Foundations of Logic Programming", which essentially explains the fundamentals behind logic languages like Prolog. We write programs using uninterpreted functions[0] to represent our data, and define predicates to drive the program. The idea of using the Herbrand universe is that it gives a convenient universal starting point: if the program has a model in some universe, it will have a model in the Herbrand universe, and if the program does not have a model, it cannot have a model in the Herbrand universe.

Your Santa Claus example helped me understand why the Herbrand universe is only useful if you restrict yourself to clauses (disjunctions under universal quantification). The Herbrand universe consists of all objects one has named (and objects one can form with function symbols, but we have none of those here), so it must necessarily falsify "~E x. x = Santa Claus". It's easy to find a model where this statement is true (take the empty universe, or the universe which contains only the Tooth Fairy), but there is no model of this statement in the Herbrand universe.

[0] https://en.wikipedia.org/wiki/Uninterpreted_function

I guess I can't really edit this comment anymore, but it looks like I was wrong. That example is actually a perfectly valid clause, since it's equivalent to "forall x. ~(x = Santa Claus)". The only reason no model satisfies this clause is because we conventionally require equality to be reflexive, but for an arbitrary predicate the empty model would be a perfectly good model in the Herbrand universe.

I think we mostly understand the paper the same way. Still this seems utterly unremarkable to me, but maybe I am still just missing the important point. If you want to come up with a language to talk about the world, a logical system in this case, you make choices. You decide if you want to be first order or higher order, whether you want temporal facts, what you allow your variables to range over, which inference rules to use, and what predicates you allow. Or whatever else.

If you only want to talk about physical things, you may be able to get away with existential qualification. If you also want to deal with concepts like Santa Claus you probably have to be more sophisticated because now »exists« is an overloaded term in your domain and throwing the same existential qualifiers in front of everything won't yield results that can be meaningfully translated to statements about the world.

In the end you have the world, you have a model of the world in your logic, and you have some kind of mapping between the world and your model, most likely even on a meta level. Not only do objects in your logic have to be related to objects in the world, but the very structure of your logic, its inference rules, the allowed constructs, and so on, have to map to some of the structure of how the world works. So as I said, it should come at no surprise that differences in logic have to be equated with differences in the world you are modelling, but the real significance of that, if any, is still beyond me.

It seems to me that it’s possible to use logic while having no belief at all as to whether that logic has any connection to reality — it could simply be an exercise in symbol manipulation with no meaning at all, which is the formalist position.

A formalist would have no problem using a logical system that implies a particular belief about existence while not holding that belief at all.

Sure, but if you are only doing string manipulation with your logic, then you are doing mathematics and not philosophy. There is absolutely nothing wrong with that but it also says nothing about the relation between logic and metaphysics.

The platonic "Santa Claus" does exist, so it's completely valid. The statement "Santa Claus doesn't exist" is stating there is no judgement from experience which adheres to the concept of Santa Claus.

The platonic "Santa Claus" does exist, so it's completely valid.

Most if not all people would would certainly agree that the idea or concept of »Santa Claus« exists in some way. But when you qualify it with »Platonic« you are implying - intentionally or not - a quite specific view about the nature of abstract objects and that will decrease the number of people agreeing with this statement substantially.

Not really it's a common noun, which just means non-physical objects which exist in some way, even if Nominalist. You're confusing platonic with Platonic realism which are different things. But perhaps he should edit it to be more clear if the mistake is quite common, albeit perhaps meaning espoused by capitalization has been forgotten.

In German we do not have that distinction between the different capitalizations, at least not that I am aware of, and the usage of platonic is probably essentially limited to platonic love and relationships. Something learned about the subtleties of the English language.

We don't have that distinction in English, either. Words derived from names just tend to lose their capitalization over time and may gradually be diluted in meaning as people use them without understanding their origin.

Bold, passive, and mistaken accusation: https://en.wikipedia.org/wiki/Proper_noun

But I do see how it could be confused with platonic love, albeit I'm comfortable using it without clarification in the appropriate contexts. You're right, in German all nouns are capitalized.

A more appropriate Wikipedia article: https://en.wikipedia.org/wiki/Theory_of_forms

If you simply meant to say that the idea of Santa Claus obviously "exists" in some sense, thus it's valid to compare our experiences with that idea, then I agree with the comment saying a lot of people would agree with you, but "platonic" is ambiguous at best.

If you really did mean to imply that an ideal Santa Claus literally exists in a literal universe of perfect ideal forms, out of which everything in our universe emerges as an imperfect projection, then I agree with the other part of the comment saying you'll find much less agreement with that claim.

My comment was that the loss of capitalization and the loss of the word's original meaning are independent phenomena. I.e. the adjective "Platonic" is often being used in the diluted sense of "conceptual" or "mental image of", and that has nothing to do with capitalization.

>If you really did mean to imply that an ideal Santa Claus literally exists in a literal universe of perfect ideal forms

In philosophy, this is "Platonic Realism" quite different from "platonic", the lower case helps convey information. You make a mistake by assuming "platonic" explicitly conveys "Platonic Realism", given there are many "Platonic *" theories, such as "Platonic Idealism". Because of the ambiguity, as you correctly acknowledge, you are expected to understand it as the wikipedia article on "Platonic" suggests (as some sort of abstract object): https://en.wikipedia.org/wiki/Platonic

"Plato's influence on Western culture was so profound that several different concepts are linked by being called "Platonic" or Platonist, for accepting some assumptions of Platonism, but which do not imply acceptance of that philosophy as a whole."

I still tend to argue that the use of »platonic» or »Platonic« most of the time implies a relation to the philosophy of Plato, the usage with the generalized meaning of something along the line of »abstract« seems to be at least quite rare. The quote from Wikipedia also seems to support this.

And that is of course why I interpreted the combination of »platonic« and »Santa Claus« as hinting at Platonic Realism, because of the implied relation to the ideas of Plato and the example of »Santa Claus« as an abstract idea. Are there any other parts to his work were »Santa Claus« could be a relevant example but that is not related to his theory of ideal forms?

Also »Platonic Realism« and »Platonic Idealism« are, as far as I can tell, the same thing. »Platonic Realism« seems to be the common term, »Platonic Idealism« seems to be a less frequently used term with its origin in the fact that Plato called his abstract objects ideal forms.

"Plato's influence on Western culture was so profound that several different concepts are linked by being called "Platonic" or Platonist, for accepting some assumptions of Platonism, but which do not imply acceptance of that philosophy as a whole."

Does not support that the "Platonic" is Platonic Realism, which is what your chief claim is and what it would implicate if the term conveyed acceptance of the entire philosophy. It merely means the acceptance of an ontology of abstractions—which is implicit when there is discussion of it, otherwise how would it be discussed?

Even if you believe Platonic Idealism and Realism are the same (which is usually meant to designate the classification between 'soft' and 'hard' Platonism), there are even different Platonic periods.

Nonetheless, it's clear that I didn't communicate this well if I'm in this conversation. Which I don't think is irrational since my discussions are usually restricted to academic contexts where this usage is ostensibly vernacular.

I have been trying to articulate this important distinction to people. The notion that properties and conditions for existence need to be thoroughly defined and unified in order to discuss whether a meta has those properties.

A philosophical discussion of logic in this decade should at least be aware of the Curry-Howard isomorphism and Linear Logic. This paper makes a passing mention of this by treating the law of excluded middle. I would say that denying that law has led to the most fruitful developments of logic in the last century.

Philosophy without technical input is sophistry, technical developments without philosophy end up answering questions of no interest. Girard is an entertaining source of both philosophical and technical insight: On the meaning of logical rules I : syntax vs. semantics http://girard.perso.math.cnrs.fr/meaning1.pdf

Per-Martin Lof's ideas are also important: ON THE MEANINGS OF THE LOGICAL CONSTANTS AND THE JUSTIFICATIONS OF THE LOGICAL LAWS https://uberty.org/wp-content/uploads/2017/06/Martin-Lof83.p...

This only scratches the surface.

Wholly irrelevant, the paper is specifically concerned with recovering a dialectic between W. O. Quine and M. Dummett. Even if the question was the more general, "Is Logic Metaphysics?", knowledge of formal logics isn't even of concern. It's trivial that we can construct a plethora of axioms with their own definitions, the problem remains: to even adhere to those definitions one is exercising another intuitive logic—even in the case of computation which is an engineered construction to proxy this very intuition, otherwise we would have never been concerned with the linear properties necessary for computation to begin with.

"Intuitive" being another word for "subjective."

The experience of truth and logical consistency is entirely subjective. We can build networks of concepts that trigger the experience in ourselves and in others, but that doesn't make them objectively true - it makes them subjectively persistent and shared.

We acquired a cat recently, and it's interesting that her experience of basic spatial relationships is very different to ours.

She doesn't have the same experience of physics that we do. She sometimes gets confused by inside vs outside, and her experience of moving objects seems to be different to ours. She also gives the impression of experiencing hands and feet as disconnected objects, and not part of a gestalt "human".

We have no guarantees that from an alien point of view, our own experience of physics and of relationships doesn't have equivalent limitations. If the limitations exist, we're not aware of them. But to the extent that our cat's view of the world is probably recognisable by other cats, she's not aware of her limitations either.

It's more of a stretch, but not impossible, that our experience of logical abstraction and consistency may also have limitations. There may be non-human viewpoints where the basic subjective qualia of truth and consistency are more coherent, reliable, and inclusive than our own.

None of this can be proved, but it seems optimistic to me to believe that our version of logic is as good as logic can possibly be.

Yet we're able to discuss topics with each other, this is the basis of Poincare's Inter-subjective reality. There must be some commonalities of experience which allows us to map our whole experiences between each other. We are definitively limited to our experience, it is impossible to discuss or probe anything outside of it when the entire world and its phenomena is only dictated through experience to us.

Experience is a language which makes meaning from the not-experience.

As Bohr put it, "We're all suspended in language."

What I'm saying is that linear logic is exactly a technical exploration directly pertinent to the questions Quine and Dummett considered. And who cares if the paper is specifically about Quine and Dummett? What's the point of resuscitating such a dialogue without informing it of modern developments? To do so seems like frolicking in the graveyard. But much like philosophy of mathematics (with some exceptions like [0]), philosophy of logic to me at least seems like it prefers dusty bones to fresh developments (if 40 years is fresh...). At the very least, modern logic and its myriad connections to other fields could shed light on whether it's even worth bothering to adjudicate the interplay of Quine and Dummet's metaphysical arguments. They might be completely irrelevant at this point in our understanding except as historical footnotes.

Linear logic is in many ways a logic of logic. Both classical and intuitionistic logic can be decomposed into finer components in linear logic, which distills logical ideas into purer components of philosophical interest, like the exponentials. The links between linear logic and processes like computation makes it a much more interesting starting point for a discussion of metaphysics and logic: Its technical results tell us that not every bespoke Broccoli logic makes sense, that one can directly study the conditions of possibility of logic. It even has connections to fundamental physics [1].

> It's trivial that we can construct a plethora of axioms with their own definitions, the problem remains: to even adhere to those definitions one is exercising another intuitive logic—even in the case of computation which is an engineered construction to proxy this very intuition, otherwise we would have never been concerned with the linear properties necessary for computation to begin with.

How are we to investigate this intuitive logic without probing the technical structure of logic and finding out what is really its essence? It's not, emphatically not trivial that one can cook up a bunch of axioms. Logic doesn't come from axioms, I think we agree about that, they are just an exigent way to surface it. There are most definitely inappropriate formulations of logic. For example, S4 is an OK modal logic of necessity and possibility but S5 is hardly a logic at all because it doesn't have cut elimination, the technical correlate of deduction.

I think this attitude just serves to marginalize philosophy of logic. Technique and philosophy must be in dialogue or both will be marginalized.

[0] https://www.urbanomic.com/book/synthetic-philosophy-of-conte...

[1] https://arxiv.org/abs/0903.0340

The author cares about that, it's his abstract. In the same way a scientist would care about the precision and conclusions of results obtained from an older study--you are forced to use the original researchers had. Of course you can verify it with new tools, but what's the point if the research is systemically flawed to begin with?

The childhood quote hammered into our ears continues to ring true: "If I have seen further it is by standing on the shoulders of Giants."- Newton

I agree that newer technical formal languages describing our own methods of sound predicate are useful, but that's excessive and even pretentious in this case. Would you use quantum computation to verify the result of addition on a classical computer? It adds nothing, especially when it is quantum computation that is being construed to emulate classical computation!

>How are we to investigate this intuitive logic without probing the technical structure of logic and finding out what is really its essence?

Its essence cannot be discovered, there are "exigent way[s] to surface it", but like experience, it's atomic. In the end the models will just become more comprehensive in terms of formalizing experience. Yet the experience of logic is the essence; how are you able to describe what makes up experience in terms of experience? If this is the purpose of these "tools" (it's not) then they ought not to be limited by objects of human experience, as the noumenon (the negation of experience) is not even guaranteed to be symbolic to objects of perception—by definition they are not.

I would be flummoxed to find fundamental physics constructed, described, and extended from axioms through logic had no connection with logic.

Philosophy of logic continues to discuss other logics, it is only that this particular article that it's of no concern to.

> Philosophy without technical input is sophistry, technical developments without philosophy end up answering questions of no interest.

This is such a great formulation.

I should say, definitely not mine. I don't know where I got it, or where they got it.

Logic, to be of any use in the real world, must in some important ways match the reality of the world. So any system of logic assumes a metaphysics. And going the other way, reality must be such as to be able to have creatures who can think logically.

This is one instance of a larger principle, namely the inherent mutual interconnectedness of the various areas of philosophy. So for instance, epistemology depends on reality being such that it can be known, and we can know about that reality only the sorts of things that a valid epistemology can determine. Similar mutual relations exist between every two main areas of philosophy.

This mutual interconnectedness is a key reason for Neurath's insight that in philosophy you can't tear it all down and change it radically, but only modify it.

Isn't logic simply the understanding of cause and effect and choosing to deny or approve of a cause depending on the level of accuracy of the effect on the context. eg. Santa doesn't exist inside conventional norms. Santa could have existed, however we don't know. We have no cause to say he does exist.

Ancient Greek philosophy was divided into logic, physics and ethics. Metaphysics was categorized as logic.

The first step in any logic is to make a distinction. This act is within the mind. The world itself is unknown except as sensory experience. Leaving aside the so-called "Hard Problem of Consciousness" for the sake of discussion, the fact that distinction happens in our heads means that all of our logic is contingent (as opposed to inherent) if our thinking is wholly internal to our brains.

However... none other than Kurt Gödel believed that thinking about e.g. infinities involved a kind of perception of a "higher" world.

"Science does not remove the Terror of the Gods."

Logic is based on the principle of non-contradiction (identified by Aristotle). The principle, in all its various forms, is used to guide valid thinking (i.e. truth) because contradictions cannot exist which is its tie to metaphysics.

"Logic is based on the principle of non-contradiction"

That's merely one type of logic. There are others which can deal with contradictions. See the Wikipedia entries on Paraconsistent logic[1] and Dialetheism[2].

Logicians enjoy coming up with new logics that have any desired or interesting properties. They are not limited to staying within the bounds of classical logic.

[1] - https://en.wikipedia.org/wiki/Paraconsistent_logic

[2] - https://en.wikipedia.org/wiki/Dialetheism

The key to understanding logic constructively goes through type theory, not philosophy.

I'll just leave this here https://78.media.tumblr.com/bfc158b432199a3e4f5de2ddc1bd7381...

The progenitor of types was Russell, who considered himself a philosopher.

>goes through type theory, not philosophy.

You’re going to be very surprised when you look up the origins of type theory.


Not that much surprised. History of type theory is a history of trying to define precisely computation. That is, try to allow recursion but enforce that all programs terminate.

The solution to this problem these days is to use a purely functional programming language with dependent types (e.g. Homotopy Type Theory, Lean).

Haskell, for example, being a practical functional programming language, is logically inconsistent. Using the fix function:

  fix :: (a -> a) -> a
  fix f = let x = f x in x
one can produce proof of everything

  Prelude Data.Function> :t fix id
  fix id :: a
that is just an infinite loop.

In a logically consistent functional language such as Lean https://leanprover.github.io, this definition is not allowed.

So you think the key for understanding constructive logic is to understand some peculiar syntax for a fragment of it. Ridiculous, but sadly quite typical among type theory cultists.

> So you think the key for understanding constructive logic is to understand some peculiar syntax.

It's not only a syntax, it's a functional programming language which turns out to be a computational model for logic.

No one is saying type theory is useless, particularly when it comes to computation. It works within its own boundaries, but it does indeed have boundaries. There is a reason the ZFC has triumphed in mathematics.

Not really. The boundaries of type theory (say HoTT) are exactly what is possible on a Turing machine (computable). And a step beyond those throws ZFC itself into paradoxes (say Russel's). Moreover ZFC is directly expressible in type theory https://hott.github.io/book/nightly/hott-online-1174-g29279f...

I agree regarding the completeness of type theory in regards to Turing computability.

But I disagree regarding paradoxes in ZFC. Russel's paradox specifically applies to naive (simple Cantor) set theory, something the ZFC was explicitly designed to address with its axioms of choice and infinity. Furthermore the HoTT is itself expressible in the common extension of ZFC which adds at least one inaccessible cardinal.

And, mathematically speaking, the ZFC excels in dealing with infinities, which is more difficult (though possible) in the various type theories.

I agree with everything besides your stated difficulties with infinities in type theory. Here's one infinity

  inductive ℕ : Type
  | zero : ℕ
  | succ (n : ℕ) : ℕ
the type of natural numbers with cardinality ℵ₀. Here' s a bigger infinity:

  ℕ → ℕ
the type of functions over natural numbers.

From then on one can start talking about different injective functions between those types and infer cardinality of which is bigger and so forth and so forth.

It's values, types and functions all the way down. Nothing from ZFC is lost, on the bright side, your proofs are checked by a computer. On an even brighter side, your proofs can be semi-automated, even brute forced.

Also set theory vs type theory (in Math) is really just dynamic typing vs static typing (in CS). And we already know how that played out in CS.

Anyone who prefers type theory to (non-naive) set theory does so for philosophical reasons. Therefore your argument is self-defeating.

Source, pretty please?



Homotopy Type Theory: Univalent Foundations of Mathematics


Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact