Can I Use Functions Returning T/F in Propositional/First-Order Logic? I am writing my (first) paper...
I need to explain about my algorithm.
I think it is good to define some functions/statements.
It is a huge pain to clearly explain them in words.
But I am not that familiar with mathematics so I am not sure if I can use functions I defined in Propositional/First-Order logic statements.
$$P\text{.isEqualTo}(P')=
\begin{cases}
\text{false,} & |P|\neq|P'|\\
\overset{|P|}{\bigwedge\limits_{i=1}}\left(P_i={P_i'} \right),& \text{otherwise}\\
\end{cases}$$
$$P\text{.isMoreGeneralThan}(P')=
\begin{cases}
\text{false,} & |P|\neq|P'|\\
\text{false,}& \overset{|P|}{\sum\limits_{i=1}}\left[P_i\neq P_i'\right]=0 \\
\overset{|P|}{\bigwedge\limits_{i=1}}\left(P_i={P_i'} \space\space\lor\space{}_{\text{-}}\right),& \text{otherwise}\\
\end{cases}$$
I defined 'pattern equality' and 'pattern generality.' Can I use them in the logical statements:
$$P\text{.isMatchedBy}(P')\impliedby P.\text{isEqualTo}(P')\lor P.\text{isMoreGreaterThan}(P')$$
$$P\text{.isParentOf}(P')\impliedby P.\text{isMoreGeneralThan}\land \left(\sum_{i=1}^{|P|}\left[P_i \neq P_i'\right]=1\right)$$
If possible, can I also wrtie a first order logic statement using quantifier like:
$$P\text{.isAddable()}\impliedby \exists P'(P'\text{.isParentOf}(P)\land P'\text{.isExpendable}())$$
where 'expandability' is defined as:
$$\text{P.isExpendable}()=
\begin{cases}
\text{True} & P\text{.SP}-\max\limits_{p\in\left\{P'|P'\text{.isParentOf(P)}\right\}}p\text{.SP}\gt\eta\\
\text{False}, & \text{Otherwise}
\end{cases}$$
Ah, I am in total confusion. Please save me. Thank you geniuses!
 A: These expressions are certainly not part of the standard language of First-order logic (FOL). As you already suspected, summations and programming constructions like $P.isEqualTo(P')$ are not part of FOL. Now, if this is just pseudocode to convey certain ideas, then it should be fine though. Also, if you really need it to be in FOL, you can do so with some additional effort. For example,
$P.isMatchedby(P') \Leftarrow P.isEqualTo(P') \lor P.isMoreGreaterThan(P')$
Can be put into FOL like so:
$\forall x \forall y ((Equals(x,y) \lor GreaterThan(x,y)) \rightarrow MatchedBy(x,y))$
For a more complicated example, you can express the $P.isEqualTo(P')$ with something like:
$\forall x \forall y (Equals(x,y) \leftrightarrow (size(x) = size(y) \land \forall z ((1 \le z \land z \le size(x)) \rightarrow ent(x,z) = ent(y,z))))$
where $size(x)$ is a function symbol that expresses the function $|P|$, and where $ent(x,z)$ denotes $P_i$ assuming $x$ denotes some object $P$ and $z$ some number $i$. Note that you may need to add some axioms to deal with $1$ and $\le$ if you were to use this in practice.
But again, if you goal is to simply convey some idea, then your notation has plenty of rigor to be precise, and is probably more readable than a full FOL epression.
