Can the judgement (A true) be made into a proposition?

[Fernando Yamauti]

      Hi,

 

      First of all, let A be a proposition. Let me state the question from a philosophical point of view and then state it inside the theory. Given that Martin-Löf apparently considers (in "On the meaning of the logical constants and the justifications of the logical laws") ' (A true) provable' as a valid form of judgement, one would be tempted to say that '(A true) true' is indeed a valid form of judgement. Now, it only makes sense to say that one knows 'B true' whenever one already known 'B prop', that is B is a proposition. From this, one is inclined to believe that (A true) is indeed a proposition and, therefore, we know the conditions of verifiability of (A true).

     Given that proposition-as-types is true, there should, then, exist a type (A true) where a proof of (A true) would mean that there exists a proof of (A true). In other words, there should exist a type (A true) where a proof it is a proof that A is inhabited. Therefore I shall call (A true) by (A inhabited).

     1) Is there a type (A inhabited) inside the theory where a proof of it would mean that A --> 0 is not inhabited or, a priori stronger, that A \cong 0? 

     (By the way, additional question not related to this one, is it true that A ---> 0 \cong (A \cong 0) ?)

     2) If this is the case, is this type homotopy equivalent to A? In other words (A inhabited) \cong A is inhabited?

     Thanks in advance.

[Fernando Yamauti]

      Correction to 1), additional question 3) and the question in parenthesis now below 3) **Ignore the previous message**

          First of all, let A be a proposition. Let me state the question from a philosophical point of view and then state it inside the theory. Given that Martin-Löf apparently considers (in "On the meaning of the logical constants and the justifications of the logical laws") ' (A true) provable' as a valid form of judgement, one would be tempted to say that '(A true) true' is indeed a valid form of judgement. Now, it only makes sense to say that one knows 'B true' whenever one already known 'B prop', that is B is a proposition. From this, one is inclined to believe that (A true) is indeed a proposition and, therefore, we know the conditions of verifiability of (A true).

     Given that proposition-as-types is true, there should, then, exists a type (A true) where a proof of (A true) would mean that there exists a proof of (A true). In other words, there should exist a type (A true) where a proof it is a proof that A is inhabited. Therefore I shall call (A true) by (A inhabited).

         1) Is there a type (A inhabited) inside the theory where a proof of it would be a proof that there's a proof of A?    

         2) If this is the case, is this type homotopy equivalent to A? In other words (A inhabited) \cong A is inhabited?

         3) Motivated by the above question question, is there a type (A inhabited classically) where a proof of it would mean that A --> 0 is not inhabited or, a priori stronger, that A \cong 0 is not inhabited? 

         (By the way, additional question not related to this one, is it true that A ---> 0 \cong (A \cong 0) ?)

[Ben Sherman]

First of all, let A be a proposition. Let me state the question from a philosophical point of view and then state it inside the theory. Given that Martin-Löf apparently considers (in "On the meaning of the logical constants and the justifications of the logical laws") ' (A true) provable' as a valid form of judgement, one would be tempted to say that '(A true) true' is indeed a valid form of judgement. Now, it only makes sense to say that one knows 'B true' whenever one already known 'B prop', that is B is a proposition. From this, one is inclined to believe that (A true) is indeed a proposition and, therefore, we know the conditions of verifiability of (A true).

For whatever it's worth, I interpret this differently. I take `A prop` to essentially mean that the typing judgment `A : U` holds, where `U` is the universe of types, whereas `A true` means that the typing judgment `a : A` holds for some term `a` (which we've decided not to mention explicitly). One cannot internally state the conditions under which there is some such term without describing type theory internally within type theory.

 1) Is there a type (A inhabited) inside the theory where a proof of it would be a proof that there's a proof of A?    

Surely this is not the answer you're looking for, but perhaps it can help refine your question: The obvious answer seems to be to define `A inhabited` as simply the type `A`. Then yes, a proof of `A` implies that there's a proof of `A` (i.e., A -> A)

2) If this is the case, is this type homotopy equivalent to A? In other words (A inhabited) \cong A is inhabited?

