Общий словарь логических понятий: авторское изложение

ru · official · sha256:3297c25928272004e81cab9c15a2dd59816cd5d8aa6001e89fde91feca8f8de9

ОБЩИЙ СЛОВАРЬ ЛОГИЧЕСКИХ ПОНЯТИЙ: АВТОРСКОЕ ИЗЛОЖЕНИЕ Настоящий документ является АВТОРСКИМ ИЗЛОЖЕНИЕМ, составленным для целей формализации семейства пакетов logic.*. Он не является учебником логики, не воспроизводит и не переводит никакой учебник и не содержит ни одного утверждения о том, что верно в той или иной логической системе. Всё, что здесь сказано, относится к УСТРОЙСТВУ ОПИСАНИЯ: какие сущности различаются, какими связями они соединяются и что означает каждая связь. Содержательные определения, схемы правил и сравнительные утверждения живут в пакетах-потребителях и закреплены байтами внешних источников, названных в тех пакетах. Настоящее изложение не является нормативным актом и не имеет силы источника права ни в одной юрисдикции.

Ссылаются нормы: Item

ru · official · sha256:046c39684519efb50ab89d06a0d1c82a78063400e026d03b106c742bc0b40fbc

Раздел 1. Логическая система. Логической системой здесь называется предмет описания, у которого есть имя, принимаемые принципы и отношение следования: классическая логика высказываний, интуиционистская логика первого порядка, модальная система S4 и так далее. Система не есть ни текст, ни исчисление, ни язык: она то, что исчисление представляет, а язык выражает. Ни одно утверждение о системе не выводится настоящим словарём; словарь лишь даёт место, куда пакет-потребитель поставит утверждение своего источника.

Ссылаются нормы: AgreesByAcceptance, DifferenceDerived, DifferenceStated, DiffersByAcceptance, LogicalSystem, agrees_here, answer_difference, differs_by_principle, differs_here

ru · official · sha256:13a7023fd377e4ab0eb0b6f3782f6cb405d0b35b35b90bdc24736b25a3c178dd

Раздел 2. Формальный язык. Формальным языком называется заданный набор символов и правил построения выражений: связок, переменных, предикатов, кванторов, модальных и временных операторов. Один язык может обслуживать несколько систем, и одна система может рассматриваться в нескольких языках. Поэтому язык объявляется отдельной сущностью, а не полем системы.

Ссылаются нормы: FormalLanguage, LanguageOfCalculus, LanguageOfSystem, answer_language, calculus_language, system_language

ru · official · sha256:5643a7f41bc21f34797f59c173f4e290264d3cb9255b344fee919edd1abc2710

Раздел 3. Исчисление. Исчислением называется конкретный аппарат вывода: набор аксиом и правил вывода вместе с понятием вывода. Исчисление ПРЕДСТАВЛЯЕТ систему, и одна система может быть представлена многими исчислениями — естественным выводом, секвенциальным исчислением, аналитическими таблицами, аксиоматическим исчислением. Утверждение «исчисление представляет систему» есть содержательное утверждение источника (корректность и полнота), а не определение; поэтому оно всегда сопровождается ссылкой на источник.

Ссылаются нормы: Calculus, represents_system

ru · official · sha256:6a9c9513c470e13a20f1e0ebc9b05041601aee63779e4ce5ba53bfa7a04c3298

Раздел 4. Формула и схема формулы. Формулой называется отдельное выражение языка. Схемой формулы называется описание формы: выражение, в котором на местах подформул стоят схемные переменные, а всякая формула, получающаяся подстановкой формул вместо схемных переменных, называется экземпляром схемы. Схема есть объект описания правил и принципов; она не является формулой и сама по себе ничего не утверждает.

Ссылаются нормы: PartOfSchema, Schema, SchemaArity, schema_arity, schema_child, schema_shape

ru · official · sha256:d9085bcbb7644f15bb17b2d7c0d9f8018526391bb1cef93f349691f332d0b621

Раздел 5. Схемная переменная. Схемной переменной называется место в схеме, на которое подставляется формула. Схемная переменная принадлежит ровно одной схеме: буквы A и B схемы одного правила и буквы A и B схемы другого правила суть разные схемные переменные, и совпадение их написания ничего не означает. Область действия схемной переменной есть та схема, которой она объявлена.

Ссылаются нормы: ForeignVariableByScope, OwnVariableByScope, SchemaVariable, VariableAtSlot, VariableThroughChild, foreign_variable, own_variable, schema_slot_ref, schema_variable, slot_scope

ru · official · sha256:d3cb63870d96a5068281cffc996560373a7fa6383b935e031ab033f7dcea6736

Раздел 6. Контекст и допущение. Контекстом называется набор формул, принятых на время рассуждения. Допущением называется формула, введённая в контекст шагом рассуждения и подлежащая последующему снятию. Снятием допущения называется действие правила, которое удаляет допущение из контекста заключения. Правило, снимающее допущение, отличается от правила, его не снимающего, и это различие записывается отдельной связью.

