Type theory in classical logic?

Stream: Type theory

[Martin Dvořák]

Why is type theory defined in the Intuitionistic logic? Would it be possible to build (some kind of sufficiently strong) type theory in the First-order (classical) logic instead?

I am not talking about Howard-Curry correspondence and interactive theorem provers. I am talking about type theory as a foundation for MathematiCS; in case we want to replace set theory by type theory. Are there any fundamental obstacles?

[Mac]

@Martin Dvořák I think the conceptual problem is that a type theory in classical logic would just be category / set theory. The distinctions would disappear.

[Martin Dvořák]

I am sorry; I don't understand your answer.

[Mac]

A type is, essentially, a constructive/Intuitionistic set/class. That is, in classical logic, a type and a set / class would just be equivalent.

[Reid Barton]

Type theory isn't defined in any "external" logic

[Karl Palmskog]

the initial type theories (first one by Russell & Whitehead in Principia, second one by Church in his paper on simple types) were designed to do classical reasoning. In the case of Church, this is why proof assistants based on HOL get LEM out of the box. People used classical logic both inside and outside the initial type theories (i.e., when reasoning about their respective metatheory)

[Martin Dvořák]

Is it impossible to define a simply-typed λ-calculus as a theory in FOL? The universe would contain a superset of all correct terms and for each type you would have a unary relational operator that would tell you whether the argument is a term of the given type. I believe there is some catch but I don't know where.

[Mario Carneiro]

you can embed anything in FOL like that

[Mario Carneiro]

well, you probably don't want an infinite set of relational operators, but you can get around that by representing types as elements of the domain and making typing a binary predicate

[Reid Barton]

