# Tag Info

Accepted

### How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

The simply-typed $\lambda$-calculus is not stronger than second-order logic. The simply-typed $\lambda$-calculus has: product types $A \times B$, with corresponding term formers (pairing and ...
• 48k

### Do combinatory logic bases need a function of 3 variables?

A Basis Result in Combinatory Logic, Remi Legrand, J. Symb. Logic 53.4 (1988), pp. 1224-1226. The aim of this article is to show that a basis for combinatory logic must contain at least one ...
• 6,571

### Do combinatory logic bases need a function of 3 variables?

@PeterTaylor’s excellent answer points to exactly the result wanted. But the proof there can be streamlined a bit, and may be paywalled for some readers, so I’ll write it out here for accessibility. ...
Accepted

### What is Chemlambda? In which ways could it be interesting for a mathematician?

UPDATE (2020) There is now chemlambda.github.io which collects all the chemlambda related projects and articles. For the history of chemlambda see arXiv:2007.10288 or the associated html version Graph ...
Accepted

### Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

The point is that the reflection rule makes $p = \mathsf{refl}_x$ a well-formed expression. This turns out to be incredibly dangerous: now we can prove it by induction on equality. More precisely: ...
• 14.9k

### Is there a proof of strong normalisation that uses ordinal numbers?

I believe that Chapter 4 of Girard's Proofs and Types proves weak normalization for typed $\lambda$-calculus in this way, using ordinals up to $\omega^2$. He first assigns a natural number "...
• 65.1k
Accepted

### Easier Girard's paradox in a circular pure type system (PTS)

I feel like most of my posts on mathoverflow and cstheory.stackexchange consist of this answer, but the most perspicuous (in my opinion) proof of inconsistency of U and $*:*$ is a construction by ...
• 1,140
Accepted

### How to handle sums in Tait's reducibility proof of strong normalisation?

The typical strategy when you're building a model to perform normalisation by evaluation (i.e. the computational part of Tait's method, see [1]) with sum types is to have as a semantics for ...
• 455
Accepted

### Relationship of lambda calculus to the rest of math

The question you are trying to ask is "What is a denotational semantics for the untyped lambda calculus?" This is a difficult problem because, as Bjorn Kjos-Hanssen said in his answer, if you try and ...
• 1,544

### Is there a proof of strong normalisation that uses ordinal numbers?

As far as I know, such a strong normalization proof is not known even for the simply-typed $\lambda$-calculus. It is mentioned as Problem 26 in the TLCA List of Open Problems. (It must be noted ...
• 1,536

### An overview of mathematical-logical approaches in formalizing natural languages

Here is what I answered in Math.SE: If you haven't read it already, I highly recommend reading L. T. F. Gamut's Logic, Language, and Meaning. If you already know some logic (say, up to first-order ...
• 181
Accepted

### Consistency in pure type systems

I think this awkwardness is coming from your “principle of constants”, which is not standard, and doesn’t seem justified by the motivation you give. You say it’s meant to correspond to the practice (...
Accepted

### Is every total computable function definable by a normalizing lambda term?

Yes, you can actually encode all computable functions by normalizable terms since it is always possible to turn a term into a normal form which computes the same function on Church's numerals. We just ...
• 4,410

### Scott on the consistency of the lambda calculus

Not exactly λ-calculus, but untyped formalisms in general. Here is an excerpt from the introduction of A type-theoretical alternative to ISWIM, CUCH, OWHY (bold emphasis is mine): No matter how ...
• 163

### Is simply typed lambda calculus with fixed-point combinator Turing-complete?

Damiano is right, the answer is no: it is not Turing complete. Supposing to define natural numbers as some type (o->o)->o->o, even with fixpoints you cannot define the predecessor (that would be ...
Accepted

### Is simply typed lambda calculus with fixed-point combinator Turing-complete?

The simply-typed $\lambda$-calculus with the fixpoint combinator but without a primitive integer type is not Turing-complete, at least not in the usual sense (Church integers and computation as $\beta$...
• 1,536

### How to handle sums in Tait's reducibility proof of strong normalisation?

Let me add to the above (perfectly correct) answers that there is a more general perspective, which works for all positive connectives, of which sums are a special case. The fundamental insight is ...
• 1,536
Accepted

### Internal language proof of Lawvere's fixed point theorem for cartesian closed categories

You're right that the statement of the theorem, and the entirety of the proof, don't fit inside the internal logic of a CCC. However, once given $f:B\to B$, the definition of $q$ and the proof that ...
• 65.1k

### How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

Simply typed lambda calculus and simple type theory are not equivalent. The former only has rules for alpha- and beta-reduction, the latter also has rules for Modus Ponens, extensionality and the ...
• 151

### An overview of mathematical-logical approaches in formalizing natural languages

This is a really a question about linguistics rather than mathematics, so you might be better off asking your question on Linguistics StackExchange rather than here. But anyway, I think what you're ...
• 78.3k
Accepted

### Selection terms in the untyped lambda calculus

No such terms can exist. Here's a proof, way too convoluted for my tastes, but I don't have time to find a better one. The proof uses a lot the so-called Genericity Lemma, a standard result the proof ...
• 1,536

• 2,147
1 vote

### Criterion for the consistency of pure type systems

I'll write some fragment of thoughts here. First some known results. All the lambda cube is consistent (and normalizing, though I didn't mention it in the question, I'm also interested in that). A ...
• 1,031
1 vote

### Relationship of lambda calculus to the rest of math

First, these are not functions. These are lambda expressions that can be artistically interpreted as functions. If you want to model lambda theory in a theory where functions are a part of the ...

Only top scored, non community-wiki answers of a minimum length are eligible