Maths - Predicate Category

See also topos theory.

The relationship XcontainsI (X is a subset of I) is a predicate. We can form a category of predicates on sets as follows:

Objects

predicates are pairs (I,X) where
XcontainsI

X(i) implies an element i∈I is a free variable in I.

predicate category 1
Morphisms

(I,X) -> (J,Y) where:

u:I-> J and X(i) implies: Y(u(i))

So, to define(I,X) -> (J,Y) , we need maps u:I -> J and X -> Y but X -> Y is implied by u.

predicate category

Reverse map

'subsitution functor' u*

examples of substitution are:

  • weakening
  • contraction
reverse
weakening   weakening
contraction   contraction
quantifiers   quantifier

metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

 

Commercial Software Shop

Where I can, I have put links to Amazon for commercial software, not directly related to the software project, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.