Fix 150--154.

1 files changed, 6 insertions, 7 deletions

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index c9f280b..3abcdef 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -165,13 +165,12 @@ pairing function, we can encode the binary tree constructors as
 One can pattern match on G\"odel encodings by unpairing a value to
 split it back into the tag and payload.
 
-One major limitation of G\"odel encodings is that they cannot
-represent higher-order data such as functions. The defining trait of
-G\"odel encodings is that they represent data by natural numbers. As
-function types cannot be encoded as naturals, we cannot encode
-functions. We also cannot use a syntactic representation of functions;
-\textcite{Squid:unpublished/Bauer17} proves there is no System~T term
-that can recover a function from its syntax.
+A major limitation of G\"odel encodings is that they cannot represent
+higher-order data such as functions. G\"odel encodings by definition
+encode data as natural numbers. We cannot encode arbitrary functions
+as naturals, even in simple models such as \mathsf{Set}. If we
+restrict ourselves to representable functions, \textcite{bauer} proves
+we cannot recover a function from its syntax.
 
 Another difficulty with G\"odel encodings is implementing the fold
 operation.  We require our chosen pairing function to be monotonic so