# Wording and interpretation: propositions, predicates and types

**URL:** <https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407>\
**Category:** Google Group\
**Created:** [December 10, 2015, 10:16pm UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407 "2015-12-10T22:16:07Z")\
**Posts on this page:** 15\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 10, 2015, 10:16pm UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/1 "2015-12-10T22:16:07Z")

</div>

ATS has predicates which looks like the usual predicates; and has what it  
names propositions, which seems not the same as usual propositions and are  
more proofs.

So far, is that OK to say ATS proposition are not propositions after the  
usual meaning?  
[http://ece.uprm.edu/~jseguel/ltoc2.pdf](http://ece.uprm.edu/~jseguel/ltoc2.pdf)  
[https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic](https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic)  
At least, these two pages say, it there are variables and/or quantifiers,  
then this is not a proposition, that’s a predicate.

Moreover ATS propositions are never false, they are always true, or can’t  
exist at all, which is not a surprise, as ATS propositions are proof in the  
form of definitions, with `absprop` or in the form of inductive definitions  
with `dataprop` (which is not exactly the same as an axiomatic proof, an  
inductive definition is a safer assertion).

Unlike a boolean expression or a predicate which may evaluates to either  
`true` or `false`, a proof may only evaluates into a kind of `true` or not  
at all, which may be understood this other way: there is no false of type  
`prop`, the evaluation of a proof either “returns” a kind of true or fails  
(by the way, is it OK to say Prolog clauses evaluation are proofs?… as too,  
it never returns a real `false` neither, just fails).

stacst True: prop // Makes sense, OK?  
stacst False: prop // Does not make sens, isn’t it?

An `absprop` and/or a `dataprop`, introduce a function-like thing returning  
something of sort `prop`. May be it’s a function just because there may be  
variable in the proven statement.

absprop F(int) // int -\> prop  
stadef g: prop = F 0 // Check it’s indeed int -\> prop

Side note: I don’t understand why I can’s write `absprop F int` and the  
parentheses are required.

Type definition may be based on predicates, but not proof (or at least, not  
directly):

absprop F(int) // int -\> prop  
// typedef t = [i: int; F i] int(i) **ILLEGAL**

There are multiple ways of understanding things. One of these way, is to  
come to a thing with prior expectations about how things should be. That  
may be nice, but may not help when trying to understand something which  
does not match at all or not exactly these prior ideas. May be that’s why  
I’m progressing so slowly in understanding ATS enough to be at ease with it.

One of my prior expectations when I accosted ATS lands, was the relation  
between a type and a proof (also between a type and a function). But in  
ATS, a function may function returns a proof of some proposition along to a  
value of a type, both distinct (the proof is not part of the type of the  
value returned).

I wanted to try to relate both. Based on the above, I first came to this:

stadef h: prop -\> bool = (lam p =\> true) // Assume a prop is a proof

Assuming a proof, either is true or does not exist (because it failed), and  
also assuming a `prop` is a proof, then the above should be sound. Is it?

typedef t = [i: int; h(F i)] int(i) // Does it mean what I think it means?

If it really means what I think, then I may have progressed a bit in  
matching ATS and my mind.

At least, this simple declaration is not rejected:

val a: t = 0

(posting… hope I have not left too much typo errors)

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 11, 2015, 4:13am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/2 "2015-12-11T04:13:58Z")

</div>

> Yes, the dataprop definition for FACT only tells you what can be  
> proven; it does not say anything about what cannot be proven. On the  
> other hand, the relation ‘fact’ corresponding to ‘FACT’ is a set, and we  
> know that either (0, 0) is in ‘fact’ or it is not in ‘fact’.

If I understand correctly, this may be all of what we know, because we may  
don’t know how to compute it: we know it’s either true or false, we know  
when it’s true as FACT says how to compute it, and may not know when it’s  
false, as FACT does not say how to compute it.

Another related wording question. Here is something I just wrote in my  
notes (which I hope a future day may become a kind of book):

