logic - 如何在形式系统中证明¬(2|9)？

Question

2|9 表示 ∃x(9=2 x)，∃x(g(x)) 表示 ¬∀x(¬g(x))。所以，¬(2|9) 表示 ∀x(¬(9=2 x))。直观地说，我们通过证明“对于任意 n”“¬(9=2 n) ”来证明 ∀x(¬(9=2 x)) 。但是在正式系统中，对于任意 t，我们只有公理∀x(g(x)) → g(t)，但是“对于任意 t 的 g(t)” → ∀x(g(x)) 既不是公理，也不是公理作为公理可以接受。因此，证明“对于任何 n 的“¬(9=2 n)”不足以证明形式系统中的 ∀x(¬(9=2 x))。那么，如何在形式系统中证明¬(2|9)？

标签： logicnumber-theoryformal-languages