You can certainly do this kind of syntactic embedding (and this is what you're doing when proving things about the metatheory of type theory) but whether the meta-logic satisfies LEM (for example) doesn't have anything to do with whether LEM is provable in the type theory itself

[Mac]

That is, the fact that the metalogic is classical does not equate to the embedded logic (type theory) being classical.

[Martin Dvořák]

Mario Carneiro said:

well, you probably don't want an infinite set of relational operators, but you can get around that by representing types as elements of the domain and making typing a binary predicate

Your suggestion sounds great for dependent type theory actually! Universe consists of all terms. And you will have an operator is_a_type_of that will take two terms to check the typing. However, I don't know how to avoid infinitely many functional operators in case we wanted the full range of inductive types.

[Mario Carneiro]

You encode inductive specifications as elements of the domain too, and have a "make inductive" term constructor

[Mario Carneiro]

I actually do exactly this in my encoding of lean in MM0, which is roughly FOL-based

[Martin Dvořák]

Mario Carneiro said:

You encode inductive specifications as elements of the domain too, and have a "make inductive" term constructor

Are inductive specifications terms themselves?

[Mario Carneiro]

no, in the MM0 formalization they are elements of a different "sort" (it is actually multi-sorted FOL); in plain one-sorted FOL everything has to live together in the same universe but you can have predicates like is_term(x), is_indspec(x) and assert that they are mutually disjoint

[Mario Carneiro]

This is also how type theories are translated to FOL for use with ATP programs (i.e. sledgehammer)

[Mario Carneiro]

(well, at least at the basic level; usually you don't go all the way to translating inductive specifications and opt for something more coarse grained that better fits the level of description of the goal)

[Mac]

Mario Carneiro said:

in plain one-sorted FOL everything has to live together in the same universe but you can have predicates like is_term(x), is_indspec(x) and assert that they are mutually disjoint

Note that this is just essentially reducing types to naive sets (i.e., the predicate is_term is equivalent to a naive set of terms), illustrating that types in classical logic are just sets / classes.

[Mario Carneiro]

@Mac Not necessarily. Since both types and terms are objects in the universe here, you can have two types t and u (such that is_type(t) and is_type(u)), which are not equal (i.e. t != u using FOL equality), such that ∀ x, has_type(x, t) <-> has_type(x, u), i.e. t and u are extensionally equal but not FOL-equal. (The relation between FOL-equal and type theory equality notions like propositional equality and defeq is somewhat flexible, but FOL-equal has to be the strongest equality notion, so it has to mean at least defeq, and it could even mean "syntactic equal", if the model is sufficiently syntactic so as to make this distinction.)

[Mac]

@Mario Carneiro wouldn't that be just as true for naive sets though to? That is, you can have two (naive) sets s and t such that s != t using FOL equality but forall x, x : s <-> x : t (i.e., are extensionally equal sets -- : being membership).

[Mario Carneiro]

no, because that's an axiom

[Mario Carneiro]

it's the first axiom in ZFC

[Mac]

but I was talking about naive sets, not ZFC?

[Mario Carneiro]

I assume by naive sets you mean that you are encoding a set theory of some description, and every set theory has an extensionality axiom

[Mario Carneiro]

otherwise it's not set theory

[Mac]

I naive set is just a set s is defined as x : s <-> P(x) where P is predicate defining the set

[Mario Carneiro]

s is not an object in that encoding

[Mario Carneiro]

so s = t is not well formed

[Mac]

fyi, by naive set, I mean a set from naive set theory i.e. that ones that encounter Russell's paradox if axiomatized.

[Mario Carneiro]

pretty sure extensionality is also the first axiom in frege's set theory axiomatization

[Mac]

in my example, both x and s are terms in first order logic and the set membership relation : is a relation between two a two terms, which for the set s is defined as x : s <-> P(s) where P is a the defining proposition. In our example, the set terms would be defined like x : terms <-> is_term(x).

[Mario Carneiro]

It's true that if : is an otherwise uninterpreted binary relation on objects then extensionality need not hold. Usually axiomatizing it is the first step in making it look like an elementhood relation

[Mac]

true, which is how russell's paradox emerges, but the theory can remain naive by simply doing as you said and leaving it uninterpreted outside the axiomatic definitions for specific sets.

[Mario Carneiro]

Note that in some presentations of naive set theory extensionality is instead taken as the definition of =, for example here

[Mac]

Fair enough, when I said naive set, I was mostly just thinking of sets defined in the way they are in Russell's paradox, but without the axiom of unrestricted comprehension restricted to specific predicates (i.e., the ones of interest). I was probably assuming that my notion was a bit more natural than it actual is.

[Mario Carneiro]

This page (https://en.wikipedia.org/wiki/Extensionality) also calls out extensionality as a defining difference between set theory and type theory

[Mac]

My main point though is that by reduce types to predicates in FOL, they lose most of what makes them types, and they could just as easily be reinterpreted as a kind of set.

[Mario Carneiro]

I don't believe that to be the case. To the extent that type theory is formalizable at all, it can be formalized in FOL

[Mario Carneiro]

this reduction is not lossy w.r.t. the intensional aspects of type theory, but identifying types with their extensions is lossy in this sense

[Mario Carneiro]

interestingly, it's even possible to formalize intuitionistic type theory in classical FOL without LEM "contamination" of the internal logic

[Mac]

Ah, oops, I think I figured out where my misunderstand was, I completely misread this statement:

Mario Carneiro said:

in plain one-sorted FOL everything has to live together in the same universe but you can have predicates like is_term(x), is_indspec(x) and assert that they are mutually disjoint

I thought that you where saying that x is of the type term would be encoded as is_term(x) or that x is of type indspec would be encoded as is_indspec(x). I for some stupid reason did not catch on to the fact that indspec was short for inductive specification and these where predicates about the logical structure and not about individual terms within the logic. :face_palm:

[Mario Carneiro]

the idea is that x is some particular term, for example nat is an element of the universe and is_term(nat) holds. Similarly (T. 1 + T) (or some such thing) is an element of the universe and is_indspec(T. 1 + T) holds, and nat != (T. 1 + T) holds (it's not necessary to assert this, but it is simpler to keep things in different syntactic categories as distinct), and let's say nat = mu(T. 1 + T) where mu is the equivalent of the inductive command, which makes types from inductive specifications

[Mario Carneiro]

term and indspec themselves are not objects in this encoding

[Mac]

Yeah, that makes perfect sense now that realized my error. Sorry for the unnecessary tangent!

[Mac]

@Mario Carneiro but as to the original question, that encoding is more reasoning about type theory in classical logic than doing type theory with classical logic, no? The question, as I saw it, was about that later, which I presumed to mean something like, for example, a simply typed lambda calculus where the terms are FOL terms/propositions.

[Mario Carneiro]

You can do reasoning about the theory in this encoding, but just doing type theory is also possible. Terms are FOL terms, and typing judgments are FOL proofs. (Type theory proof terms are FOL terms, which can get cumbersome but that's mostly a display issue - they are just as cumbersome in type theory proper, but the computer is usually good at hiding the complexity)

[Martin Dvořák]

Mario Carneiro said:

interestingly, it's even possible to formalize intuitionistic type theory in classical FOL without LEM "contamination" of the internal logic

For this purpose, Prop cannot by modelled by a relation symbol, right?

[Mario Carneiro]

@Martin Dvořák It can; you just don't have that ¬ (∃ x, has_type(x, p)) → ∃ x, has_type(x, ¬ p) which can be read "if p is not provable then ¬ p is provable"

[Mario Carneiro]

LEM in the outer logic means that (∃ x, has_type(x, p)) ∨ ¬ (∃ x, has_type(x, p)) is provable but this isn't much use for finding witnesses in the inner logic

[Martin Dvořák]

In type theory, we speak solely about provability, right?

[Martin Dvořák]

Is there any _semantics_ of type theory?

[Karl Palmskog]

pretty hard to prove an implementation of a type theory correct without any semantics, e.g., http://www.sigplan.org/Awards/Dissertation/2017_kumar.pdf#page=91

[Martin Dvořák]

Mario Carneiro said:

LEM in the outer logic means that (∃ x, has_type(x, p)) ∨ ¬ (∃ x, has_type(x, p)) is provable but this isn't much use for finding witnesses in the inner logic

If I understand you correctly, you are saying that the "outer" LEM (of FOL here) (∃ x, has_type(x, p)) ∨ ¬ (∃ x, has_type(x, p)) does not imply ¬ (∃ x, has_type(x, p)) → ∃ x, has_type(x, ¬ p), i.e., the LEM in the "inner system" (type theory). Am I right?

[Martin Dvořák]

The latter could be written as (∃ x, has_type(x, p)) ∨ (∃ x, has_type(x, ¬ p)) afaik.

[Reid Barton]

Martin Dvořák said:

The latter could be written as (∃ x, has_type(x, p)) ∨ (∃ x, has_type(x, ¬ p)) afaik.

This isn't LEM in the internal theory, because there will be undecidable statements

[Martin Dvořák]

Is ¬ (∃ x, has_type(x, p)) → ∃ x, has_type(x, ¬ p) LEM in the internal theory?

[Reid Barton]

no

[Reid Barton]

Also the two ¬ in that formula are not the same thing, so maybe we should write them differently

[Reid Barton]

LEM is ∃ x, has_type(x, p or not p)

[Reid Barton]

Or more precisely, this is the claim that the type theory proves p or not p for some specific p

[Martin Dvořák]

Reid Barton said:

Or more precisely, this is the claim that the type theory proves p or not p for some specific p

For any given p, right?

[Reid Barton]

A specific, given, and in all other ways predetermined p

[Martin Dvořák]

Can we add an axiom ∀ p : Prop, p or not p to our inner theory?

[Martin Dvořák]

On the implementation-in-FOL level, it would be ∃ x, has_type(x, (∀ p : Prop, p or not p)).

[Mario Carneiro]

yes, that's what LEM in the inner theory looks like

[Mac]

What does the outer FOL representation add to the setup in this case?

[Reid Barton]

It gives you a language to express metatheoretic properties of the type theory, e.g., soundness: ¬ (∃ x, has_type(x, false))

[Mario Carneiro]

Another major advantage of this representation is that the rules for proof are simply standard FOL (with axioms about has_type), rather than requiring a custom verifier. This is very useful for connecting DTT to standard logic, since FOL is much more "canonical" in its design than type theory, which has many knobs at the foundation like what things are defeq to what other things

[Steven Obua]

@Martin Dvořák
You can also try to embed type theory directly into classical logic, that is what I am trying to do with Practical Types.
At the moment though I am occupied with the target of the embedding. I believed initially it is first-order logic, but it actually is Abstraction Logic. I believe type theory will embed very naturally into Abstraction Logic just by means of axioms; I believe that because I think that any sensible logic can be embedded into Abstraction Logic via axioms. That might be easy to show in principle just by embedding first-order logic into Abstraction Logic, and then cite @Mario Carneiro 's work for the other embeddings :laughing:

[Steven Obua]

@Mario Carneiro Do you have a writeup somewhere about how you embed Lean into mm0? I checked out the link, but that example is too dense for me to understand it easily.

[Mario Carneiro]

@Steven Obua No, it is still unfinished and on hiatus, so I have only gotten as far as the axioms (I would like to be producing proofs from lean export files at some point). The rules for inductives are pretty complicated, because we basically have to simulate a program that reads the indspec and decides whether it is strictly positive and implements all the edge case stuff right. But feel free to ask about how the predicates work or something.

At a high level it's not too hard to see what it's doing: we have a sort for terms/types and there is a predicate Gamma |- e : A that has axioms corresponding to the rules of the judgment. These rules should all be fairly recognizable from the lean type theory paper, except possibly for the one that has to evaluate a substitution. (Here the complication is that substitution is not actually a type operator, it is a metafunction that operates at the level of terms, so we need a bunch of rules to describe what it does.)

[Steven Obua]

This paper is perfect, that is probably what I was looking for in the first place, thanks!

[suhr]

But Howard-Curry correspondence is exactly how you derive an intuitionistic type theory in the first place! It is essentially Heyting–Kolmogorov interpretation applied to the intuitionistic natural deduction.

Are there any fundamental obstacles?

Computability is sort of blind spot of classical mathematics, and type theory takes an advantage of things being computable. In classical systems like HOL you have to rely on some heavy proof automation even for basic proofs.

[Mario Carneiro]

You certainly don't need to rely on proof automation for basic proofs. That's entirely an artifact of the proof assistant design. Type theory only changes the game a little by making it possible to write automation that the kernel will execute, rather than writing untrusted automation outside the kernel that generates proof terms.

[Simon Cruanes]

@suhr in HOL, proof terms are distinct from the terms of the logic, and they live in the meta language (they're typically in some sort of ML-family language). You could just write proofs by hand this way, it gets unwieldy very quickly so people write tactics and automation around it. But the upside is that classical logic is easier to automate than intuitionistic logic, and there's a lot more research on classical ATPs. You can even see that in HOL light and Isabelle/HOL because they have such powerful automation.