dataprop P(int) =  
| Q(0) of () // Asserts Q(0) from ()  
| Q(0) // Asserts Q(0) from nothing (same as above)  
| R(1) of P(0) // Asserts R(1), that is P(1) from P(0)  
| {i:int; i == 1} R(i) of P(0) // Same, with explicit constraint  
| {i:int; i == 1} R(i) of [j: int; j == 0] P(j) // Even more.

This holds:

- `P: int -> prop`
- `Q: unit -> prop`
- `R: prop -> prop`

More precisely:

- `Q: unit -> P(0):prop`
- `R: P(0):prop -> P(1):prop`

I have two other wording questions.

About the argument `R` gets, what would be the proper expression to qualify  
it: a subset, a subtype or a constrained type or any of the three?

About `Q` and `R`, how to name it: is “proof of P” the only expression or  
is “clause” appropriate too?

Also, as the argument to `R` is both of type `prop` (type, at the static  
level) and can only get something returned by `P`, then `P` is both a  
function and a type. Is it OK to say it this way? (if that’s OK, I will  
underline and put a stress on it… I like the idea of functions implying  
types)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 11, 2015, 5:10am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/3 "2015-12-11T05:10:01Z")

</div>

P: int → prop

So P is called a prop constructor (for construction props). P is usually not  
called a function. P itself is not a prop; P(i) is a prop if i is of the  
sort int.

Note that prop should not be confused with concepts like proposition,  
predicates, etc.  
To me, prop may be thought of as the collection of formulas that are  
assigned boolean  
values in models.

Q: () → P(0) // this is very different from writing: unit → prop

Q is not a prop; the type of Q is a prop. Often Q is called a proof  
constructor  
(as it is used to construct proofs).

R: P(0) → P(1) // again, this is very different from prop → prop

R is also a proof constructor; the argument of R is often called a proof.On Thursday, December 10, 2015 at 11:13:58 PM UTC-5, Yannick Duchêne wrote:

> Le vendredi 11 décembre 2015 04:33:18 UTC+1, gmhwxi a écrit :
> 
> > Yes, the dataprop definition for FACT only tells you what can be  
> > proven; it does not say anything about what cannot be proven. On the  
> > other hand, the relation ‘fact’ corresponding to ‘FACT’ is a set, and we  
> > know that either (0, 0) is in ‘fact’ or it is not in ‘fact’.
> 
> If I understand correctly, this may be all of what we know, because we may  
> don’t know how to compute it: we know it’s either true or false, we know  
> when it’s true as FACT says how to compute it, and may not know when it’s  
> false, as FACT does not say how to compute it.
> 
> Another related wording question. Here is something I just wrote in my  
> notes (which I hope a future day may become a kind of book):
> 
> ##### 
> 
> dataprop P(int) =  
> | Q(0) of () // Asserts Q(0) from ()  
> | Q(0) // Asserts Q(0) from nothing (same as above)  
> | R(1) of P(0) // Asserts R(1), that is P(1) from P(0)  
> | {i:int; i == 1} R(i) of P(0) // Same, with explicit constraint  
> | {i:int; i == 1} R(i) of [j: int; j == 0] P(j) // Even more.
> 
> This holds:
> 
> - `P: int -> prop`
> - `Q: unit -> prop`
> - `R: prop -> prop`
> 
> More precisely:
> 
> - `Q: unit -> P(0):prop`
> - `R: P(0):prop -> P(1):prop`
> 
> I have two other wording questions.
> 
> About the argument `R` gets, what would be the proper expression to  
> qualify it: a subset, a subtype or a constrained type or any of the three?
> 
> About `Q` and `R`, how to name it: is “proof of P” the only expression or  
> is “clause” appropriate too?
> 
> Also, as the argument to `R` is both of type `prop` (type, at the static  
> level) and can only get something returned by `P`, then `P` is both a  
> function and a type. Is it OK to say it this way? (if that’s OK, I will  
> underline and put a stress on it… I like the idea of functions implying  
> types)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 11, 2015, 2:35am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/4 "2015-12-11T02:35:44Z")

</div>

Hope this can shed a bit light.

