1
vote
1answer
69 views

How to extract the sets “produced” by a axiomatic set theory, into some newly introduced collection?

Say I know well how to reason in a set theory, which for the sake of this question I'll call $\bf{ST}$, say one of those, it can by $\bf ZFC$. It's principally written down via first order logic and ...
3
votes
0answers
37 views

Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models ...
5
votes
0answers
106 views

Axiom of Choice - Type Theory (Proof)

Background In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory ...
2
votes
1answer
87 views

Unprovable Equivalence in Type Theory

Let $\prec$ be a binary relation on a set $A$… A predicate $P(x)$ set $(x:A)$ is said to be progressive with respect to $(A,\prec)$ if \begin{equation} (\forall a:A)\Big((\forall b:A)\big(b \prec a ...
4
votes
0answers
144 views

Foundational theories, their uses, interactions and comparisons?

Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are: Set theory; Logic; Category theory; Type ...
4
votes
1answer
97 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
1
vote
1answer
57 views

How to construct a term of a particular type

I am reading the article "Introduction to Type Theory" by Herman Geuvers, the chapter explaining the Fitch style of natural inference. I stuck at the exercise 1.3 (first two are simple): ...
0
votes
1answer
68 views

What can be proven within Simply Typed lambda calculus?

I was reading http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus and I'm having a hard time thinking of anything remotely interesting that can be proven within Simply Typed lambda calculus. Am ...
6
votes
1answer
407 views

Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory

I understand there is propositional logic, first-order logic, second-order logic higher-order logic, and type theory, where the latter logics are extensions of the former logics. Can someone explain ...
4
votes
2answers
124 views

Is higher order type theory the same as higher order logic?

The internal language of a topos is higher order intuitionistic type theory (or logic). Here the higher order simply refers to allowing function types. In mathematical logic we have higher-order ...
9
votes
0answers
149 views

Reference on standard types

This question is about what I presume is a basic construction in type theory. The finite types are defined as follows: 0 is a finite type; if $\sigma, \tau$ are finite types, then so is ...
3
votes
3answers
187 views

Book on lambda calculus logic and type theory

Can someone recommend me a book for self study which will cover topics of logic, lambda calculus and type theory. I know about "Computability and Logic" written by Bolos but it describe recursive ...
5
votes
2answers
87 views

Is there a theory of extensible definitions?

We can define $+$ as a function $\mathbb{N}^2 \rightarrow \mathbb{N}$, and then prove: Theorem 1. The range of $+$ is $\mathbb{N}$. If we later wish to extend $+$ to a function $\mathbb{Z}^2 ...
2
votes
2answers
51 views

mapping simple first oreder problems to type theory

Since Peano axioms expressed in type theory doesn't seem to be going anywhere, here is a simpler question: How would I map simple first order systems to an equivalent type theoretic notation. ...
7
votes
1answer
370 views

Intuitionistic Banach-Tarski Paradox

While the Banach-Tarski paradox is a counter-intuitive result which requires the Axiom of Choice, leading some people to argue specifically against Choice, and others to argue for constructive ...
3
votes
2answers
589 views

Curry-Howard correspondence

I read that the Curry-Howard correspondence introduces an isomorphism between typed functions and logical statements. For example, supposedly the function $$\begin{array}{l} I : \forall a. a \to a\\ ...
11
votes
2answers
908 views

Classic type theory textbooks

There are many classic textbooks in set and category theory (as possible foundations of mathematics), among many others Jech's, Kunen's, and Awodey's. Are there comparable classic textbooks in ...
2
votes
2answers
243 views

Has a Dependent Type always a Type?

I am experimenting with dependent types. Lets assume the following short notation: ...
2
votes
0answers
70 views

Introductory text about different stratification methods in higher-order logic and set theory

Could someone recommend me a good overview text about stratification of predicates, comprehension axioms, and other methods of avoiding the paradoxes in untyped or only loosely/relatively typed ...
1
vote
2answers
299 views

formal rules for avoiding bound/unbound variable problems in lambda calculus

I have been interested in learning formal math formally enough so that I could write a proof assistant using some simple parsing tools, and explain to someone else with little math knowledge how to ...
38
votes
6answers
4k views

Learning Lambda Calculus

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus? Specifically, I am interested in the following areas: Untyped lambda calculus ...