Maxima で綴る数学の旅ゴールに存在量化子が入っている場合、存在量化子がついた変数に値を入ることでゴールの論理式を証明することができます。useタクティクを使うと、「この値を使え」ということができます。例えばこんな感じです。 example : ∃ x : ℝ, 2 < x ∧ x < 3 := by use 5 / 2 -- ⊢ 2 < 5 / 2 ∧ 5 / 2 < 3 norm_num -- No goals ゴールの論理式の意味は「2より大きくて3より小さい実数xが存在する」です。まあ当たり前ですがどうやって証明するかです。この場合xが$\frac{5}{2}$であればこの不等式は確かに成立するので、xが存在することがわかり証明が終わります。 use 5/2とするとゴールの論理式が次のように変化します。 ⊢ ∃ x, 2 < x ∧ x < 3 が以下に変化する ⊢ 2 < 5 / 2 ∧ 5 /
