Two questions about SMT-LIB 3 format from a knowledgeable colleague who does not use email

[Martin Suda]

1. Can types be empty in SMT3? It's hard to have dependent types

without allowing for empty types, though not impossible. Mizar does

it, but it's a very different kind of type system than CIC.

2. Is it extensional wrt types? EG, if v has type Vector (n + m) where n,m : Int, then

   does it also have type Vector (m + n)? CIC does not have this property, and including

   it makes type checking as hard as theorem proving.

Here are a few references everyone probably knows, but just in case:

Benjamin Werner and Peter Aczel showed how to interpret a "classical

CIC like type theory" in classical set theory (and vice versa):

Benjamin Werner. Sets in Types, Types in Sets. TACS 97.

Peter Aczel. On Relating Type Theories and Set Theories. TYPES 1998.

There's also relevant later work, e.g.:

Bruno Barras. Sets in Coq, Coq in Sets. JFR 3. 2010.

Gyesik Lee and Benjamin Werner. Proof-irrelevant model of {CC} with

predicative induction and judgmental equality. LMCS 4. 2011.

With respect to proofs, if SMT3 is really a fragment of CIC, then the

quickest way to get a preexisting notion of proof is simply to

translate the formula into a Coq/Lean type and then say the proof is

something of that type (allowing the use of classical, extensional and

choice axioms in the proof term). This won't work if types are meant

to be extensional (Question 2 above), but in that case one could still

translate to an underlying set theory (via Werner and Aczel's ideas)

and say a proof is a proof in the set theory.

[Cody Roux]

This is a question I was meaning to ask as well!

I'm pretty sure that the "usual" interpretation of fresh types in SMT is non-empty, which may make things a bit finicky.

In Lean and Coq, there is often use of a type-class "inhabited" which is defined by

Class inhabited A := { elt : A }

Then every declaration, say of a polymorphic function like nil : forall A, list A, could be guarded by this type class: nil : forall A { _ : inhabited A}, list A.

However this does create a proof obligation when defining things like inductive families.

Concerning extensionality, I don't think this comes up much in the absence of type families like Vect, which I suspect is not really high on the radar of what SMT-LIb 3 is trying to accomplish. I think it's more about having a higher-order polymorphic predicate logic with proof terms. This suggests to me that types should be extensional, and in general, not a lot of computation is expected to occur in the type checking process beyond beta and delta reductions.

Indeed, further restrictions may even be necessary if type checking is to be efficient.

Is there a reference for Mizar's model of non-empty types?

Best,

Cody