13 Matching Annotations
1. Sep 2023
2. en.wikipedia.org en.wikipedia.org

#### URL

3. en.wikipedia.org en.wikipedia.org
1. In type theory, product types (with no field names) are generally preferred due to their simplicity

#### URL

4. Dec 2022
5. math.stackexchange.com math.stackexchange.com
1. My freely downloadable Beginning Mathematical Logic is a Study Guide, suggesting introductory readings beginning at sub-Masters level. Take a look at the main introductory suggestions on First-Order Logic, Computability, Set Theory as useful preparation. Tackling mid-level books will help develop your appreciation of mathematical approaches to logic.

This is a reference to a great book "Beginning Mathematical Logic: A Study Guide [18 Feb 2022]" by Peter Smith on "Teach Yourself Logic A Study Guide (and other Book Notes)". The document itself is called "LogicStudyGuide.pdf".

It focuses on mathematical logic and can be a gateway into understanding Gödel's incompleteness theorems.

I found this some time ago when looking for a way to grasp the difference between first-order and second-order logics. I recall enjoying his style of writing and his commentary on the books he refers to. Both recollections still remain true after rereading some of it.

It both serves as an intro to and recommended reading list for the following: - classical logics - first- & second-order - modal logics - model theory<br /> - non-classical logics - intuitionistic - relevant - free - plural - arithmetic, computability, and incompleteness - set theory (naïve and less naïve) - proof theory - algebras for logic - Boolean - Heyting/pseudo-Boolean - higher-order logics - type theory - homotopy type theory

#### URL

6. Nov 2021
7. www.typescriptlang.org www.typescriptlang.org
1. the name union comes from type theory. The union number | string is composed by taking the union of the values from each type. Notice that given two sets with corresponding facts about each set, only the intersection of those facts applies to the union of the sets themselves.
2. For example, if we had a room of tall people wearing hats, and another room of Spanish speakers wearing hats, after combining those rooms, the only thing we know about every person is that they must be wearing a hat.

#### URL

8. Mar 2021
9. en.wikipedia.org en.wikipedia.org
1. How is it that https://en.wikipedia.org/wiki/Type_theory links to https://en.wikipedia.org/wiki/Type_(model_theory) but the latter does not have any link to or mention of https://en.wikipedia.org/wiki/Type_theory

Neither mentions the relationship between them, but both of them should, since I expect that is a common question.

#### URL

10. en.wikipedia.org en.wikipedia.org
1. In fact categories can themselves be viewed as type theories of a certain kind

#### URL

11. en.wikipedia.org en.wikipedia.org

#### URL

12. Jul 2020
13. osf.io osf.io
1. Halford, E., Dixon, A., Farrell, G., Malleson, N., & Tilley, N. (2020). Crime and coronavirus: Social distancing, lockdown and the mobility elasticity of crime [Preprint]. SocArXiv. https://doi.org/10.31235/osf.io/4qzca

#### URL

14. Dec 2015
15. math.mit.edu math.mit.edu
1. Since ducks can both swim and fly, each duck is found twice inC, once labeled as aflyer and once labeled as a swimmer. The typesAandBare kept disjoint inC, whichjustifies the name “disjoint union.”

The disjoint union reminds me of algebraic datatypes in functional programming languages, whereas a set-theoretic union is more like a union in CS: the union has no label associated with it, so additional computation (or errors) may arise due to a lack of ready information about elements in the union.

2. An aspect of a thingxis a way of viewing it, a particular way in whichxcan be regardedor measured. For example, a woman can be regarded as a person; hence “being a person”is an aspect of a woman. A molecule has a molecular mass (say in daltons), so “havinga molecular mass” is an aspect of a molecule. In other words, byaspectwe simply meana function. The domainAof the functionf:A—Bis the thing we are measuring, andthe codomain is the set of possible “answers” or results of the measurement.

Naïvely (since my understanding of type theory is naïve), this seems to mesh with the concepts of inheritance for the "is" relationships, and also with type-theory more generally for "has" relationships, since I believe we can view any object or "compound type", as defined here, as being a subtype of another type 'o' if one of its elements is of type 'o'. Though we have to be careful for functional mapping when thinking of aspects: we can't just say Int is an aspect of Pair(Int, Int), since this is ambiguous (there are two ints) --- we must denote which Int we mean.

3. We represent eachtype as a box containing asingular indefinite noun phrase.
4. In 1980 Joachim Lambek showed that the types and programs used in computerscience form a specific kind of category. This provided a new semantics for talking aboutprograms, allowing people to investigate how programs combine and compose to createother programs, without caring about the specifics of implementation. Eugenio Moggibrought the category theoretic notion of monads into computer science to encapsulateideas that up to that point were considered outside the realm of such theory.