From 9748fdc127c537fcae6d6272c819514819d8e252 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 18:18:26 +0100
Subject: Fix 150--154.

---
 sec/systemt.ltx | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'sec/systemt.ltx')

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
-- 
cgit v1.2.3

