Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [types]

The tag has no usage guidance.

2
votes
2answers
224 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 ...
1
vote
1answer
336 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 ...
-3
votes
1answer
111 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 ...
4
votes
1answer
403 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.
6
votes
1answer
359 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....
4
votes
1answer
145 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 ...
0
votes
2answers
263 views

Types with only one token

This article seemed to me to suggest that a kind can occur more times than it has tokens, even if the token is a concrete object. E.g. mister smith is a single token that occurs twice in the list of ...
4
votes
2answers
638 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 ...
7
votes
2answers
151 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 ...
1
vote
1answer
83 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 ...
13
votes
1answer
532 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 ...