Let me use an example to explain the relation and difference  
between the impredicative sort ‘prop’ and the predicative sort  
‘bool’.

dataprop  
FACT(int, int) =  
| FACTbas(0, 1)  
| {n:pos}{r1:int}  
FACTind(n, n\*r1) of FACT(n-1, r1)

The above dataprop essentially introduces the following constants:

FACT: (int, int) → prop

FACTbas: () → FACT(0, 1)

FACTind:  
{n:pos}{r1:int} FACT(n-1, r1) → FACT(n, n\*r1)

There exists a constant ‘fact’ corresponding to ‘FACT’:

fact: (int, int) → bool

and the following first-order formulas are true:

(1)  
fact(0, 1) = true

(2)  
{n:pos}{r1:int}  
fact(n-1, r1)=true implies fact(n, n\*r1)=true

If there exists a closed value of the prop FACT(n, r), then  
fact(n, r)=true holds. Another way to put it, if FACT(n, r) is  
provable, then fact(n, r) is true.

Note that the existence of ‘fact’ is implied by the so-called  
fixed-pointed theorem. Usually, ‘fact’ is taken to be the least  
relation satisfying (1) and (2). So we know ‘fact(0, 0)=false’  
holds. However, the statement that there is no closed value of  
the prop FACT(0, 0) is not provable inside ATS (Godel’s incompleteness  
result).On Thursday, December 10, 2015 at 5:16:07 PM UTC-5, Yannick Duchêne wrote:

> ATS has predicates which looks like the usual predicates; and has what it  
> names propositions, which seems not the same as usual propositions and are  
> more proofs.
> 
> So far, is that OK to say ATS proposition are not propositions after the  
> usual meaning?  
> [http://ece.uprm.edu/~jseguel/ltoc2.pdf](http://ece.uprm.edu/~jseguel/ltoc2.pdf)
> 
> [https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic](https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic)  
> At least, these two pages say, it there are variables and/or quantifiers,  
> then this is not a proposition, that’s a predicate.
> 
> Moreover ATS propositions are never false, they are always true, or can’t  
> exist at all, which is not a surprise, as ATS propositions are proof in the  
> form of definitions, with `absprop` or in the form of inductive definitions  
> with `dataprop` (which is not exactly the same as an axiomatic proof, an  
> inductive definition is a safer assertion).
> 
> Unlike a boolean expression or a predicate which may evaluates to either  
> `true` or `false`, a proof may only evaluates into a kind of `true` or not  
> at all, which may be understood this other way: there is no false of type  
> `prop`, the evaluation of a proof either “returns” a kind of true or fails  
> (by the way, is it OK to say Prolog clauses evaluation are proofs?… as too,  
> it never returns a real `false` neither, just fails).
> 
> stacst True: prop // Makes sense, OK?  
> stacst False: prop // Does not make sens, isn’t it?
> 
> An `absprop` and/or a `dataprop`, introduce a function-like thing  
> returning something of sort `prop`. May be it’s a function just because  
> there may be variable in the proven statement.
> 
> absprop F(int) // int → prop  
> stadef g: prop = F 0 // Check it’s indeed int → prop
> 
> Side note: I don’t understand why I can’s write `absprop F int` and the  
> parentheses are required.
> 
> Type definition may be based on predicates, but not proof (or at least,  
> not directly):
> 
> absprop F(int) // int → prop  
> // typedef t = [i: int; F i] int(i) **ILLEGAL**
> 
> There are multiple ways of understanding things. One of these way, is to  
> come to a thing with prior expectations about how things should be. That  
> may be nice, but may not help when trying to understand something which  
> does not match at all or not exactly these prior ideas. May be that’s why  
> I’m progressing so slowly in understanding ATS enough to be at ease with it.
> 
> One of my prior expectations when I accosted ATS lands, was the relation  
> between a type and a proof (also between a type and a function). But in  
> ATS, a function may function returns a proof of some proposition along to a  
> value of a type, both distinct (the proof is not part of the type of the  
> value returned).
> 
> I wanted to try to relate both. Based on the above, I first came to this:
> 
> stadef h: prop → bool = (lam p =\> true) // Assume a prop is a proof
> 
> Assuming a proof, either is true or does not exist (because it failed),  
> and also assuming a `prop` is a proof, then the above should be sound. Is  
> it?
> 
> typedef t = [i: int; h(F i)] int(i) // Does it mean what I think it means?
> 
> If it really means what I think, then I may have progressed a bit in  
> matching ATS and my mind.
> 
> At least, this simple declaration is not rejected:
> 
> val a: t = 0
> 
> (posting… hope I have not left too much typo errors)

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 10, 2015, 11:06pm UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/5 "2015-12-10T23:06:53Z")

