Logical equivalence of logical propositions that are converted from compact (implicit) notation to Mathematica code

Question

Here is logical formula:

$$\bigwedge_{i=1}^{9} \bigwedge_{n=1}^{9} \bigvee_{j=1}^{9}~p(i,j,n)$$

To use it in Mathematica I use that code:

X=Array[p[#1,#3,#2]&,{9,9,9}];a=Apply[And,Apply[And,Apply[Or,X,{2}],{1}],{0}];
Y=Array[p,{9,9,9}];b=Apply[And,Apply[And,Apply[Or,Transpose[Y,{1,3,2}],{2}],{1}],{0}];
c = 0

Two methods are used above. In the first one, I am putting the result in a variable and with the second method in b variable.

Now:

MatchQ[a,b]

True

MatchQ[a,c]

False

So, I conclude that the output of a and b are the same.

Now I want to check the logical equivalence of a and b.

I tried:

TrueQ[Equivalent[a, b]]

True

TrueQ[Equivalent[a, c]]

False

TrueQ[Equal[a,b]]

True

TrueQ[Equal[a,c]]

False

SameQ[a,b]

True

SameQ[a,c]

False

---

Questions:

1. What is called the content of a and b? Logical formula? Function(s)? Normal expression? Object? Other?

2. Are the all ways of checking the logical equivalence of a and b that I have used above right?

3. Are there any other possible ways to check the logical equivalence of a and b that I have not used above?

4. Is there one best way to check the logical equivalence of a and b and if yes which one and why its is best one?

Answer 1

1). Maybe, this would be referred to as "Boolean expression" in Mathematica speech.

2.) SameQ is problematic as it does not respect the logical content:

hamlet = Or[be, Not[be]];
a = SameQ[hamlet, True]
b= Equivalent[hamlet, True]

False

be || ! be

So using these in later computions may lead to wrong results:

Simplify[a]
Simplify[b]

False

True

The TrueQ/Equal combo is similarly dangerous as TrueQ will return False whenever it gets a symbolic expression as arguments that does not evaluate immediately to True. Better not use it here.

Moreover, Equivalent may be able to perform some simplifications that Equal cannot perform because using Equivalent implies that its arguments are Boolean expressions.

3.) Some more simplifications are performed by TautologyQ:

TautologyQ[Equivalent[hamlet, True]]

True

4.) In life, there is usually never one best way to do anything. For example,SameQ is a very inexpensive test and if it evaluates to True, you are done. Equivalent and TautologyQ have to perform actual computations, taking a bit longer.