S
ты молодец
Size: a a a
2021 June 10
S
S
ты там в гейпорке уже освоился я смотрю
AG
но поскольку диалектика разрешима, мы можем симметрично определить
Definition invalid (p : prp) := { b : C p | forall a : W p, ~ dia a b }.AG
и тогда
Theorem neoleg : invalid oleg.
Proof.
by exists (existT (fun=> (unit+unit)%type) 0 (inr tt))=>? /=.
Qed.
AG
типа наша стратегия опровержения - даем конкретное число 0 и выбираем правую ветку конъюнкции (что
neg (a==0))AG
тогда независимо от стратегии доказателя мы всегда выигрываем
AG
в целом можно сказать что диалектика это очень специфический вид игровой семантики
AG
которая логике первого порядка ставит в соответствие игру всего из двух шагов
SK
хорошее упражнение, надо его в куда-нибудь включать
AG
либо сначала ходит доказатель, а потом зная его ход, пытается выиграть опровергатель (игра в валидность)
AG
либо наоборот (игра в невалидность)
SK
с чего начать въезжать в игросем какому-нибудь аспиранту с каким-нибудь sf в бэкграунде?
AG
ну вот с диалектики например :)
AG
можно попробовать сразу нырять в арена-игры типа как тут https://github.com/clayrat/Game_Semantics/blob/polymorphic_pointer_seq_refactor/Ghica.v
w
могу провести ресерч по читаемости среди моих коллег
AG
в целом наверное без мотивации сложно будет понять что там и зачем
AG
т.е. неплохо бы в общих чертах представлять как исторически развивалась денотационная семантика, и в чем там были фейлы с классической теорией доменов