</div>

> Here is an encoding of propositional logic in ATS:
> 
> [http://www.cs.bu.edu/~hwxi/academic/courses/CS520/Fall15/code/lecture-09-21/prop-logic.dats](http://www.cs.bu.edu/~hwxi/academic/courses/CS520/Fall15/code/lecture-09-21/prop-logic.dats)
> 
> You can see clearly that ‘False’ is indeed encoded.

Already seen some long time ago, but not studied. I will study it and see  
if it help.

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 11, 2015, 3:33am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/6 "2015-12-11T03:33:18Z")

</div>

A closed value is just a value that contains no free variables.  
If you can prove something, then the proof you have must be a closed  
value (as no dangling hypotheses are allowed).

Yes, the dataprop definition for FACT only tells you what can be  
proven; it does not say anything about what cannot be proven. On the  
other hand, the relation ‘fact’ corresponding to ‘FACT’ is a set, and we  
know that either (0, 0) is in ‘fact’ or it is not in ‘fact’.On Thursday, December 10, 2015 at 5:16:07 PM UTC-5, Yannick Duchêne wrote:

> ATS has predicates which looks like the usual predicates; and has what it  
> names propositions, which seems not the same as usual propositions and are  
> more proofs.
> 
> So far, is that OK to say ATS proposition are not propositions after the  
> usual meaning?  
> [http://ece.uprm.edu/~jseguel/ltoc2.pdf](http://ece.uprm.edu/~jseguel/ltoc2.pdf)
> 
> [https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic](https://www.quora.com/What-is-the-precise-difference-between-propositional-and-predicate-logic)  
> At least, these two pages say, it there are variables and/or quantifiers,  
> then this is not a proposition, that’s a predicate.
> 
> Moreover ATS propositions are never false, they are always true, or can’t  
> exist at all, which is not a surprise, as ATS propositions are proof in the  
> form of definitions, with `absprop` or in the form of inductive definitions  
> with `dataprop` (which is not exactly the same as an axiomatic proof, an  
> inductive definition is a safer assertion).
> 
> Unlike a boolean expression or a predicate which may evaluates to either  
> `true` or `false`, a proof may only evaluates into a kind of `true` or not  
> at all, which may be understood this other way: there is no false of type  
> `prop`, the evaluation of a proof either “returns” a kind of true or fails  
> (by the way, is it OK to say Prolog clauses evaluation are proofs?… as too,  
> it never returns a real `false` neither, just fails).
> 
> stacst True: prop // Makes sense, OK?  
> stacst False: prop // Does not make sens, isn’t it?
> 
> An `absprop` and/or a `dataprop`, introduce a function-like thing  
> returning something of sort `prop`. May be it’s a function just because  
> there may be variable in the proven statement.
> 
> absprop F(int) // int → prop  
> stadef g: prop = F 0 // Check it’s indeed int → prop
> 
> Side note: I don’t understand why I can’s write `absprop F int` and the  
> parentheses are required.
> 
> Type definition may be based on predicates, but not proof (or at least,  
> not directly):
> 
> absprop F(int) // int → prop  
> // typedef t = [i: int; F i] int(i) **ILLEGAL**
> 
> There are multiple ways of understanding things. One of these way, is to  
> come to a thing with prior expectations about how things should be. That  
> may be nice, but may not help when trying to understand something which  
> does not match at all or not exactly these prior ideas. May be that’s why  
> I’m progressing so slowly in understanding ATS enough to be at ease with it.
> 
> One of my prior expectations when I accosted ATS lands, was the relation  
> between a type and a proof (also between a type and a function). But in  
> ATS, a function may function returns a proof of some proposition along to a  
> value of a type, both distinct (the proof is not part of the type of the  
> value returned).
> 
> I wanted to try to relate both. Based on the above, I first came to this:
> 
> stadef h: prop → bool = (lam p =\> true) // Assume a prop is a proof
> 
> Assuming a proof, either is true or does not exist (because it failed),  
> and also assuming a `prop` is a proof, then the above should be sound. Is  
> it?
> 
> typedef t = [i: int; h(F i)] int(i) // Does it mean what I think it means?
> 
> If it really means what I think, then I may have progressed a bit in  
> matching ATS and my mind.
> 
> At least, this simple declaration is not rejected:
> 
> val a: t = 0
> 
> (posting… hope I have not left too much typo errors)

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 11, 2015, 6:17am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/7 "2015-12-11T06:17:49Z")

</div>

> _A prop is like a type; a value classified by a prop is often called a  
> proof,_
> 
> _which is dynamic but erased by the compiler. So while proofs are dynamic,_  
> _there is no proof construction at run-time._

A funny thing about the dynamic aspect…

As said before:  
prval q:P(0) = Q

And this too! :  
val q:P(0) = Q

Just like one would write:  
val a:int = 0

Even more funny:  
prval a:int = 0

So a question comes: how much differently `prval` and `val` are handled? Is  
this only syntactic sugar or is there more?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 11, 2015, 6:26am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/8 "2015-12-11T06:26:05Z")

