Can I Write Propositional Logic Statement Using Functions Returning T/F?

Question

A pattern is a sequence of elements.

Let P, and P' are patterns.

I defined 'equality' and 'generality' as:

$$\def\false{\operatorname{false}}\begin{align} \operatorname {EqualTo}(P, P') ~&:=~\begin{cases}\false &:& \lvert P\rvert \neq \lvert P'\rvert \\[1ex]\bigwedge\limits_{i-1}^{\lvert P\rvert}\big(P_i=P_i'\big) &:& \lvert P\rvert = \lvert P'\rvert\end{cases} \\[2ex] \operatorname {GeneralThan}(P, P') ~&:=~\begin{cases} \false &:& \lvert P\rvert \neq \lvert P'\rvert \\[1ex] \false &:& \sum_{i=1}^{\lvert P\rvert}\big[P_i \neq P_i'\big]=0 \\[1ex]\bigwedge\limits_{i-1}^{\lvert P\rvert}\big(P_i=P_i'\vee \underline{\;}\big) &:& \text{otherwise}\end{cases} \end{align}$$

Then, can I write a propositional logic statement using the two functions like:

$$\operatorname{MatchedWith} \impliedby \operatorname{EqualTo}(P,P')\vee\operatorname{GeneralThan}(P,P')$$

Is it possible?

Or, should I make 'MatchedWith' as a predicate (by using equalit sign instead of implication sign)?

Thank you!

Answer 1

You definitely want to use $MatchedWith(P,P')$ since you want to define this predicate relative to patterns $P$ and $P'$.