Ссылаются нормы: Assumption, discharges_assumption, step_discharges, step_opens_context

ru · official · sha256:34f3d03e32c5304250ff045b142b26763392989ee99a17b3e6b6a8185a5f04f7

Раздел 7. Посылка и заключение. Посылкой правила называется схема, стоящая над чертой; заключением — схема, стоящая под чертой. Посылки правила упорядочены номером: у правила отделения первая посылка есть схема P, вторая — схема из P и Q, соединённых импликацией. Порядок посылок принадлежит описанию правила и не означает порядка их обоснования.

Ссылаются нормы: PartOfRuleConclusion, PartOfRulePremise, has_conclusion, has_premise

ru · official · sha256:59882e0df3a190f7ec9884d83b61ff7ddc6da87bdadb14e1248be1dd544eb865

Раздел 8. Правило вывода как объект описания. Правилом вывода здесь называется ОПИСАНИЕ: имя, посылки, заключение, побочные условия, снимаемое допущение и принадлежность исчислениям. Описание правила не есть само правило движка и ничего не выводит: наличие в пакете описания правила отделения не позволяет и не должно позволять вывести Q из предъявленных делом P и «если P, то Q». Граница проведена намеренно и проверяется отрицательными сценариями.

Ссылаются нормы: InferenceRule, InstructionAvailable, instruction_available

ru · official · sha256:737b4d5bb5ba2dfecb1f715f9b224d00bded3113e1d94509f4b526585d98c20e

Раздел 9. Применение правила. Применением правила называется отдельный шаг предъявленного рассуждения, в котором названы правило, использованные основания и полученное заключение. Применение принадлежит рассуждению, а не исчислению; описание правила принадлежит исчислению, а не рассуждению.

Ссылаются нормы: RuleUse, UseGround, answer_use_ground, use_conclusion, use_ground, use_of_rule

ru · official · sha256:2b46c857eb4e15b8c4fdc61db027daf1847b90670fcd1e161cca04d3c0690df6

Раздел 10. Принцип. Принципом называется схема, принимаемая системой в качестве общезначимой или доказуемой: исключённое третье, устранение двойного отрицания, ex falso quodlibet, схема K, схема T. Отношение системы к принципу может быть трояким: принят, отвергнут либо в настоящем описании не установлен. Третье значение существенно: отсутствие сведений о принципе не есть его отвержение, и словарь запрещает читать молчание как запрет.

Ссылаются нормы: AcceptsPrinciple, Attitude, AttitudeUnrecorded, Principle, RejectsPrinciple, accepts_principle, attitude_to_principle, attitude_unrecorded, rejects_principle

ru · official · sha256:bb16677d81e86379ed346640b660b554b21ce215059bf5324a6ef45f6d66d349

Раздел 11. Статус правила в исчислении. Правило может принадлежать исчислению тремя различными способами: как ОСНОВНОЕ — входящее в определение исчисления; как ПРОИЗВОДНОЕ — имеющее схематический вывод из основных правил; как ДОПУСТИМОЕ — такое, что всякая выводимая с ним секвенция выводима и без него, хотя схематического вывода может не быть. Производное правило допустимо; допустимое не обязано быть производным. Эти три статуса не отождествляются, и ни один из них не приписывается правилу без ссылки на источник.

Ссылаются нормы: RuleStatus, WhereUsed, answer_used_in, rule_of_calculus

ru · official · sha256:b7d13b42f5d66dc04cb142ae6cb4e464cab2d1b36c12a5c0b6591cc6371b6a6e

Раздел 12. Метод и шаг метода. Методом называется пошаговое описание способа обосновать или использовать утверждение определённой формы: как обосновать импликацию, как разобрать случаи, как предъявить свидетеля существования. Метод имеет цель, упорядоченные шаги, зависимости между шагами, условия применимости, используемые правила и понятия, ожидаемую форму результата и границы. Шаг метода есть описание ДЕЙСТВИЯ, а не выполненное действие: шаг «обосновать B в расширенном контексте» при показе инструкции остаётся описанием и никакого B не обосновывает.

Ссылаются нормы: HowToApply, LimitOfMethod, Method, MethodStep, MethodSystem, PartOfMethod, ResultForm, StepDependencyWithinMethod, answer_limit, answer_method_system, answer_result_form, answer_step, answer_step_dependency, contains_step, method_goal, method_in_system, method_limit, method_result_form, step_depends_on

ru · official · sha256:5e9af9b1bfb67ad4e3aa9d78a00cb947df39c582fe3221eba19881751e606c2a

Раздел 13. Условие применения. Условием применения называется требование, при невыполнении которого шаг метода или правило неприменимы: свежесть переменной, отсутствие свободных вхождений, непопадание подставляемого терма под квантор, наличие в системе дополнительного принципа. Условие есть отдельный объект описания, потому что оно называется источником отдельно и переносится вместе с правилом из исчисления в исчисление не всегда.

