A better general definition of a predicate

Question

What's a better definition for (an interpretation of) a predicate in general (i.e. non-theory-specifically):

(1) a proposition-valued function.
(2) a proposition-valued function w/ a nonempty domain.

This suggests (2), while that suggests (1). (1) seems to imply the principle of propositions-as-predicates, which makes sense if we view predicate logic as a generalization of propositional logic. (You may suggest better definitions if you have one)

Answer 1

For the changed question, about the interpretation of predicate symbols instead of about predicates, in general it is a function from the domain to the collection of truth values. The domain need not be non-empty (that is peculiar to the conventional definition of first-order logic but not always assumed so), and the truth-values may not be two (such as in 3-valued logic).

Note that this definition is implementation-agnostic; you could have defined the truth values to be $0,1$ for $\bot,\top$ respectively, in which case predicates would be the same as indicator functions on the domain. Or you could have done otherwise; the definition will just follow along.

Answer 2

Very very generally, a predicate is something that expects zero or more objects as inputs and produces a truth value as output. Now, of course you have to specify what exactly that means.

In particular, in first-order logic here are two possible definitions of predicates (but you cannot choose both!):

1. Simply a (well-formed) formula. The inputs are the free variables, and the output is the truth value of the formula (in a given model).

2. An function $f$ in the meta-system based on a formula $φ$ with numbered blanks that when given terms as inputs produces a formula that is obtained by substituting each blank numbered $k$ by the $k$-th input term. Under this definition a predicate applied to terms can still have free variables.

Also, there are things called predicate symbols, which are just symbols that can be used in a formula by writing it with the appropriate number of terms after it, usually placed in brackets. Of course, for every predicate symbol there is a corresponding predicate (no matter which definition above you choose) that 'behaves' the same way.

But predicate symbols are not the same as predicates. However, for any first-order theory we can add in one predicate symbol for every predicate, like this:

  For each $k$-input predicate $P$:

    Let $p$ be a new predicate symbol.

    Add the axiom $\forall x_{1..k}\ ( P(x_{1..k}) \leftrightarrow p(x_{1..k}) )$.

This can be proven to give a conservative extension of the original theory, meaning that any sentence over the original theory can be proven iff it can be proven over the extended theory. This is in fact how we formally justify definitions!

For example over the theory of $PA$ we can let $even$ be a new predicate symbol such that:

  $\forall n\ ( even(n) \leftrightarrow \exists k\ ( n=k+k ) )$.

Since this is a conservative extension, we can now work in the extended theory and use $even$ anywhere we like without worrying that we can prove 'more' than we could before.

A similar technique can be used for formulae that 'express functions', but that's for another time!