Adam
  • Member for 12 years, 1 month
What programming languages do mathematicians use?
33 votes

Haskell is very popular with category theorists.

View answer
In set theories where Continuum Hypothesis is false, what are the new sets?
20 votes

You might not get new sets -- you might get fewer bijections between the sets you already have! Sometimes getting more cardinals means having fewer sets.

View answer
Difference between turnstile and implication
13 votes

@Joel's answer is concise and correct, and I am glad that @Henry mentioned the connection to modal logic. I'd like to add one more perspective: they seem similar because -- when you look at the right ...

View answer
What are κappa-categories?
Accepted answer
12 votes

The intuitive explanation is that $\kappa$-categories are to first-order functions what cartesian closed categories are to higher-order functions. This all started with Lambek's work on polynomial ...

View answer
Categorical foundations without set theory
12 votes

You write: "set theory permeates the formulation of first order logic. In first order logic, structures are sets together with constants" No; first order logic does not assume any set theory. The ...

View answer
Russell and Whitehead's types: ramified and unramified
Accepted answer
11 votes

Yes, this still occurs in modern type theory; in particular, you'll find it in the calculus of constructions employed by the Coq language. Consider the type called Prop, whose inhabitants are logical ...

View answer
What are your favorite instructional counterexamples?
10 votes

"Every finitely-branching tree with infinitely many nodes has an infinite branch" is constructively false, as witnessed by the following counterexample: http://math.andrej.com/wp-content/uploads/2006/...

View answer
Logical problems in category theory
7 votes

Short answer: category theorists often elide the extra annotations when employing typical ambiguity or universe polymorphism. Proof theorists demand that these annotations be provided, and study how ...

View answer
Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?
6 votes

What are the consequences of technically proving anything in Coq? This is a question in the Coq faq.

View answer
What is the manner of inconsistency of Girard's paradox in Martin Lof type theory
6 votes

It leads to a well-typed term, having no normal form, which is assigned the type False. You can find the term given explicitly in A simplification of Girard's paradox

View answer
Models of ZFC Set Theory - Getting Started
6 votes

You're supposed to think of sets. Definitely. Here's an analogy you might find helpful: let's use the name "ZFC-" for the axioms of ZFC but without the axiom of infinity. Now, if I suddenly decreed ...

View answer
Machine model for primitive recursion?
5 votes

If you're willing to accept register machines (rather than just tape machines), you can get what you want via the Grzegorczyk hierarchy, which generates the class of primitive recursive functions in ...

View answer
What category without initial object do you care about?
5 votes

Any programming languages based on lambda calculus (Haskell, (OCa)ML, Clean, Coq, Agda) forms a category -- in many different ways, in fact. One way is to have an object for each type of the language ...

View answer
How would one even begin to try to prove that a simple number-theoretic statement is undecidable?
5 votes

I had similar questions, and after stumbling around for a long time figured out that Kaye's book Models of Peano Arithmetic is pretty much the first book to read if you want to start building ...

View answer
How do they verify a verifier of formalized proofs?
5 votes

See question #5 in the Coq FAQ: http://coq.inria.fr/faq "You have to trust that the implementation of the Coq kernel mirrors the theory behind Coq. The kernel is intentionally small to limit the ...

View answer
'Closure' of CFLs under complementation and intersection
Accepted answer
4 votes

Grammars involving the usual context-free operations plus intersection are called conjunctive grammars. Adding negation (in addition to intersection) gives boolean grammars. Alexander Okhotin has ...

View answer
Theory mainly concerned with $\lambda$-calculus?
Accepted answer
4 votes

"combinatory logic"

View answer
What are interesting families of subsets of a given set?
4 votes

A ZF-algebra (as in Algebraic Set Theory) is a collection of sets closed under singleton and union. A Grothendieck Universe (aka strongly inaccessible cardinal, aka model of set theory) is a ...

View answer
Computer Science for Mathematicians
3 votes

Well, if you want to know how computers work, the authoritative reference on computer architecture happens to have been written by a set theorist! John von Neumann. First Draft of a Report on the ...

View answer
Provable(P) ⇒ provable(provable(P))?
3 votes

In order to talk about provability, we need to say what provability is. There are basically two options: Define an explicit provability predicate: encode some proof calculus in the natural numbers, ...

View answer
Context free grammar + functions = ?
3 votes

Just as a bit of a "big picture" comment... most grammatical formalisms are chosen for parsing use because they admit efficient implementations as some sort of automaton. An automaton implementation ...

View answer
Is functional programming a branch of mathematics?
3 votes

I think most people here would agree that Category Theory is part of mathematics. The study of strongly-typed functional programming languages is really just the study of cartesian closed categories, ...

View answer
Proper classes and their consequences
2 votes

Off-hand, I can think of at least two reasons why a collection whose elements are all sets might fail to be a set: The collection is too big (which you've mentioned) The collection is too complicated....

View answer
What do I call type theory without Curry-Howard?
2 votes

"Term category of a hyperdoctrine." The hyperdoctrine approach to categorical logic segregates the individuals (terms inhabiting types) in a category completely apart from the categories containing ...

View answer
How to think like a set (or a model) theorist.
2 votes

I think the more fundamental question to ask is why set theorists insist that the axioms of set theory be strictly first-order in nature (*). I claim that you can't really explain the motivations of ...

View answer
Generalizations of PA and its standard and non-standard models
1 votes

Regarding Question 2, rather than having finitely many function symbols $S_n(x)$, the easiest solution is to have a single relation symbol $S(n,x,m)$ asserting that the "$n$-labeled" successor of $x$ ...

View answer
Can dependent sums be encoded as dependent products?
1 votes

The statement "for any type-indexed family of propositions exists a proposition isomorphic to their coproduct" is inconsistent with impredicative type theory (CC); this leads to Girard's Paradox. The ...

View answer
How much of the current logic is about syntax?
0 votes

I would posit that proof theory is exactly the syntactical part of logic, and the other three branches (set theory, model theory, and recursion theory) are what's left when you get rid of the syntax. ...

View answer