</div>

val … // not erased  
prval … // erased after type-checking

If you do

val q:P(0) = Q

Then the compiler should complain later as ‘Q’ is not available.

Try to compile the following code and see what happens:

prval a: int = 0  
val b = a + 1

The generated C code contains PMVerr(…), which should point  
you to the source of the error: no definition for ‘a’.On Fri, Dec 11, 2015 at 1:17 AM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Le vendredi 11 décembre 2015 06:56:38 UTC+1, gmhwxi a écrit :
> 
> > _A prop is like a type; a value classified by a prop is often called a  
> > proof,_
> > 
> > _which is dynamic but erased by the compiler. So while proofs are  
> > dynamic,_  
> > _there is no proof construction at run-time._
> 
> A funny thing about the dynamic aspect…
> 
> As said before:  
> prval q:P(0) = Q
> 
> And this too! :  
> val q:P(0) = Q
> 
> Just like one would write:  
> val a:int = 0
> 
> Even more funny:  
> prval a:int = 0
> 
> So a question comes: how much differently `prval` and `val` are handled?  
> Is this only syntactic sugar or is there more?
> 
> –  
> You received this message because you are subscribed to the Google Groups  
> “ats-lang-users” group.  
> To unsubscribe from this group and stop receiving emails from it, send an  
> email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/37f08799-c612-4dc6-a6e3-92c444e565f8%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/37f08799-c612-4dc6-a6e3-92c444e565f8%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/37f08799-c612-4dc6-a6e3-92c444e565f8%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/37f08799-c612-4dc6-a6e3-92c444e565f8%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 10, 2015, 11:13pm UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/9 "2015-12-10T23:13:43Z")

</div>

> Maybe you just need to be more creative in creating an inconsistent  
> set of axioms. 🙂
> 
> A disproof can be done with ‘case … =/=\>’ so I am not sure a ‘false  
> proposition’ can’t exist. I’ve used it for reductio ad absurdum.

To be back on that point, I was saying this can’t happen with the  
assertions generated by an inductive definition.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 11, 2015, 5:50am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/10 "2015-12-11T05:50:34Z")

</div>

> That makes sense, if P is not a prop constructor, not a prop.
> 
> Sorry, typo. I wanted to say “That makes sense, if P **is a prop**  
> constructor, not a prop.”

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 11, 2015, 3:20am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/11 "2015-12-11T03:20:38Z")

