как доказать следующие утверждения с помощью Isabelle / HOL?

Может ли кто-нибудь помочь мне доказать X=M, используя следующий набор уравнений (логика первого порядка) в Isabelle / HOL?

N>=M

forall n. 0=<n<N --> n<M

X=N

где N, M, X - целые постоянные. n целочисленная переменная .. '->' означает подразумевает


first-order-logic isabelle
person Tom    schedule 23.09.2019    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Доказательство может быть выполнено только в том случае, если переменные являются натуральными, а не целыми числами, например используя это доказательство:

theory Scratch
imports Main
begin
theorem
  fixes N M X :: nat
  assumes "N ≥ M"
  assumes "∀ n. (0 ≤ n ∧ n < N) ⟶ n<M"
  assumes "X = N"
  shows "X = M"
proof-
  have "¬ N > M"
  proof
    assume "M < N" with `∀ n. _` show False by auto
  qed
  with `N ≥ M` and `X = N`
  show "X = M" by auto
qed

end

Если вы разрешаете целые числа, то контрпримером будут M=-2, N=-1 и X=-2.

person Joachim Breitner    schedule 23.09.2019
comment
большое спасибо. Еще один вопрос: если свойство X = N ^ 3, то нам нужно определить мощность. Не могли бы вы помочь мне в этом вопросе? - person Tom; 23.09.2019
comment
Думаю, вы можете написать N ^ 3 для полномочий. - person Joachim Breitner; 23.09.2019