Skip to main content

Questions tagged [types]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
0 answers
25 views

Where does the type of practical reason fit into Kant's layered terminology?

At one point in the first Critique, Kant shoots off this list of stipulative definitions: We are in no want of words to denominate adequately every mode of representation, without the necessity of ...
Kristian Berry's user avatar
2 votes
0 answers
91 views

Seeking a quote of Russell on what he could conceive or discuss

At some point someone asked Bertrand Russell about formal logical language without distinctions of type. (I think it might have been Quine, who was developing for example kinds of algebraic logic ...
Colin McLarty's user avatar
2 votes
3 answers
683 views

Can something be both a type and a token?

I wonder, can something be both a type and a token (in reference to the type-token distinction in philosophy)? For example, an individual dog is a token of the type of dog, but the type of dog is ...
user107952's user avatar
  • 7,632
0 votes
0 answers
48 views

Mathematical "forms" as a relation of varying arity

This might be more a MathSE question, but on the other hand, it would involve a peculiar reimagining of the relation between set theory and type theory, so I'll try it out here. OK, so earlier I ...
Kristian Berry's user avatar
10 votes
3 answers
6k views

Set theory vs. type theory vs. category theory

IIRC, in the univalent-foundations program (per Voevodsky), category theory is represented as a possible sort of evolution or new wave of type theory. Maybe my memory is off, but anyway, in nlab they ...
Kristian Berry's user avatar
1 vote
0 answers
75 views

Is there a materialist explanation for the type-token distinction?

Is there a materialist theory in philosophy that goes beyond giving a dictionary definition of the type/token distinction and attempts to explain what types and tokens really are in material terms, e....
ali's user avatar
  • 267
1 vote
1 answer
101 views

The type of all types, the type of being a token

Do descriptions like those result in paradox or antinomy like "set of all sets" or (nLab seems to say at one point) "category of all categories" do? It seems that the type of types ...
Kristian Berry's user avatar
1 vote
2 answers
170 views

Can the paradox of the gentle murderer be resolved using the sentence-type/token distinction?

Quick recap: the paradox in question can be formulated like so (I think; look in the SEP article on deontic logic for a better recap if this doesn't work): If Jill kills Jane, she ought to kill Jane ...
Kristian Berry's user avatar
2 votes
2 answers
994 views

What's an intuitive way of thinking about type versus token identity?

What's an intuitive way of thinking about type versus token identity? I have read and understand the difference between those two terms: tokens are things in space and time; types are abstract and ...
user avatar
1 vote
1 answer
391 views

Given proofs of A → B and A, when do we get a proof of B?

In intuitionistic mathematics, a proposition is true only when a proof of it has been experienced. Following the BHK semantics, a proof of A → B is an algorithm that, when given a proof of A, will ...
mudri's user avatar
  • 153
-3 votes
1 answer
137 views

Why can't type theory be applied on personality types? [closed]

Given that type theory is a system for describing mathematics, and given that "Math can be applied everywhere", why is it that type theory can't seem to be applied to personality type theory? I've ...
damat-perdigannat's user avatar
3 votes
1 answer
548 views

What it the relationship between Type theory and logic?

I am aware that a similar question was asked about the type theory in the principia, but I'm more interested in what the relationship between, say Martin-Lof Type theory and intuitionistic logic is.
Carlo Lori's user avatar
7 votes
1 answer
520 views

Are Univalent Foundations of mathematics a modern version of logicism?

As I understand it (and mine is just basic understanding) the Univalent Foundations program is an attempt to reduce mathematics to an interpretation of Martin-Löf type theory by using homotopy theory....
Carlo Lori's user avatar
5 votes
1 answer
373 views

What types of inconsistency are there that we know of?

Just trying to verify consistency of a system, I need to have a list types of inconsistency to look out for, so far I have the followings: 1.Anachronistic inconsistency (e.g. trying to read a file ...
jimjim's user avatar
  • 788
2 votes
2 answers
349 views

In sequences of tokens that cannot repeat, can types occur twice?

This article suggests that a type can occur more times than it has tokens. e.g., the type mister smith has a single token but occurs twice in the list of lottery winners. The article bases that on ...
user avatar
6 votes
2 answers
1k views

What is the difference between Aristotle's theory of categories and Russell's theory of types?

A partial answer might come through an introduction. Well, we know that Russell's efforts to understand the contradictory appearance of the class of all classes not members of themselves (a notion ...
Dallas-Rey Davis's user avatar
8 votes
2 answers
190 views

Is there any relation beetwen justification logic and type theory?

Justification logics, was introduced by Sergei Artemov, are epistemic logics which allow knowledge and belief modalities to be ‘unfolded’ into justification terms: instead of □X one writes t:X, and ...
Ali's user avatar
  • 181
1 vote
1 answer
123 views

How are sortals different than types?

The criteria for a sortal from Wikipedia: gives a criterion for counting the items of that kind gives a criterion of identity and non-identity among items of that kind gives a criterion for the ...
Hal's user avatar
  • 1,230
11 votes
1 answer
783 views

What are the differences between Tarski's 1933 and 1956 truth definitions?

The paper "The Seven Virtues of Simple Type Theory" mentions that it uses the same trick (due to Tarski) to define the semantics that is also used by first-order logic. I interpreted this a reference ...
Thomas Klimpel's user avatar