</div>

> Hope this can shed a bit light.
> 
> Let me use an example to explain the relation and difference  
> between **the impredicative sort ‘prop’ and the predicative sort  
> ‘bool’**.

Interesting to see this question came back here 🙂

> dataprop  
> FACT(int, int) =  
> | FACTbas(0, 1)  
> | {n:pos}{r1:int}  
> FACTind(n, n\*r1) of FACT(n-1, r1)
> 
> The above dataprop essentially introduces the following constants:
> 
> ###### 
> 
> FACT: (int, int) → prop
> 
> FACTbas: () → FACT(0, 1)
> 
> FACTind:  
> {n:pos}{r1:int} FACT(n-1, r1) → FACT(n, n\*r1)
> 
> ###### 
> 
> There exists a constant ‘fact’ corresponding to ‘FACT’:
> 
> fact: (int, int) → bool
> 
> and the following first-order formulas are true:
> 
> ###### 
> 
> (1)  
> fact(0, 1) = true
> 
> (2)  
> {n:pos}{r1:int}  
> fact(n-1, r1)=true implies fact(n, n\*r1)=true
> 
> ######

This looks like what I had in mind, and that’s why I though this was like  
it can only evaluates to a kind of true, or else fail, so no kind of  
`false`.

> If there exists a closed value of the prop FACT(n, r), then  
> fact(n, r)=true holds. Another way to put it, if FACT(n, r) is  
> provable, then fact(n, r) is true.

What is a closed value? Is it related to function closure?

> Note that the existence of ‘fact’ is implied by the so-called  
> fixed-pointed theorem. Usually, ‘fact’ is taken to be the least  
> relation satisfying (1) and (2). So we know ‘fact(0, 0)=false’  
> holds. However, the statement that there is no closed value of  
> the prop FACT(0, 0) is not provable inside ATS (Godel’s incompleteness  
> result).

I’m not a Godel theorem guru (just have an intuitive understanding of it),  
but I would say FACT does not assert there can’t be any FACT(0,0), it just  
assert what it states to be true, and says nothing about the rest. Is it OK  
to say that?

A bit out of topic while not too much and may be nice for some ones, I just  
checked proofs can be type-annotated to make them explicit about their  
“content”.

I checked this example:

> **[ATS Programming](https://fr.slideshare.net/mirrorren/ats-programming)**
>
> ATS Programming - Download as a PDF or view online for free

dataprop SUM(int, int) =  
| SUMBase(0, 0)  
| {x, y:int} SUMInd(x + 1, y + x + 1) of SUM(x, y)

fun sum {x:int; x \>= 0} (a: int x): [y:int] (SUM(x, y) | int y) =  
if a = 0 then (SUMBase | 0)  
else let  
val (pf1 | s) = sum(a - 1)  
prval pf2 = SUMInd pf1  
in (pf2 | s + a)  
end

Can be rewritten in this more explicit way:  
dataprop SUM(int, int) =  
| SUMBase(0, 0)  
| {x, y:int} SUMInd(x + 1, y + x + 1) of SUM(x, y)

fun sum {x:int; x \>= 0} (a: int x): [y:int] (SUM(x, y) | int y) =  
if a = 0 then (SUMBase:SUM(0, 0) | 0)  
else let  
val [y:int] (pf1:SUM(x - 1, y) | s:int y) = sum(a - 1)  
prval pf2:SUM(x, y + x) = SUMInd pf1  
in (pf2 | s + a)  
end

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 11, 2015, 5:56am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/12 "2015-12-11T05:56:38Z")

</div>

Yes, I think you have got it!

Just in case others read these messages, I would like to say this:

_A prop is like a type; a value classified by a prop is often called a  
proof,_

