2.2 The fixed point theorem
GL ⊢ B ↔ A(B)
GL ⊢ LiarParadox ↔ ~True(LiarParadox)
Do you see the similarity? Prolog rejects both of these as erroneous.
Here is the error that Prolog detects: (see above link)
match a term against an uninstantiated subterm of itself.
The exact same thing as this C++
bool LiarParadox = LiarParadox == false;
Copyright 2017 Pete Olcott
Copyright 2016, 2017 Pete Olcott