Beyond propositional calculus lies an analysis of phrases such as ``for all'', ``for every'', ``there exists'' and ``there is''. As we saw in chapter 3, in Nuprl we treat these phrases as operations on propositional functions. Thus the sentence ``for every integer y there is an integer z such that z is less than y'' is analyzed first as the operator all y:int applied to the propositional function ``there is an integer z such that z is less than y''. This in turn is analyzed as the operator some z:int applied to the propositional form z<y. Nuprl provides two propositional forms on the integers: x=y in int and x<y.
Once we have seen how to express arbitrary propositions, we can state all the formulas of the predicate calculus over an arbitrary domain or over an arbitrary nonempty domain as is common in classical logic textbooks. Chapter 3 gave several examples of these statements; we now show how to prove one of them. The snapshots below should be almost self--explanatory, so little further comment will be given.
,----------------------,--------------------------------------, |EDIT THM t3 |EDIT main goal of t3 | |----------------------|--------------------------------------| |? top |>>all A:U1.all P:A->A->U1. | |<main proof goal> | some y:A.all x:A.P(x)(y) => | | | all x:A.some y:A.P(x)(y) | | '--------------------------------------' | | '-------------------------------------------------------------'
,-------------------------------------------------------, |EDIT THM t3 | |-------------------------------------------------------| |# top 1 1 | |1. A:(U1) | |2. P:(A->A->U1) | |>> some y:A.all x:A.P(x)(y) => all x:A.some y:A.P(x)(y)| | | |BY intro at U1 | | | |1# 1. A:(U1) | | 2. P:(A->A->U1) | | 3. some y:A.all x:A.P(x)(y) | | >> all x:A.some y:A.P(x)(y) | | | |2# 1. A:(U1) | | 2. P:(A->A->U1) | | >> some y:A.all x:A.P(x)(y) in U1 | '-------------------------------------------------------'
,--------------------------------------,-----------------, |EDIT THM t3 |EDIT rule of t3 | |--------------------------------------|-----------------| |# top 1 1 1 1 |elim 3 | |1. A:(U1) | | |2. P:(A->A->U1) | | |3. some y:A.all x:A.P(x)(y) | | |4. x:(A) | | |>> (some y:A.P(x)(y)) | | | | | |BY <refinement rule> '-----------------| | | '--------------------------------------------------------'
Since some x:T.P is defined to be a dependent product, an inhabitant of the third hypothesis above is a pair. The next elimination step thus requires two new variables, y0 and h in this case, which will each contain a component of the pair.
,------------------------------------------------, |EDIT THM t3 | |------------------------------------------------| |# top 1 1 1 1 | |1. A:(U1) | |2. P:(A->A->U1) | |3. some y:A.all x:A.P(x)(y) | |4. x:(A) | |>> (some y:A.P(x)(y)) | | | |BY elim 3 new y0, h | | | |1# 1. A:(U1) | | 2. P:(A->A->U1) | | 3. some y:A.all x:A.P(x)(y) | | 4. x:(A) | | 5. y0:(A) | | 6. h:(all x:A.P(x)(y0)) | | >> (some y:A.P(x)(y)) | '------------------------------------------------'
,------------------------------------------------, |EDIT THM t3 | |------------------------------------------------| |# top 1 1 1 1 1 | |1. A:(U1) | |2. P:(A->A->U1) | |3. some y:A.all x:A.P(x)(y) | |4. x:(A) | |5. y0:(A) | |6. h:(all x:A.P(x)(y0)) | |>> (some y:A.P(x)(y)) | | | |BY intro y0 | | | |1* 1. A:(U1) | | 2. P:(A->A->U1) | | 3. some y:A.all x:A.P(x)(y) | | 4. x:(A) | | 5. y0:(A) | | 6. h:(all x:A.P(x)(y0)) | | >> y0 in (A) | | | |2# 1. A:(U1) | | 2. P:(A->A->U1) | | 3. some y:A.all x:A.P(x)(y) | | 4. x:(A) | | 5. y0:(A) | | 6. h:(all x:A.P(x)(y0)) | | >> (P(x)(y0)) | '------------------------------------------------'
,-------------------------------------------------, |EDIT THM t3 | |-------------------------------------------------| |* top 1 1 1 1 1 2 | |1. A:(U1) | |2. P:(A->A->U1) | |3. some y:A.all x:A.P(x)(y) | |4. x:(A) | |5. y0:(A) | |6. h:(all x:A.P(x)(y0)) | |>> (P(x)(y0)) | | | |BY elim h on x | | | |1* 1. A:(U1) | | 2. P:(A->A->U1) | | 3. some y:A.all x:A.P(x)(y) | | 4. x:(A) | | 5. y0:(A) | | 6. h:(all x:A.P(x)(y0)) | | >> x in (A) | | | |2* 1. A:(U1) | | 2. P:(A->A->U1) | | 3. some y:A.all x:A.P(x)(y) | | 4. x:(A) | | 5. y0:(A) | | 6. h:(all x:A.P(x)(y0)) | | 7. (P(x)(y0)) | | >> (P(x)(y0)) | '-------------------------------------------------'