Логика знания о знании: автоэпистемический подход.

Введение

Рассуждения о знании о знании
Автоэпистемическая логика — это формальная логика для представления и рассуждений о знании о знании. В то время как пропозициональная логика может выражать только факты, автоэпистемическая логика может выражать знание и незнание фактов. Семантика стабильных моделей, используемая для определения семантики логического программирования с отрицанием как отказом, может рассматриваться как упрощенная форма автоэпистемической логики.

Синтаксис

Синтаксис автоэпистемической логики расширяет синтаксис пропозициональной логики модальным оператором, обозначающим знание: если φ – формула, то Kφ означает, что φ известно. Следовательно, Kφ означает, что φ известно, а ¬Kφ означает, что φ не известно. Этот синтаксис используется для обеспечения рассуждений, основанных на знании фактов. Например, ¬Kφ означает, что φ считается ложным, если не известно, что оно истинно. Это одна из форм отрицания как отказа (или отрицания как неудачи).

Семантика

Семантика автоэпистемической логики основана на расширениях теории, которые играют роль, аналогичную моделям в пропозициональной логике. В то время как пропозициональная модель определяет, какие атомарные пропозиции истинны или ложны, расширение определяет, какие формулы истинны, а какие ложны. В частности, расширения автоэпистемической формулы делают такое определение для каждой подформулы, содержащейся в ней. Это позволяет рассматривать ее как пропозициональную формулу, поскольку все ее подформулы, содержащие , либо истинны, либо ложны. В частности, проверка того, следует ли из в этом случае, может быть выполнена с использованием правил пропозиционального исчисления. Чтобы спецификация являлась расширением, необходимо и достаточно, чтобы подформула следовала из тогда и только тогда, когда присвоено значение «истина». С точки зрения семантики возможных миров, расширение состоит из S5-модели , в которой возможные миры состоят только из миров, где истинно. [Возможные миры не обязаны содержать все такие непротиворечивые миры; это соответствует тому факту, что модальным пропозициям присваиваются значения истинности перед проверкой выводимости обычных пропозиций.] Таким образом, автоэпистемическая логика расширяет S5; это расширение является собственным, поскольку и являются тавтологиями автоэпистемической логики, но не S5. Например, в формуле существует только одна “подформула с модальным оператором”, которая является . Следовательно, существует только два кандидата в расширения, предполагая, что истинно или ложно, соответственно. Проверка того, являются ли они фактическими расширениями, выглядит следующим образом. Ложно: с этим предположением становится тавтологией, поскольку эквивалентно , а предполагается истинным; следовательно, не следует. Этот результат подтверждает предположение, что ложно, то есть, что в настоящее время не известно. Поэтому предположение, что ложно, является расширением. Истинно: вместе с этим предположением влечет за собой ; следовательно, исходное предположение, подразумеваемое тем, что истинно, то есть, что известно как истинное, удовлетворено. В результате, это еще одно расширение. Таким образом, формула имеет два расширения, одно из которых неизвестно, а другое – известно. Второе считается неинтуитивным, поскольку первоначальное предположение, что истинно, является единственной причиной, по которой истинно, что подтверждает предположение. Иными словами, это самоподдерживающее предположение. Логика, допускающая такую самоподдержку убеждений, называется нестрого обоснованной, чтобы отличать ее от строго обоснованных логик, в которых самоподдержка невозможна. Существуют строго обоснованные варианты автоэпистемической логики.

The semantics of autoepistemic logic is based on the expansions of a theory, which have a role similar to models in propositional logic. While a propositional model specifies which atomic propositions are true or false, an expansion specifies which formulae are true and which ones are false. In particular, the expansions of an autoepistemic formula make this determination for every subformula contained in This determination allows to be treated as a propositional formula, as all its subformulae containing are either true or false. In particular, checking whether entails in this condition can be done using the rules of the propositional calculus. In order for a specification to be an expansion, it must be that a subformula is entailed if and only if has been assigned the value true. In terms of possible world semantics, an expansion of consists of an S5 model of in which the possible worlds consist only of worlds where is true. [The possible worlds need not contain all such consistent worlds; this corresponds to the fact that modal propositions are assigned truth values before checking derivability of the ordinary propositions.] Thus, autoepistemic logic extends S5; the extension is proper, since and are tautologies of autoepistemic logic, but not of S5. For example, in the formula , there is only a single “boxed subformula”, which is Therefore, there are only two candidate expansions, assuming is true or false, respectively. The check for them being actual expansions is as follows. is false : with this assumption, becomes tautological, as is equivalent to , and is assumed true; therefore, is not entailed. This result confirms the assumption implicit in being false, that is, that is not currently known. Therefore, the assumption that is false is an expansion. is true : together with this assumption, entails ; therefore, the initial assumption that is implicit in being true, i. e., that is known to be true, is satisfied. As a result, this is another expansion. The formula has therefore two expansions, one in which is not known and one in which is known. The second one has been regarded as unintuitive, as the initial assumption that is true is the only reason why is true, which confirms the assumption. In other words, this is a self supporting assumption. A logic allowing such a self support of beliefs is called not strongly grounded to differentiate them from strongly grounded logics, in which self support is not possible. Strongly grounded variants of autoepistemic logic exist.

Обобщения

При неопределённом выводе двойственность «истинно/ложно» заменяется степенью достоверности факта или вывода; достоверность может меняться от 0 (полностью недостоверно/неизвестно) до 1 (достоверно/известно). В вероятностных логических сетях истинные значения также получают вероятностную интерпретацию (то есть истинные значения могут быть неопределёнными, и даже если они почти достоверны, они всё равно могут быть «вероятно» истинными (или ложными).)