Каково формальное и полное определение слов «мета-логика» и «объектная логика» в Изабель? Я вижу, что люди продолжают использовать их, но не могут найти для них никакого определения.Определение «Мета-логика» и «объектно-логическая» (как слово) в Isabelle
Вы не можете найти их, потому что они специфичны для Изабель (насколько я знаю). «Объектная логика» и «мета-логика» - это слова, введенные Ларри Полсоном (насколько я могу судить). В целом, хотя и не конкретно, они связаны с общими терминами «метаязык» и «предметный язык», для таких дисциплин, как логика и теория множеств. Сделайте поиск по ним, и вы получите стандартные вики-страницы, потому что они являются стандартной частью логики.
Вот, я смотрю на странице 16, 2.2.3 Мета и объектного языка из логики и Вычислительного - Интерактивная Proof с Cambridge LCF, Ларри Полсон, опубликованной 1987. В то время он был еще соответствующей до стандартных терминов, но затем он переключился. Я забыл, где я его прочитал, но он переключился куда-нибудь на «мета-логику» и «объектную логику», чтобы прояснить ситуацию в своих целях. Эти два термина находятся в его документах и в документах рассылки Изабель.
Другие могут дать вам свои экспертные знания, но мета-логика конкретно то, что вы получаете, когда вы импортируете теорию Pure, в частности, минимальный набор логических связок, ==>, \<And>, &&& и ==. Обсуждение этих вопросов распространяется по всей документации по распространению Изабель.
Я ничего не знаю об интуиционистской логике, кроме того, что она не предусматривает закон исключенного среднего, но вы прочтете, что они обеспечивают минимальную, интуиционистскую логику.
Не благодарите меня. Я только что кое-что прочитал здесь и там, и слушал. Другие могут предоставить экспертные знания.
Мои выводы по этому вопросу ниже.
я нашел в Clemens Ballarin slides, slide 20.:
Meta логика: Логика, используемая для формализации другой логики.
Пример: математика, используемая для формализации дифференцирования в формальной логике.
и ставится параллельно:
Мета язык: язык используется, чтобы говорить о другом языке.
Примеры: немецкий в испанском классе, английский в английском классе.
В Википедии есть запись на Metalogic, один раздел Метаязык - язык объекта:
В металогики, формальные языки иногда называют языки объектов. Язык, используемый для составления заявлений об объектном языке, - это , называемый метаязыком. Это различие - ключевое различие между логикой и металогией между .Хотя логика имеет дело с доказательствами в формальной системе, выражается в некотором формальном языке, металогика имеет дело с доказательствами о формальной системе, которые выражаются в метаязыке о некотором объекте языке.
А вот слайд 21 из Ballarin:
