Метаязык логики высказываний и переход от импликативной формы к высказываниям на метаязыке

Язык логики высказываний называют объектным, a метаязык исследователя –субъектным. В соответствии с этим различают символы, применяемые в высказываниях: ~-объектный символ эквивалентности

=- субъектный символ эквивалентности

Λ- объектный символ конъюнкции

,- субъектный символ конъюнкции

V- объектный символ дизъюнкции

;- субъектный символ дизъюнкции

- объектный символ импликации

- субъектный символ импликации

Тогда утверждение, которое надо доказать в логике высказываний, оформляется в виде причинно-следственных отношения

P1,P2,…P(N-1),PN=>C (1.1)

Pi, i=1,N-посылки

С- заключение или следствие

Словами это выражается: если посылки P1,…,PN – истинны, то заключение Р также истинно.

Предложение 1.1 называется клаузой – метапредложение, в котором используется отношение порядка, оформленное с помощью символа метаимпликации (=>) также как и отношение эквивалентности, отношение порядка удовлетворяет трем условиям: 1.Закон рефлексивности А=>А; 2. Закон симметричности: если А=>В то В=>А; 3. Закон транзитивности: если А=>В и В=>С то А=>С(если

А=>В и А=>В то А=В).Клауза это формальная запись доказываемого предложения. Если вместо букв в него подставить объектные высказывания, то клауза наполняется конкретным содержанием, которое называется семантикое(легендой).

Пример клаузы: А→В, А=> В

А-«сверкнула молния», В-«грянул гром»

В-«грянул гром» - тогда данная клауза отображает следующую легенду. Известно, что если сверкнула молния, то после этого грянет гром. Молния сверкнула => грянул гром. Над субъектом, который формулирует предложение может находиться другой субъект, для которого предложение 1 будет являться объектом

(P1ΛP2Λ…ΛPn-1ΛPn)→C

P1vP2v…vPn-1vPnvC

Отсюда находим, что (P1ΛP2Λ…ΛPn-1) →(PnvC), клауза 2.1 может быть представлена в др. эквивалентной форме P1,P2,…,Pn-1=>Pn;C (2.2)

P1,P2,P3,P4=>C1;C2;C3; можно преобразовать к виду Р4,С2,Р1,С1=> Р3;C3;P2 (2.3) => через метод компликации клаузы типа 2.1 назыв. Хорновской используют в ПРОЛОГе – языке программирования.

Пусть дано выражение в импликативной форме AvB→C на мета языке: A,B;C

A	B	C			A	B

Λ= “,”

V= “;”