Ссылаются нормы: Condition, ConditionsOf, answer_condition, requires_condition

ru · official · sha256:18b81c5b03f687d2d9f04e2c3a60f9e041d9085cebd0d9f9ca298f89ec0be366

Раздел 14. Интерпретация и модель. Интерпретацией называется способ сопоставить выражениям языка значения; моделью — интерпретация вместе с носителем, относительно которой определено отношение выполнимости. Описание семантики не требует ни перебора носителя, ни построения модели: пакет сообщает, ЧТО задано определением, ЧТО известно из источника и ЧТО действительно вычислено, и эти три вещи различаются явной пометкой.

Ссылаются нормы: Interpretation, LogicModel, Provenance

ru · official · sha256:14745477bba0f744b15955aef0ebb7facc17571b84ff2e7a20e7a4fcd6acad00

Раздел 15. Обоснование. Обоснованием шага называется указание на то, чем шаг оправдан: правилом исчисления, определением понятия, принципом системы либо ссылкой на утверждение источника. Обоснование не есть доказательство: пакет сохраняет обоснование шага и его происхождение, а доказательство теоремы остаётся в источнике.

Ссылаются нормы: GroundIsConcept, GroundIsPrinciple, GroundIsRule, SourceOfItself, answer_source, stated_by, step_ground, step_needs_principle, step_uses_concept, step_uses_rule

ru · official · sha256:e224483f95955254054ddbe7fe5f38f802ee8539b518d3325dd36c50e59d5a88

Раздел 16. Предъявленный ход рассуждения. Предъявленным ходом рассуждения называется конкретная последовательность применений правил, поданная делом. Она не принадлежит ни методу, ни исчислению: метод описывает, как рассуждать, исчисление — чем, а ход рассуждения есть данные дела. Настоящее семейство пакетов ПОКАЗЫВАЕТ способ рассуждения и не производит поиска вывода: универсального поиска доказательств здесь нет и не предполагается.

Ссылаются нормы: Reasoning, RuleAppliedInReasoning, ShownConclusionFromPresentedStep, presented_step, rule_applied_in, shown_conclusion

ru · official · sha256:546fad1859a1427962dd485b0f2b99a5257d4e20c175f37f8ea317aa6676730b

Раздел 17. Связи между понятиями. Понятия соединяются связями с РАЗЛИЧНЫМ смыслом, и одна неразличимая связь «связано с» здесь запрещена. Различаются: использует; определяется через; имеет посылку; имеет заключение; содержит шаг; требует условие; снимает допущение; представляет систему; отличается принципом; принадлежит исчислению; обосновано источником. Каждая связь имеет свои типы аргументов и свой смысл, названный в настоящем разделе.

Ссылаются нормы: Concept, WhatIs, answer_part, answer_what_is, defined_via, gloss, item_key, term_name, uses

ru · official · sha256:01880531a6200f85757fe68895fd9bf5748038bb5b73ee3673f7e67ba32a07ad

Раздел 18. Раскрытие объяснения. Раскрытием называется обход связей от предъявленного понятия к тем, через которые оно объяснено, и далее до листьев. Обход обязан быть конечным при наличии взаимных ссылок и не обязан молча обрываться: достижимость вычисляется замыканием, а недостижимость источника называется отдельно. Понятие считается доведённым до источника, если у него самого либо у достижимого из него понятия есть ссылка на закреплённый фрагмент.

Ссылаются нормы: ExplainsByCalculus, ExplainsByConclusion, ExplainsByCondition, ExplainsByDefinition, ExplainsByDischarge, ExplainsByDischargedForm, ExplainsByGoal, ExplainsByGround, ExplainsByOpenedContext, ExplainsByPart, ExplainsByPremise, ExplainsByRuleOfCalculus, ExplainsBySlot, ExplainsByStep, ExplainsByUse, GroundedDirectly, GroundedThroughUnfolding, ProvenanceFromLocator, ReachCount, ReachesDirect, ReachesTransitive, SourceThroughUnfolding, explains, grounded_in_source, has_provenance, reach_count, reaches

ru · official · sha256:152a0d8561a87bfa42ce18cd49fbe4bf17e2c36b5cbaf4fd9979d9ee75da44e5

Раздел 19. Граница описания. Настоящее семейство пакетов описывает знание о логиках и способах их применения. Оно не проверяет доказательства, не строит модели, не перебирает бесконечные носители и не доказывает заново теорем своих источников. Утверждение источника представляется как утверждение источника — с условиями и ссылкой, — а не как результат вычисления; вычисленным называется только то, что действительно вычислено движком на предъявленных данных.

Ссылаются нормы: GradeOfKnowledge, SourceClaimNeedsLocator, answer_grade, knowledge_grade, source_claim