AG
Ладно
Size: a a a
2021 November 15
a
@nulled_brain Толку будет больше если сообщать о том, как идут дела с прошлыми упражнениями.
2021 November 16
ДГ
Это про какие именно упражнения
a
Ну вот это например.
Остальные не помню, но было еще. Мне к сожалению было лень разбираться с упражнениями про вычисление объемов, но было еще что-то, и там у меня осталось ощущение незавершенности.
Остальные не помню, но было еще. Мне к сожалению было лень разбираться с упражнениями про вычисление объемов, но было еще что-то, и там у меня осталось ощущение незавершенности.
NC
Добрый день, правильно я понимаю, что такие рассуждения как:
не(А или В) <=> не А и не В
Стоит доказывать через таблицу истинности?
не(А или В) <=> не А и не В
Стоит доказывать через таблицу истинности?
NC
То есть я бы сказал, можно доказывать*
a
«такие как» это какие?
NC
не(А или В) <=> не А и не В
NC
Это другой пример
s
Докажи через правила вывода.
s
https://gist.github.com/suhr/d5b7784e0760933279a1e6498df77264 — вот подробнее с примерами на Isabelle и Lean.
NC
Понял, посмотрю спасибо
s
Кстати, твой вариант даже исключения третьего не требует, в отличие от https://t.me/higher_math/64331
a
Я не очень вижу альтернативы таблице истинности. Но я знаю логику хуже чем хотел бы.
NC
понял
s
Могу расписать доказательство, если надо.
T
Распиши.
s
lemma not_or_ {P Q : Prop} : ¬(P ∨ Q) ↔️ ¬P ∧ ¬Q :=
begin
apply iff.intro,
show ¬(P ∨ Q) → ¬P ∧ ¬Q, {
assume npq: ¬(P ∨ Q),
split,
show ¬P,
{ assume p: P, from npq (or.inl p) },
show ¬Q,
{ assume q: Q, from npq (or.inr q) },
},
show ¬P ∧ ¬Q → ¬(P ∨ Q), {
assume npnq: ¬P ∧ ¬Q,
assume pq: P ∨ Q,
cases pq with p q,
show false, from npnq.1 p,
show false, from npnq.2 q,
}
ends
Надеюсь, расписал достаточно подробно.