>>689
∀x∈ℕ.∃y∈ℕ.x<y
と
∀x∈ℕ.x<x+1
だと後者の方が強い主張をしてるでしょ
箱入り無数目の定式化では関数の形も主張に必要なんだから後者の形で命題を書かないと