It sure is if you read enough "Functional Pearls" to think all you need for logic programming is some backtracking. Oh, and the cut. Because you can't control backtracking without the cut. Not if you don't understand what the backtracking is for in the first place! Mwahahaha.
I suppose you could hack a bug-ridden implementation of Prolog unification in Prolog but why?
Hindley-Milner type inference is unification over types and unification is built-in to Prolog. Functional programmers ignore this because their textbooks never refer to the original description of unification by Robinson. Wait who? Unification was probably invented by Damas, Hindley or Milner right? Or maybe Haskell Curry? Hey maybe it was John McCarthy?
More to the point, our mathematics work to solve real problems up to a certain point. For instance our mathematics have not yet been able to identify polynomial-time solutions to problems in the class NP and it's possible that this is exactly because our mathematics are inadequate to express such solutions, if such solutions do exist (and Donald Knuth, for example, believes they do). In which case we'll never know whether P = NP (or we will, but it won't be any use, similar to what Knuth, again, suggests).
It is a tautology that the famous incompleteness results in mathematics and computer science are the result of the axioms of arithmetic used to derive them. Would Gödel be able to derive his incompleteness result without Peano's axiomatisation of arithmetic? Not really. Arithmetic is axiomatic and our axioms of it are arbitrary and ad hoc. Because they're axioms. Who says aliens would come up with the same ones?
There are huge assumptions made in this thread that only indicate the brief time that the contributors have given to thinking about all this stuff. If you think about it for a couple of minutes, sure, it all feels very natural. Zero, infinity, division, mathematical logic, set theory, etc. But if you think about it a bit more, and then do a bit more than think, and go read about it, it's obvious that those are just the ideas that we chose to go with, not the only ones that exist, and certainly not the only ones proposed by mathematicians, logicians, computer scientists and philosophers over the years. For instance, Hilbert was a finitarian, division doesn't work with zero, zero doesn't work with division, dividing an infinity multiplies it, material implication leads to counter-intuitiveness paradoxes, set theory with only the membership relation leads to paradoxes, etc etc etc. Mathematics is full of unnatural holes that need constant patching up, and there is nothing to say that it is in any way, shape or form "real", let alone universal as so many people in this thread seem to be saying.
> And the Pythagorean theorem is a universal truth that holds everywhere.
Or at least in every world where there exist straight lines, yes? For instance:
> The Pythagorean theorem is derived from the axioms of Euclidean geometry, and in fact, were the Pythagorean theorem to fail for some right triangle, then the plane in which this triangle is contained cannot be Euclidean. More precisely, the Pythagorean theorem implies, and is implied by, Euclid's Parallel (Fifth) Postulate.[59][60] Thus, right triangles in a non-Euclidean geometry[61] do not satisfy the Pythagorean theorem. For example, in spherical geometry, all three sides of the right triangle (say a, b, and c) bounding an octant of the unit sphere have length equal to π/2, and all its angles are right angles, which violates the Pythagorean theorem because {\displaystyle a^{2}+b^{2}=2c^{2}>c^{2}}.
> Any such alien will distinguish true and false, will have AND, OR and NOT connectives, and will understand a form of implication (it's inherent to causality).
Implication doesn't have anything to do with causality and in fact the concept of implication in mathematical logic is broken. See: the paradoxes of material implication:
To simplify, F -> T (true if false) is a true implication so, for example, I can say that "I am the pope therefore it rained yesterday" and, if it rained yesterday, then the implication is true even though I am not the pope. There has been endless grumbling among philosophers and mathematicians because of this kind of paradox but it is an inevitable result of the axiomatic definition of implication by means of a truth table, and there's no way to correct it without also changing the truth tables of disjunction and negation (because A OR NOT B is equivalent to NOT B THEREFORE A, i.e. because of the way disjunction and negation work, false implies true; you will have to work through this on your own and hit your head on your desk very hard, many times, just as I did when I first realised what a mess this is).
In other words, either we accept human axioms of logic, and we have paradoxes of implication, or we don't have paradoxes of implication but then we don't accept human axioms of logic. An alien civilisation may well choose to not accept any axioms of logic that lead to paradoxes of material implication, so they won't have human axioms of logic and, if their formal system is sound, they won't have human logic, and therefore, no human mathematics.
In other words, no, aliens will not necessarily have the same mathematics as humans.
Oh sorry. Did I let my schadenfreude out again?