The way Prolog is "declarative" is that it bridges the gaps between assertions about the properties of a result and actions used to achieve those properties. For example,

    p(X) :- sorted(X).

is saying both (the imperative) "p(X) = sort(X)" and (the assertive) "a sorted X has property p(X)". To solve for P(X), one only needs to find an X such that X is sorted. This makes it difficult to say: "I expect input that, when sorted, has this property" because there is no clear meaning when X is uninitialized. Yet if you expand the meaning you can become "more explicit" about it and convince Prolog that what you're saying is true.

To express "I expect input that, when sorted, has this porperty", you have to use slightly more modern language features that are called constraints.

For example, let us describe sorted lists of integers:

    sorted([]).
    sorted([L|Ls]) :-
            maplist(#=<(L), Ls),
            sorted(Ls).

Here, I am using the CLP(FD) constraint (#=<)/2 that works correctly in all directions, whether or not its arguments are already instantiated to concrete integers. Such constraints are available in all widely used Prolog systems. You can try the above in GNU Prolog, for example.

Now the point:

Exactly as you say, the predicate works for concrete lists of integers that are already given:

    ?- sorted([1,2,3]).
    true.

    ?- sorted([2,1,3]).
    false.

And moreover, it also works if the integers are not given, for example:

    ?- sorted([X,Y,Z]).
    Z#>=X,
    Y#>=X,
    Z#>=Y.

We can even ask for example:

    ?- sorted([X,2,3]).
    X in inf..2.

This means that if this relation holds, than X is at most 2.

We can obtain concrete solutions with enumeration predicates. For example:

    ?- Vs = [X,Y,Z], sorted(Vs), Vs ins 1..3, label(Vs).
    Vs = [1, 1, 1], X = Y, Y = Z, Z = 1 ;
    Vs = [1, 1, 2], X = Y, Y = 1, Z = 2 ;
    Vs = [1, 1, 3], X = Y, Y = 1, Z = 3 ;
    Vs = [1, 2, 2], X = 1, Y = Z, Z = 2 .

And maybe most strikingly, we can also use this in the most general sense, where we ask: Is there any solution whatsoever? The system generates answers in this case:

   ?- sorted(Ls).
   Ls = [] ;
   Ls = [_28] ;
   Ls = [_170, _176],
   _176#>=_170 ;
   Ls = [_1194, _1200, _1206],
   _1206#>=_1194,
   _1200#>=_1194,
   _1206#>=_1200 .

Note that all these considerations lead us to the conclusion that "sorted" is a rather bad name for the relation, since it implies that "something has been sorted" and thus encourages a rather imperative view. A better name would be ascending/1, denoting a relation that is true iff its argument is a list of ascending integers, whether or not they are already known.

>> (the assertive) "a sorted X has property p(X)".

Sure, but X is a variable, implicitly universally quantified, and p(X) <- sorted(X) is only going to be true for some values of X. Unless you apply some stricter constraints, for example, as indicated below, you can't really know for which values the relation is true.

Are you saying that, in a purely declarative context, p(X) :- sorted(X) is always true? That depends entirely on the definition of sorted/1. For instance, the following is trivially always false:

  p(X):- sorted(X).
  sorted(X):- false.

And the following always true:

  p(X):- sorted(X).
  sorted(X):- true.

Normally, sorting predicats will do something more interesting- including declaring properties of X that would probably answer your question.

I'm still a bit unsure about what you are trying to say and what you mean with inlining properties etc so apologies if I haven't addressed your concerns.