How would you represent exponents in predicate logic statements?

Question

So I've seen simpler logic statements that are translated into English, but for this one, how exactly could this be represented?

"For any positive number, there exists a second number, the square of which is equal to the first number."

In predicate logic, could you add exponents? Something like this?

$$(\forall A) \,\,(\exists B) \,\,B^2 \equiv A$$

Given that $A$ is the first integer and $B$ is the second. Or do they even need to be 2 separate variables?

Answer 1

$\forall a: \forall b: [N(a) \land N(b) \implies [S(a,b) \iff M(a,a,b)]] $

Where the predicates $N,M$ and $S$ can be interpreted as follows:

$~~~~~N(x)~~~~~~~~~~\equiv ~~$"$x$ is a number"

$~~~~~M(x,y,z)~~\equiv~~ x\cdot y =z$

$~~~~~S(x,y)~~~~~~~\equiv ~~ x\cdot x = y$

Answer 2

1. "For any positive number, there exists a second number, the square of which is equal to the first number." $$(\forall A) \,\,(\exists B) \,\,B^2 \equiv A$$

   do $A$ and $B$ even need to be 2 separate variables?

   Yes, here, $A$ and $B$ are required to be separate variables.

2. could you add exponents, like this?

   Am I correct in guessing that you made up the exercise?

   In symbolic/formal logic (which is algorithmic/programmable by design), a statement consists not only of logical symbols like $\forall$ and $\to,$ but also non-logical symbols (which depend on the "language" and "model" that we are working in), e.g., arithmetical symbols like $0$ and $+.\quad$ My model may for example have $\#$ as a binary arithmetical operator (like $+$ is) such that $B\#2$ means $B^2.$

   Note that mathematical writing containing symbolic statements like $$\forall \epsilon>0\;\exists \delta > 0\;\forall x\;\big(|x-x_0|<\delta\implies|f(x)-a| < \epsilon\big),$$ is not formal logic.

3. The meaning of the symbol $\equiv$ depends on the text/context, and I like to use it metalogically to mean logical equivalence (i.e., a biconditional $(\leftrightarrow)$ statement that is true regardless of what its non-logical symbols mean). In contrast, the equality relation $=$ is actually a standard logical symbol, which ought to be used instead of the $\equiv$ in your suggested statement.

4. The parentheses around $\forall A$ and $\exists B$ are redundant; on the other hand, parentheses are required when the quantification is meant to apply beyond its minimum construeable scope. So, $$\forall x\;(x=0\to x=0')\\\not\equiv(\forall x \;\,x=0\to x=0')\\\equiv\forall x \;\,x=0\to x=0'\\\equiv(\forall x\;\, x=0)\to x=0'\\\equiv(\forall x)\; x=0\to x=0'.$$