Алгебра логики высказываний Основные понятия

Исчисление высказываний

• 
  Алфавит (совокупность используемых символов);
  
• 
  Синтаксические правила построения формул в алфавите;
  
• 
  Аксиомы (общезначимые формулы или тождественно истинные формулы);
  
• 
  Правила вывода по аксиомам производных формул или теорем.
  

Классическое исчисление высказываний

1. 
   α  (  α),
   
2. 
   (α  (  γ))  (( α  )  (α  γ)),
   
3. 
   (α  )  α,
   
4. 
   (α  )  ,
   
5. 
   α  (α  ),
   
6. 
     (α  ),
   
7. 
   (α  )  ((α  γ)  (α  (  γ)),
   
8. 
   (α  γ)  ((  γ)  ((α  )  γ)),
   
9. 
   (α  )  (  α),
   
10. 
    α  α,
    
11. 
    α  α.
    

• 
  Modus ponens. Из истинности условия импликации и истинности самой импликации следует истинность следствия импликации: α, α├ .
  
• 
  Правило одновременной подстановки. Из формулы α(р), где р – переменная, выводима формула α(R), где R – формула, получаемая заменой в α(р) каждого вхождения переменной р на формулу R: α (р) ├ α (R). В общем случае будем обозначать подстановку (x₁,…, x_n  α₁,…, α_n).
  

Натуральное исчисление высказываний

• 
  Исключение конъюнкта. Из истинности конъюнкции следует истинность любого ее конъюнкта:
  

• 
  Введение конъюнкции. Из списка истинных формул следует истинность их конъюнкции:
  

• 
  Введение дизъюнкции. Из истинности формулы следует истинность ее дизъюнкции с любыми другими формулами:
  

• 
  Исключение двойного отрицания. Из истинности двойного отрицания формулы следует истинность ее самой:
  

• 
  Простая резолюция (удаление дизъюнкта). Из истинности дизъюнкции и отрицания одного из ее дизъюнктов следует истинность формулы после удаления этого дизъюнкта:
  

• 
  Резолюция. Из истинности двух дизъюнкций, одна из которых содержит дизъюнкт, а другая его отрицание следует формула, являющаяся дизъюнкцией исходных формул после удаления этого дизъюнкта:
  

Понятие выводимости

1. 
   либо B H,
   
2. 
   либо B – доказуемая формула исчисления высказываний,
   
3. 
   либо B получается по правилу Modus ponens из формул C и C  B, которые выводимы из совокупности H.
   

Примеры

1. 
   Возьмем аксиому (α  γ)  ((  γ)  ((α  )  γ)) и сделаем в ней подстановку (α, γ,   A, A, A). Получим: (A  A)  ((A  A)  ((A  A)  A));
   
2. 
   Докажем выводимость A  A:
   
   1. 
      Возьмем аксиому (α  (  γ))  (( α  )  (α  γ)) и сделаем в ней подстановку (α, γ,   x, y, x). Получим: (x  (y  x))  ((x  y)  (x  x));
      
   2. 
      Из аксиомы x  (y  x) и правила Modus ponens имеем: (x  y)  (x  x);
      
   3. 
      Выполним подстановку (y  x). Получим: (x  x)  (x  x);
      
   4. 
      Из аксиомы x  x и правила Modus ponens имеем: x  x;
      
3. 
   Из формулы x  x и правила Modus ponens имеем: (A  A)  ((A  A)  A);
   
4. 
   Аналогично: (A  A)  A;