弱ケーニッヒ補題と1階論理の完全性定理の同値性はRCA0だけで書ける。
これは見かけ上の記述がRCA0でOKということ。
実際にこれらの同値性を証明する議論に
どういう体系(最低でも公理的集合論？)が必要かは
明確に述べられないと思う。

1階論理とその完全性定理をすべて公理的集合論(例えばZFC)で書いたとき、
完全性定理を意味する長大な論理式の中に、
選択公理から推論される何らかの論理式を使わなければ、
論理式を整列することはできないことは簡単に想像できる。
ところが論理式をゲーデル数化することで、この選択公理が不要になることもわかっている。
事実不完全性定理の対角定理で選択公理が不要なのはこの議論による。