With my perhaps disingenuous answer to (1), these types are indeed equivalent.

3) Motivated by the above question question, is there a type (A inhabited classically) where a proof of it would mean that A --> 0 is not inhabited or, a priori stronger, that A \cong 0 is not inhabited? 

The way one normally expresses this is with the double-negation translation, which is a method of expressing classical logic within an intuitionistic system. Assuming consistency of the logical system, then we can translate "A --> 0 is not inhabited" to `(A -> 0) -> 0`, which is the double negation of A.

Note that it is a theorem that `A -> 0` if and only if `A \cong 0`.

 (By the way, additional question not related to this one, is it true that A ---> 0 \cong (A \cong 0) ?)

Yes, this is true. By the above argument, this is equivalent to `A -> ((A \cong 0) -> 0)`, and using that principle again, this is equivalent to `A -> ((A -> 0) -> 0)`, that is, that any proposition implies its double negation, which is true.

I'll do my best to point you in directions you may be interested in. One would be the study of several variations of "weaker notions of truth" than the intuitionistic one. You have pointed out that one such notion is `not (not P)` as a weak notion of truth of `P`. In intuitionistic logic, this is indeed weaker (there are models which separate the two). With HoTT, there is another notion, propositional truncation (see section 3.7 of the HoTT book), written `||P||` which in general lies strictly in between, i.e.,

P    ->   || P ||   ->    not (not P)

but there are choices of P and models of type theory such that the reverse implications do not hold. You may be interested in this paper, which examines these notions (and some other ones) in detail:

http://www.cs.nott.ac.uk/~psztxa/publ/jhedberg.pdf

On another note, you may be interested in this paper

https://people.csail.mit.edu/jgross/personal-website/papers/2016-lob-icfp-2016-draft.pdf

whose abstract has as its first sentence "Löb’s theorem states that to prove that a proposition is provable, it is sufficient to prove the proposition under the assumption that it is provable".