_which is dynamic but erased by the compiler. So while proofs are dynamic,_  
\*there is no proof construction at run-time.\*On Fri, Dec 11, 2015 at 12:48 AM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Le vendredi 11 décembre 2015 06:10:01 UTC+1, gmhwxi a écrit :
> 
> > Q: () → P(0) // this is very different from writing: unit → prop
> 
> Indeed, my apologies, I was silly (red-face):
> 
> propdef p:prop = P(0) // OK and in the static.  
> prval q:P(0) = Q // OK and in the dynamic, however erased by the compiler.
> 
> The type of `Q` is `P(0)` which is of sort `prop`.
> 
> > […] the argument of R is often called a proof.
> > 
> > So one must be able to say prop = proof. That makes sense, if P is not a  
> > prop constructor, not a prop.
> 
> That’s OK, modulo my previous errors, everything is clear.
> 
> Your lights really lit 😛
> 
> –  
> You received this message because you are subscribed to the Google Groups  
> “ats-lang-users” group.  
> To unsubscribe from this group and stop receiving emails from it, send an  
> email to [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/e038b307-4288-4cd6-ab5a-fa4e5d2f9d2d%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/e038b307-4288-4cd6-ab5a-fa4e5d2f9d2d%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/e038b307-4288-4cd6-ab5a-fa4e5d2f9d2d%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/e038b307-4288-4cd6-ab5a-fa4e5d2f9d2d%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 10, 2015, 11:01pm UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/13 "2015-12-10T23:01:56Z")

</div>

> Maybe you just need to be more creative in creating an inconsistent  
> set of axioms. 🙂
> 
> A disproof can be done with ‘case … =/=\>’ so I am not sure a ‘false  
> proposition’ can’t exist. I’ve used it for reductio ad absurdum.

So this is not sound:  
stadef h: prop → bool = (lam p =\> true)  
?

And I can’t use it in predicates without introducing inconsistencies?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [December 10, 2015, 10:51pm UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/14 "2015-12-10T22:51:25Z")

</div>

A ‘prop’ in ATS is for classifying types for proofs  
(and ‘type’ is for classifying types for (run-time) values).

You could have

stacst False: prop

What you should not introduce is

prfun False\_elim : {a:prop} False → a // False implies everything

Because you can prove very thing if False\_elim is available.

Here is an encoding of propositional logic in ATS:

[http://www.cs.bu.edu/~hwxi/academic/courses/CS520/Fall15/code/lecture-09-21/prop-logic.dats](http://www.cs.bu.edu/~hwxi/academic/courses/CS520/Fall15/code/lecture-09-21/prop-logic.dats)

You can see clearly that ‘False’ is indeed encoded.On Thursday, December 10, 2015 at 5:41:19 PM UTC-5, Barry Schwartz wrote:

> ‘Yannick Duchêne’ via ats-lang-users \<[ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> \<javascript:\>\> skribis:
> 
> > Moreover ATS propositions are never false, they are always true, or  
> > can’t  
> > exist at all, which is not a surprise, as ATS propositions are proof in  
> > the  
> > form of definitions, with `absprop` or in the form of inductive  
> > definitions  
> > with `dataprop` (which is not exactly the same as an axiomatic proof, an  
> > inductive definition is a safer assertion).
> 
> Maybe you just need to be more creative in creating an inconsistent  
> set of axioms. 🙂
> 
> A disproof can be done with ‘case … =/=\>’ so I am not sure a ‘false  
> proposition’ can’t exist. I’ve used it for reductio ad absurdum.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [December 11, 2015, 5:48am UTC](https://discourse.ats-lang.org/t/wording-and-interpretation-propositions-predicates-and-types/407/15 "2015-12-11T05:48:16Z")

</div>

> Q: () → P(0) // this is very different from writing: unit → prop

Indeed, my apologies, I was silly (red-face):

propdef p:prop = P(0) // OK and in the static.  
prval q:P(0) = Q // OK and in the dynamic, however erased by the compiler.

The type of `Q` is `P(0)` which is of sort `prop`.

> […] the argument of R is often called a proof.
> 
> So one must be able to say prop = proof. That makes sense, if P is not a  
> prop constructor, not a prop.

That’s OK, modulo my previous errors, everything is clear.

Your lights really lit 😛