According to your "how it should be", Fpc should also not allow "Boolean(5)".
Correct. That doesn't make sense because a boolean value can only have two values, true and false, which are supposed to be 1 and 0 respectively so they fit in _one_ bit.
FPC and Delphi allowing boolean(5) creates a type (which is not a genuine boolean) that cannot be represented with one bit, therefore cannot be bitpacked, therefore isn't a boolean.
IOW, the behavior and semantics of boolean types should remain the same whether they are packed or unpacked.
However, once we accept that it does, the result of the comparison in your example is known to be undefined, and there is no "logic in wonderland" at all.
No, the result isn't undefined because FPC _consistently_ will consider zero (0) as false and _not zero_ as true, which is _not_ the definition of a boolean.
Accepting booleans with a value of 5 (or some other value that is neither zero (0) nor one (1)) is like accepting square circles.
Once you leave the valid scope, behaviour does not have to be defined.
That argument doesn't work because FPC is very consistent in considering "not zero" as true and "zero" as false. That seems to be rather well defined.
If your point is: You dislike type-casting (at least the way it currently happens to be) => well, you can make that point.
My point is: I dislike invalid typecasts such as boolean(5) which is as wrong as typecasting a null terminated array[11..2017] of char to an integer. The numeral 5 doesn't fit in one bit anymore than that array fits in an integer.
Thanks for quoting this out of context 
It wasn't my intention. I missed the point you were making.
But if those values are not boolean values, why should your example code work?
The compiler should not allow a typecast "boolean(5)" because it knows that the numeral 5 cannot be represented with a single on/off instrument.
By typecasting them into boolean, you acknowledge that you mess up the underlying data in the boolean var. It no longer contains the binary representation for true, nor for false. So, as I said, it leads to undefined behaviour.
If the behavior was really undefined then it would not be predictable yet, it is rather predictable that any value other than zero is considered true, therefore it is not undefined, it is simply incorrect.
Yes, I understand, you would rather that typecast was not allowed.
Correct.

Why do you highlight the comparison line by using a text like "(logic in wonderland)"?
because the compiler consistently states that a non zero value is logically true but when two logically true values are compared, it says they are not equal. If two values are logically equal (true) then the compiler cannot claim they are logically different. The problems stems from the fact that it uses an arithmetic operation (an arithmetic comparison) to determine equality on logical types. That's inherently incorrect.
The undefined behaviour just currently coincides with C BOOL. Does not mean it is the same....
You're right, they aren't the same but, there is one thing that is _always_ the same: not zero always means "true". It's difficult to consider that "undefined behavior" when it is always the same.
"undefined behavior" implies not predictable.
the way it's documented is incorrect.
Different issue.
Not really. It's documented according to what boolean is _supposed_ to be in Pascal which is different than what boolean actually is in FPC and Delphi.
But nothing in the field of boolean algebra somehow mandates that the representation has to be that way. Inventing a different representation would not be wrong, in the sense that it breaks something that is mandated by the underlying concept.
BUT, boolean algebra mandates only two possible values. true = any non zero value violates that.
Choosing which gate state represents true or false is arbitrary but, a gate can represent only two values, zero and one (or whatever names you want to assign to them.) It cannot represent zero and multiple distinct non zero values (they'll have to either, come up with 18 wheeler gates or, "elastic" gates, to accommodate FPC and Delphi's "boolean"s.)
Where does your application "shows that FPC (and Delphi) treat boolean the same as ByteBool, i.e, any non-zero value is true" ?
Fine... no problem. Here is a little test program:
{$APPTYPE CONSOLE}
program TestBoolean8Typecast;
var
i : byte;
b : boolean;
begin
for i := low(i) to high(i) do
begin
b := boolean(i);
writeln('arithmetic b = ', ord(b):3, ' ', ' logical b = ', b);
end;
end.
It prints "true" 255 times and "FALSE" one time. It's surprisingly consistent for something that is supposed to be "undefined behavior".
In fact look at my "bitpacked" example. And assigning "x.a := boolean(2)", will lead to the writeln returning switching between printing true or false. So clearly undefined behaviour.
It's no surprise it trips all over itself when it tries to pack a value greater than 1 into 1 bit. The code you posted shouldn't compile. Even in the 21st century putting a value greater than 1 into a single bit, takes a David Copperfield act.