Я хочу формализовать формальные языки и их семантику в MMT и определить общее понятие семантики. эквивалентность двух семантик относительно. один синтаксис. Именно кодирование последнего оказывается идентификацией/склеиванием, что я понятия...

Учитывая следующие теории, которые формализуют бессмысленные вещи для целей небольшого MWE, theory Meta : http://cds.omdoc.org/urtheories?LF = ℕ: type ❙ prop: type ❙ or: prop ⟶ prop ⟶ prop ❘ # 1 ∨ 2 ❙ ❚ theory S : ?Meta = c: ℕ ⟶ ℕ ⟶ prop ❘...