[Fernando Yamauti]

  Hi Ben,

  Thanks for your references. I've realized that my question is kind of dumb. At first, I thought that it would be impossible to talk about the theory from inside the theory itself since this leads to circularity and some philosophical problems, however apparently \sum_{x : A} A would be an answer to 1) and it's homotopy equivalent to A (at least in categorical semantics, it's actually A itself), so there's a positive answer to 2). And, then \not \sum_{x: A} A would be an answer to 3). This is not what I really wanted anyway.

  If it matters, what I really want is to talk about derivability of judgements from inside the theory itself (as in Löb's theorem that you mentioned) and see how this relates to Gödel incompleteness theorem (given that truth equates to provability in constructive matematics). However, unfortunately, all the answers seems to be only trivial and unsatisfactory.

  

  Regards,

  Fernando Yamauti

[Fernando Yamauti]

Whoops! Correction \not \not \sum_{x : A} A.

[Fernando Yamauti]

 Whoops!Another correction \sum_{x: A} A is obviously not homotopy equivalent to A in general, which is kind of weird from proposition-as-types.

[Ben Sherman]

You may be interested in:

https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/

https://jmchapman.github.io/papers/lfmtp08_jmc.pdf

http://www.cse.chalmers.se/~peterd/papers/InductionRecursionInitialAlgebras.pdf

It's a nice exercise to write an interpreter of STLC (or similar theories) in Coq or Agda (see, for instance, "A lambda calculus interpreter" in http://adam.chlipala.net/cpdt/html/Cpdt.DataStruct.html). Having an interpreter is very strong, and implies, for instance, consistency of STLC. Then one can very easily prove, for instance, that there is no closed (syntactic) term of (syntactic) type "False" within the STLC, because you can interpret this term to produce a term of type False in the Agda/Coq theory (metatheory).

[Andrej Bauer]

Perhaps you meant ∑(x:A) True instead of ∑(x:A) A ?

> --
> You received this message because you are subscribed to the Google Groups
> "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Fernando Yamauti]

   Thank you, Ben1 Unfortunately, my lack of proficiency with programming makes it harder to digest the language in which most of the references you mentioned is written. I'm ok with higher category and sequent calculus though. 

[Fernando Yamauti]

2017-04-13 4:04 GMT-03:00 Andrej Bauer <andrej...@andrej.com>:

Perhaps you meant ∑(x:A) True instead of ∑(x:A) A ?

    Sure. I have corrected it later in my sixth message. I was sleep deprived when I wrote that.

[Fernando Yamauti]

     For sake of completeness, let me explain the source of my question with more details. In Intuitionistic Type Theory , ML himself mentions in page 7:

     " Thus, intuitionistically, truth is identified with provability, though of course not (because of Gödel’s incompleteness theorem) with derivability within any particular formal system. "

      An equivalent formulation of the above is by Tarski undefinability of truth, which, in this case, implies that there are proofs (programs) that are not derivations in a formal system if type theory is consistent. But since type theory can talk about itself through universes, these derivations and proofs seems to coincide. Or maybe its just that these proofs are not really proofs that terminate in finite time, that is they are undecidable. I'm not sure. 

[Matt Oliveri]

Something that's potentially confusing about Martin-Löf's usage of terminology is precisely what he's saying in that quote. That by "provability", he does not mean provability in any formal system. As he says, you cannot consistently identify formal provability with truth. As you point out, that's precisely what Tarski's undefinability of truth tells us. So you have to watch out when followers of Matin-Löf talk about "proofs". A more modern term for this semantic notion of proof is "witness". Another is "evidence". A formal type system gives us a formal way to judge that some witness is indeed evidence for some proposition. But such judgments do not start out as pure formalism.

I thought I'd emphasize the confusion since Ben Sherman brought up interpretation functions and quining and stuff, and this is the kind of working with formal proofs that Martin-Löf is *not* talking about. Maybe you already realized this.

I'm not sure what you're getting at about universes, but I do know that it's not the same as working with formal derivations. There is no need for nontermination if you don't want it, since universes don't violate undefinability of truth. (Even if universes *were* about formally-definable stuff, it'd be definability in a strictly weaker system, so you'd still actually be OK.)

[Fernando Yamauti]

    Thanks for your remarks, Matt.

2017-04-13 22:34 GMT-03:00 Matt Oliveri <atm...@gmail.com>:

Something that's potentially confusing about Martin-Löf's usage of terminology is precisely what he's saying in that quote. That by "provability", he does not mean provability in any formal system. As he says, you cannot consistently identify formal provability with truth. As you point out, that's precisely what Tarski's undefinability of truth tells us. So you have to watch out when followers of Matin-Löf talk about "proofs". A more modern term for this semantic notion of proof is "witness". Another is "evidence". A formal type system gives us a formal way to judge that some witness is indeed evidence for some proposition. But such judgments do not start out as pure formalism.

     Indeed I'm aware of this difference in terminology. First of all, "evidence" is what makes a judgement true, so its not something about propositions, so I believe this is not a good terminology according to ML tradition. Now, you mention that a proof is not a derivation but only a "witness". I'm not aware of rigorous definition of "witness" without an intended computational interpretation. In this case a witness is a program, which can for instance refer to itself and never halt in finite time. Maybe you have a more absolute definition of witness or maybe my intended interpretation of witness (in computation) is not correct? 

 

I'm not sure what you're getting at about universes, but I do know that it's not the same as working with formal derivations. There is no need for nontermination if you don't want it, since universes don't violate undefinability of truth. (Even if universes *were* about formally-definable stuff, it'd be definability in a strictly weaker system, so you'd still actually be OK.)

     What I had in mind is that, if type theory can be encoded inside type theory, it should be able to talk about truth from the outside and about derivations from the inside (the internal type theory), but, as you said, it's in a strictly weaker system that truth would be defined, so there's no problem at all (it's like in any extension of interpretations or models). I was being silly.

[Matt Oliveri]

On Thursday, April 13, 2017 at 10:12:56 PM UTC-4, Fernando Yamauti wrote:

    Thanks for your remarks, Matt.

2017-04-13 22:34 GMT-03:00 Matt Oliveri <atm...@gmail.com>:

Something that's potentially confusing about Martin-Löf's usage of terminology is precisely what he's saying in that quote. That by "provability", he does not mean provability in any formal system. As he says, you cannot consistently identify formal provability with truth. As you point out, that's precisely what Tarski's undefinability of truth tells us. So you have to watch out when followers of Matin-Löf talk about "proofs". A more modern term for this semantic notion of proof is "witness". Another is "evidence". A formal type system gives us a formal way to judge that some witness is indeed evidence for some proposition. But such judgments do not start out as pure formalism.

     Indeed I'm aware of this difference in terminology. First of all, "evidence" is what makes a judgement true, so its not something about propositions, so I believe this is not a good terminology according to ML tradition. Now, you mention that a proof is not a derivation but only a "witness". I'm not aware of rigorous definition of "witness" without an intended computational interpretation. In this case a witness is a program, which can for instance refer to itself and never halt in finite time. Maybe you have a more absolute definition of witness or maybe my intended interpretation of witness (in computation) is not correct?

Oh hmm. I forgot Martin-Löf used the term "evidence". Never mind that then. I was thinking of how Robert Constable, from the Nuprl group, uses "evidence".

My understanding was that a "witness" for the truth of a type A is simply an element of A. It doesn't presume any particular interpretation, like computations. The additional terminology is just to suggest that a type is currently being thought of as a proposition. Maybe I misunderstood.

[Bruno Bentzen]

Hi Fernando,

Here is my two cents:

If it matters, what I really want is to talk about derivability of judgements from inside the theory itself (as in Löb's theorem that you mentioned) and see how this relates to Gödel incompleteness theorem (given that truth equates to provability in constructive matematics). However, unfortunately, all the answers seems to be only trivial and unsatisfactory.

  

We know that the relation of provability in a formal system can be encoded (via Gödel’s numbering technique) into a relation P : ℕ × ℕ → U on the natural numbers such that the judgment ‘P(n,m) true’ is evident iff n is the Gödel number of a formal proof of ‘A is true’ and m = G(A) is the Gödel number of A. So we can internally express the derivability of ‘A is true’ through the type ∑ (n : ℕ) P(n,m) – which basically express the existence a formal proof of ‘A is true’.

Is your question something along the lines of: for all judgments of the form ‘A is true’ in MLTT, is it the case that the types ∑ (n : ℕ) P(n,m) and A are equivalent (in the sense of the HoTT book)?

If this is the question you had in mind, then it is my understanding (and please correct me if I am wrong) that the answer is negative. For a counterexample, we just need to observe that A:=Unit is a mere proposition whereas ∑ (n : ℕ) P(n,m) does not have to be.

Best,

Bruno

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Fernando Yamauti]

     Hi Bruno,

Is your question something along the lines of: for all judgments of the form ‘A is true’ in MLTT, is it the case that the types ∑ (n : ℕ) P(n,m) and A are equivalent (in the sense of the HoTT book)?

    Yes! That's what I was looking for. Thank you!

 

If this is the question you had in mind, then it is my understanding (and please correct me if I am wrong) that the answer is negative. For a counterexample, we just need to observe that A:=Unit is a mere proposition whereas ∑ (n : ℕ) P(n,m) does not have to be.

     Do you mean A is point? In this case, I'm not sure if  ∑ (n : ℕ) P(n,m) wouldn't be a mere proposition again. Shouldn't it be the case that every derivation of 'A is true' is given by a term of A (of course, reciprocal assertion is not true)? In this case,  ∑ (n : ℕ) P(n,m)  would be a point, such that this point is located above the fiber over the Gödel code of the unique term of A. 

     A contractible A with more terms than derivations would do the trick since ∑ (n : ℕ) P(n,m) would be a bunch of points over a discrete space. However I don't know how to construct it nor if it exists. 

    In any case, this makes me think whether its the case that homotopy equivalence preserves truth since we can't identify which terms are derivations. Actually it's not clear even if an isomorphism preserves truth. 

    Regards,

    Fernando

[Matt Oliveri]

On Saturday, April 15, 2017 at 10:41:52 AM UTC-4, Fernando Yamauti wrote:

     Hi Bruno,

...

 

If this is the question you had in mind, then it is my understanding (and please correct me if I am wrong) that the answer is negative. For a counterexample, we just need to observe that A:=Unit is a mere proposition whereas ∑ (n : ℕ) P(n,m) does not have to be.

     Do you mean A is point? In this case, I'm not sure if  ∑ (n : ℕ) P(n,m) wouldn't be a mere proposition again. Shouldn't it be the case that every derivation of 'A is true' is given by a term of A (of course, reciprocal assertion is not true)? In this case,  ∑ (n : ℕ) P(n,m)  would be a point, such that this point is located above the fiber over the Gödel code of the unique term of A.

Essentially yes, in the case of intensional type theory. But these are terms up to syntactic equality, not definitional equality. So, for example, "()" and "(fun x=>x) ()" correspond to different formal proofs of Unit.

     A contractible A with more terms than derivations would do the trick since ∑ (n : ℕ) P(n,m) would be a bunch of points over a discrete space. However I don't know how to construct it nor if it exists.

I guess you meant more derivations than elements? Anyway, we can see this already with Unit.

    In any case, this makes me think whether its the case that homotopy equivalence preserves truth since we can't identify which terms are derivations. Actually it's not clear even if an isomorphism preserves truth.

But the sigma of formal derivations of a type is generally not homotopy equivalent to the actual type. In addition to the Unit example, where there are more derivations, we also have that the sigma of derivations is always an hSet, but not all types are hSets. Yet another example is "nat -> nat": the metalanguage will be able to witness more functions than the object language can derive, because it must be logically stronger. (If it isn't, you still don't get an equivalence, but this time because of undefinability of truth.)

It sure seems to me that equivalence preserves truth, pretty much by definition.

[Bruno Bentzen]

Hi Fernando,

Do you mean A is point? In this case, I'm not sure if  ∑ (n : ℕ) P(n,m) wouldn't be a mere proposition again. [...]

The type ∑ (n : ℕ) P(n,m) where m:= G(Unit) is not a mere proposition since, as Matt seemed to suggest, the derivations that are being represented here by their Gödel numbers are identified up to syntactic equality. To give an illustration, consider both the following “redundant” derivation of ‘⋆ : Unit’

--- UNIT-INTRO     --- UNIT-INTRO

⋆ : Unit                 ⋆ : Unit

---------------------------------------- PROD-INTRO

       (⋆,⋆) : Unit × Unit

---------------------------------------- PROD-ELIM1

       pr1(⋆,⋆) ≡ ⋆ : Unit

and the one-line UNIT-INTRO derivation of ‘⋆ : Unit’: they are both syntactically distinct derivations of the same judgment.

You are right in some sense, though: we can refuse to adopt this obvious syntactic identity criterion if we want and, for example, declare that two derivations are equal just in case they have the same normal form. However, note that, strictly speaking, we would not be characterizing the “type of derivations of the judgment ‘A true’” anymore but only the “type of derivations of the judgment ‘A true’ up to sameness of their normal form”.

In any case, under this second view:

1. We apparently get only one derivation of ‘a : A’ per term a of A in the intensional flavor of MLTT (although I would love to be proven wrong). If this is correct and, provided that P(n,m) is always a mere proposition for all n, m : ℕ, this means that indeed A ≅ ∑ (n : ℕ) P(n,m).

2. In general, we may get more than one derivation of ‘a : A’ per term a of A in the extensional version of MLTT. One way to see why this is true is the following. Recall that the rule x : Empty ⊢ J is provable in the extensional theory for any judgment J. As a result, we may have at least two different derivations of (say) the judgment ‘λx.⋆ : Empty → Unit’, namely, one using UNIT-INTRO and →-INTRO and the other one using →-INTRO and the above-mentioned rule for J := '⋆ : Unit'.

[...] Shouldn't it be the case that every derivation of 'A is true' is given by a term of A (of course, reciprocal assertion is not true)? 

Yes, but observe that the judgment ‘a : A’ of any given type theory – for any term a and type A of the language – need not, in principle, have only one possible derivation (provided it is indeed derivable), even up to sameness of normal form. Whenever a judgment such as ‘a : A’ has more than one derivation, it means that A and the Gödel number of ‘A true’ are not equivalent as types.

Best,

Bruno

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Fernando Yamauti]

  Matt, thanks for your remarks.

Essentially yes, in the case of intensional type theory. But these are terms up to syntactic equality, not definitional equality. So, for example, "()" and "(fun x=>x) ()" correspond to different formal proofs of Unit.

    Whoops! I forgot that the equality in derivations (when encoding proofs by Gödel codes) is not the definitional one. You're right. 

 

     A contractible A with more terms than derivations would do the trick since ∑ (n : ℕ) P(n,m) would be a bunch of points over a discrete space. However I don't know how to construct it nor if it exists.

I guess you meant more derivations than elements? Anyway, we can see this already with Unit.

     Hmmm...It seems that we are interpreting the meaning of witness in a different way. Let me try to clarify this point. Please, take a look at this answer by Bob Harper . You're considering the syntactic proposition-as-types and not the semantic one right? (By the way, does the the semantic version fail to interpret MLITT? Why?) 

     Let me ask another question. By your interpretation it's not true that

         A true

-----------------------  the rule holds, right? 

       exists a: A 

    In other words, a witness is a program that fulfills a task (in finite time, of course) or a formal proof (derivation) of a proposition? Notice that the second option does not contradicts Tarski theorem if one doesn't assume that inhabited means true. That is we can choose the second option and approximate the notion of truth by provability.

 

    In any case, this makes me think whether its the case that homotopy equivalence preserves truth since we can't identify which terms are derivations. Actually it's not clear even if an isomorphism preserves truth.

But the sigma of formal derivations of a type is generally not homotopy equivalent to the actual type. In addition to the Unit example, where there are more derivations, we also have that the sigma of derivations is always an hSet, but not all types are hSets. Yet another example is "nat -> nat": the metalanguage will be able to witness more functions than the object language can derive, because it must be logically stronger. (If it isn't, you still don't get an equivalence, but this time because of undefinability of truth.)

It sure seems to me that equivalence preserves truth, pretty much by definition.

      I can only make sense of your assertion that "it's clear by definition" if we agree about the definition of witness as I mentioned above.

[Fernando Yamauti]

 Hi Bruno,

  Thanks for your remarks.

In any case, under this second view:

1. We apparently get only one derivation of ‘a : A’ per term a of A in the intensional flavor of MLTT (although I would love to be proven wrong). If this is correct and, provided that P(n,m) is always a mere proposition for all n, m : ℕ, this means that indeed A ≅ ∑ (n : ℕ) P(n,m).

2. In general, we may get more than one derivation of ‘a : A’ per term a of A in the extensional version of MLTT. One way to see why this is true is the following. Recall that the rule x : Empty ⊢ J is provable in the extensional theory for any judgment J. As a result, we may have at least two different derivations of (say) the judgment ‘λx.⋆ : Empty → Unit’, namely, one using UNIT-INTRO and →-INTRO and the other one using →-INTRO and the above-mentioned rule for J := '⋆ : Unit'.

      Could you clarify why 2 is only true for the extensional case? Ex falso quodlibet holds for MLITT.

[Bruno Bentzen]

Hi Fernando,

Could you clarify why 2 is only true for the extensional case? Ex falso quodlibet holds for MLITT.

I am assuming that by EFQ you mean the usual induction principle of the empty type

    ind_empty : ∏ (C : Empty → U) ∏ (x : Empty) C(x) 

which is in clear contrast with the aforementioned rule, which states that

      x : Empty

    -----------------

          J 

for any judgment J.

Roughly speaking, both are “representations” of EFQ, but the latter is (say) a “judgmental” explosion principle: it allows us, for example, to derive things such as p : Id_ℕ (0,1) ⊢ 3 : ℕ → ℕ in the extensional version of MLTT.

Best,

Bruno

--

Bruno Bentzen

https://sites.google.com/site/bbentzena/

[Matt Oliveri]

Sorry about the delay in replying.

On Monday, April 17, 2017 at 2:48:45 AM UTC-4, Fernando Yamauti wrote:

     A contractible A with more terms than derivations would do the trick since ∑ (n : ℕ) P(n,m) would be a bunch of points over a discrete space. However I don't know how to construct it nor if it exists.

I guess you meant more derivations than elements? Anyway, we can see this already with Unit.

     Hmmm...It seems that we are interpreting the meaning of witness in a different way. Let me try to clarify this point. Please, take a look at this answer by Bob Harper . You're considering the syntactic proposition-as-types and not the semantic one right? (By the way, does the the semantic version fail to interpret MLITT? Why?)

I don't see how that distinction is relevant to what I was saying. There should be only one element of Unit in any interpretation. More specifically, equality is interpreted in such a way that internally, there's one element. And the "derivations" are always formal derivations. I didn't think there was any ambiguity in that term.

But maybe I misunderstood what you were originally saying, so that my reply, as I meant it, wasn't appropriate.

Anyway, I have indeed been thinking in terms of syntactic props-as-types for our conversation. I assumed that that was the right choice, since that's what Martin-Löf ended up favoring, as I understand it. (I actually prefer semantic props-as-types. I'm a big fan of Nuprl's Computational Type Theory.) Personally, I prefer to just think of syntactic props-as-types as "use proof terms", and semantic props-as-types as "use realizability". They need not be philosophical commitments, and they need not be mutually exclusive.

     Let me ask another question. By your interpretation it's not true that

         A true

-----------------------  the rule holds, right? 

       exists a: A 

    In other words, a witness is a program that fulfills a task (in finite time, of course) or a formal proof (derivation) of a proposition? Notice that the second option does not contradicts Tarski theorem if one doesn't assume that inhabited means true. That is we can choose the second option and approximate the notion of truth by provability.

I don't understand the question. First, my "interpretation"? Do you mean my informal interpretation of some English word we've been using, or an interpretation of type theory? (And which theory, in the latter case?) Second, both "A true" and "exists a : A" are not basic judgments in the type theories I'm familiar with. So whether that rule "holds" (true? valid? admissible?) depends on how the judgments are defined, which I could only guess at. Maybe you're trying to ask about my intuitive idea of these judgments' meaning. But I'm afraid I don't actually think along those lines at all. For me, type theory is a tool, not a philosophy.
 

    In any case, this makes me think whether its the case that homotopy equivalence preserves truth since we can't identify which terms are derivations. Actually it's not clear even if an isomorphism preserves truth.

But the sigma of formal derivations of a type is generally not homotopy equivalent to the actual type. In addition to the Unit example, where there are more derivations, we also have that the sigma of derivations is always an hSet, but not all types are hSets. Yet another example is "nat -> nat": the metalanguage will be able to witness more functions than the object language can derive, because it must be logically stronger. (If it isn't, you still don't get an equivalence, but this time because of undefinability of truth.)

It sure seems to me that equivalence preserves truth, pretty much by definition.

      I can only make sense of your assertion that "it's clear by definition" if we agree about the definition of witness as I mentioned above.

To be more precise, equivalence of types A and B, as defined in HoTT, provides (among other things) a pair of functions (A->B) and (B->A). By any props-as-types I know of, this means that each implies the other.

[Matt Oliveri]

On Monday, April 17, 2017 at 2:48:45 AM UTC-4, Fernando Yamauti wrote:

(By the way, does the the semantic version fail to interpret MLITT? Why?)

You can interpret ITT with realizability, no problem. Ignoring type annotations (which is the right thing to do for realizability, since they have no computational content), ITT is a fragment of ETT, which is in turn a fragment of Computational Type Theory (CTT). At least for predicative versions of ITT and ETT. (But conjecturally for some appropriate impredicative version of CTT too.) What the "purer" versions of type theory buy you is a greater variety of interpretations. (And maybe some sort of philosophical peace of mind. I dunno.)