6 Predicate types

Examples:

op and:(t => truth ×t => truth) => truth

var x:t; P,Q:t => logical

axiom and(P,Q)(x) <=> P(x) /\ Q(x)

In (an encoding of) a temporal logic, we would have a sort time, and truth values are predicates time => logical. Then a predicate everytime:(time => logical) => logical could be defined as everytime(p) <=> forall t:time.p(t)

Another advantage is that user-defined logical connectives become possible:

op xor:(truth ×truth) => truth

var x,y:truth

axioms xor(x,y) <=> (¬x <=> y)

...xor(phi,psi) ...

Alternatives:

1. Enrich the current proposal by allowing also pred(t) as a synonym for t => truth in order to be consistent with first-order CASL. (This is more a matter of syntax.)
2. Modify the current proposal by requiring pred(t) instead of t => truth (so functions into truth are disallowed). (Again, this is more a matter of syntax.)
3. Modify the current proposal by dropping the special sort truth and adding a type constructor pred, which gives for any type t the type pred(t) of predicates over t, instead. As before, an application of a predicate term to an argument term yields false, if the predicate term or the argument term is undefined.

   With this, we loose the possibility to have user-defined logical connectives in a convenient manner. We have to write:

   op xor:pred(pred() ×pred())

   var P,Q:pred()

   axioms xor(P,Q) <=> (¬P() <=> Q())

   ...xor(\x:().phi,\x:().psi) ...

4. There is a type constructor pred, but the set of admissible types is restricted [Far91] in order to guarantee that each predicate term is defined. Call a type predicative, if it is of form pred(t) or if it is a function type whose result type is predicative. For each predicative type, there is a canonical value given by \x₁....\x_n.false. A type is admissible if it is not forbidden and all its components are admissible. Forbidden types are partial function types with non-predicative codomain.

   Then, predicate application is defined as follows: The predicate term is always defined by the above restriction of the type system. If the argument term is undefined, yield the canonical value, otherwise, apply the predicate.

   This alternative is a s which still captures all practically needed cases. But since the restriction rather adds complexity instead of reducing complexity, we do not find it so useful.

5. Predicate types are allowed only at the top level. This rules out many useful examples (cf. above).