Исчисление высказываний Фреге - Frege's propositional calculus
В математической логике , исчисление Фреге было первой аксиоматизацией в исчислении высказываний . Он был изобретен Готлобом Фреге , который также изобрел исчисление предикатов , в 1879 году как часть своего исчисления предикатов второго порядка (хотя Чарльз Пирс был первым, кто использовал термин «второй порядок» и независимо разработал свою собственную версию исчисления предикатов. Фреге).
Он использует всего два логических оператора: импликацию и отрицание, и состоит из шести аксиом и одного правила вывода : modus ponens .
| Аксиомы | Правило вывода |
|---|---|
|
|
Исчисление высказываний Фреге эквивалентно любому другому классическому исчислению высказываний, например, «стандартному ПК» с 11 аксиомами. ПК Фреге и стандартный ПК разделяют две общие аксиомы: ТОГДА-1 и ТОГДА-2. Обратите внимание, что аксиомы с THEN-1 по THEN-3 используют (и определяют) только оператор импликации, тогда как аксиомы FRG-1 по FRG-3 определяют оператор отрицания.
Следующие теоремы будут стремиться найти оставшиеся девять аксиом стандартного ПК в «пространстве теорем» ПК Фреге, показывая, что теория стандартного ПК содержится в теории ПК Фреге.
(Теория, также называемая здесь в переносных целях «пространством теорем», представляет собой набор теорем, которые являются подмножеством универсального набора правильно сформированных формул . Теоремы связаны друг с другом направленным образом посредством правила вывода , образующие своего рода дендритную сеть. В основе пространства теорем находятся аксиомы, которые «порождают» пространство теорем во многом так же, как порождающее множество порождает группу.)
Правила
Правило ( ТО-1 ) - A A B → A
| # | wff | причина |
|---|---|---|
| 1. | А | посылка |
| 2. | А → (В → А) | ТО-1 |
| 3. | Б → А | МП 1,2. |
Правило ( ТО-2 ) - A → (B → C) ⊢ (A → B) → (A → C)
| # | wff | причина |
|---|---|---|
| 1. | А → (В → С) | посылка |
| 2. | (A → (B → C)) → ((A → B) → (A → C)) | ТО-2 |
| 3. | (А → В) → (А → С) | МП 1,2. |
Правило ( ТО-3 ) - A → (B → C) ⊢ B → (A → C)
| # | wff | причина |
|---|---|---|
| 1. | А → (В → С) | посылка |
| 2. | (A → (B → C)) → (B → (A → C)) | ТО-3 |
| 3. | В → (А → С) | МП 1,2. |
Правило ( ФРГ-1 ) - А → В ⊢ ¬B → ¬A
| # | wff | причина |
|---|---|---|
| 1. | (A → B) → (¬B → ¬A) | ФРГ-1 |
| 2. | А → Б | посылка |
| 3. | ¬B → ¬A | МП 2,1. |
Правило ( TH1 ) - A → B, B → C ⊢ A → C
| # | wff | причина |
|---|---|---|
| 1. | B → C | посылка |
| 2. | (B → C) → (A → (B → C)) | ТО-1 |
| 3. | А → (В → С) | МП 1,2 |
| 4. | (A → (B → C)) → ((A → B) → (A → C)) | ТО-2 |
| 5. | (А → В) → (А → С) | MP 3,4 |
| 6. | А → Б | посылка |
| 7. | А → С | МП 6,5. |
Теоремы
Теорема ( TH1 ) - (A → B) → ((B → C) → (A → C))
| # | wff | причина |
|---|---|---|
| 1. | (B → C) → (A → (B → C)) | ТО-1 |
| 2. | (A → (B → C)) → ((A → B) → (A → C)) | ТО-2 |
| 3. | (B → C) → ((A → B) → (A → C)) | TH1 * 1,2 |
| 4. | ((B → C) → ((A → B) → (A → C))) → ((A → B) → ((B → C) → (A → C))) | ТО-3 |
| 5. | (A → B) → ((B → C) → (A → C)) | МП 3,4. |
Теорема ( TH2 ) - А → (¬A → ¬B)
| # | wff | причина |
|---|---|---|
| 1. | А → (В → А) | ТО-1 |
| 2. | (B → A) → (¬A → ¬B) | ФРГ-1 |
| 3. | А → (¬A → ¬B) | TH1 * 1,2. |
Теорема ( TH3 ) - ¬A → (A → ¬B)
| # | wff | причина |
|---|---|---|
| 1. | А → (¬A → ¬B) | TH 2 |
| 2. | (A → (¬A → ¬B)) → (¬A → (A → ¬B)) | ТО-3 |
| 3. | ¬A → (A → ¬B) | МП 1,2. |
Теорема ( TH4 ) - ¬ (А → ¬B) → А
| # | wff | причина |
|---|---|---|
| 1. | ¬A → (A → ¬B) | TH3 |
| 2. | (¬A → (A → ¬B)) → (¬ (A → ¬B) → ¬¬A) | ФРГ-1 |
| 3. | ¬ (А → ¬B) → ¬¬A | МП 1,2 |
| 4. | ¬¬A → А | ФРГ-2 |
| 5. | ¬ (А → ¬B) → А | TH1 * 3,4. |
Теорема ( TH5 ) - (A → ¬B) → (B → ¬A)
| # | wff | причина |
|---|---|---|
| 1. | (А → ¬B) → (¬¬B → ¬A) | ФРГ-1 |
| 2. | ((A → ¬B) → (¬¬B → ¬A)) → (¬¬B → ((A → ¬B) → ¬A)) | ТО-3 |
| 3. | ¬¬B → ((A → ¬B) → ¬A) | МП 1,2 |
| 4. | B → ¬¬B | ФРГ-3, с A: = B |
| 5. | B → ((A → ¬B) → ¬A) | TH1 * 4,3 |
| 6. | (B → ((A → ¬B) → ¬A)) → ((A → ¬B) → (B → ¬A)) | ТО-3 |
| 7. | (A → ¬B) → (B → ¬A) | МП 5,6. |
Теорема ( TH6 ) - ¬ (A → ¬B) → B
| # | wff | причина |
|---|---|---|
| 1. | ¬ (B → ¬A) → B | TH4, где A: = B, B: = A |
| 2. | (B → ¬A) → (A → ¬B) | TH5, где A: = B, B: = A |
| 3. | ((B → ¬A) → (A → ¬B)) → (¬ (A → ¬B) → ¬ (B → ¬A)) | ФРГ-1 |
| 4. | ¬ (A → ¬B) → ¬ (B → ¬A) | MP 2,3 |
| 5. | ¬ (A → ¬B) → B | TH1 * 4,1. |
Теорема ( TH7 ) - А → А
| # | wff | причина |
|---|---|---|
| 1. | А → ¬¬A | ФРГ-3 |
| 2. | ¬¬A → А | ФРГ-2 |
| 3. | А → А | TH1 * 1,2. |
Теорема ( TH8 ) - А → ((А → В) → В)
| # | wff | причина |
|---|---|---|
| 1. | (А → В) → (А → В) | TH7, где A: = A → B |
| 2. | ((A → B) → (A → B)) → (A → ((A → B) → B)) | ТО-3 |
| 3. | А → ((А → В) → Б) | МП 1,2. |
Теорема ( TH9 ) - B → ((A → B) → B)
| # | wff | причина |
|---|---|---|
| 1. | Б → ((А → В) → Б) | ТО-1, где A: = B, B: = A → B. |
Теорема ( TH10 ) - A → (B → ¬ (A → ¬B))
| # | wff | причина |
|---|---|---|
| 1. | (A → ¬B) → (A → ¬B) | TH7 |
| 2. | ((A → ¬B) → (A → ¬B)) → (A → ((A → ¬B) → ¬B) | ТО-3 |
| 3. | А → ((А → ¬B) → ¬B) | МП 1,2 |
| 4. | ((A → ¬B) → ¬B) → (B → ¬ (A → ¬B)) | TH5 |
| 5. | A → (B → ¬ (A → ¬B)) | TH1 * 3,4. |
Примечание: ¬ (A → ¬B) → A (TH4), ¬ (A → ¬B) → B (TH6) и A → (B → ¬ (A → ¬B)) (TH10), поэтому ¬ (A → ¬B) ведет себя так же, как A∧B (сравните с аксиомами AND-1, AND-2 и AND-3).
Теорема ( TH11 ) - (A → B) → ((A → ¬B) → ¬A)
| # | wff | причина |
|---|---|---|
| 1. | A → (B → ¬ (A → ¬B)) | TH10 |
| 2. | (A → (B → ¬ (A → ¬B))) → ((A → B) → (A → ¬ (A → ¬B))) | ТО-2 |
| 3. | (A → B) → (A → ¬ (A → ¬B)) | МП 1,2 |
| 4. | (A → ¬ (A → ¬B)) → ((A → ¬B) → ¬A) | TH5 |
| 5. | (A → B) → ((A → ¬B) → ¬A) | TH1 * 3,4. |
TH11 - это аксиома НЕ-1 стандартного ПК, называемая « reductio ad absurdum ».
Теорема ( TH12 ) - ((A → B) → C) → (A → (B → C))
| # | wff | причина |
|---|---|---|
| 1. | В → (А → В) | ТО-1 |
| 2. | (B → (A → B)) → (((A → B) → C) → (B → C)) | TH1 |
| 3. | ((A → B) → C) → (B → C) | МП 1,2 |
| 4. | (B → C) → (A → (B → C)) | ТО-1 |
| 5. | ((A → B) → C) → (A → (B → C)) | TH1 * 3,4. |
Теорема ( TH13 ) - (B → (B → C)) → (B → C)
| # | wff | причина |
|---|---|---|
| 1. | (B → (B → C)) → ((B → B) → (B → C)) | ТО-2 |
| 2. | (B → B) → ((B → (B → C)) → (B → C)) | ТО-3 * 1 |
| 3. | B → B | TH7 |
| 4. | (B → (B → C)) → (B → C) | МП 3,2. |
Правило ( TH14 ) - A → (B → P), P → Q ⊢ A → (B → Q)
| # | wff | причина |
|---|---|---|
| 1. | P → Q | посылка |
| 2. | (P → Q) → (B → (P → Q)) | ТО-1 |
| 3. | B → (P → Q) | МП 1,2 |
| 4. | (B → (P → Q)) → ((B → P) → (B → Q)) | ТО-2 |
| 5. | (B → P) → (B → Q) | MP 3,4 |
| 6. | ((B → P) → (B → Q)) → (A → ((B → P) → (B → Q))) | ТО-1 |
| 7. | A → ((B → P) → (B → Q)) | MP 5,6 |
| 8. | (A → (B → P)) → (A → (B → Q)) | ТОГДА-2 * 7 |
| 9. | А → (В → П) | посылка |
| 10. | А → (В → Q) | МП 9,8. |
Теорема ( TH15 ) - ((A → B) → (A → C)) → (A → (B → C))
| # | wff | причина |
|---|---|---|
| 1. | ((A → B) → (A → C)) → (((A → B) → A) → ((A → B) → C)) | ТО-2 |
| 2. | ((A → B) → C) → (A → (B → C)) | TH12 |
| 3. | ((A → B) → (A → C)) → (((A → B) → A) → (A → (B → C))) | TH14 * 1,2 |
| 4. | ((A → B) → A) → (((A → B) → (A → C)) → (A → (B → C))) | ТО-3 * 3 |
| 5. | А → ((А → В) → А) | ТО-1 |
| 6. | A → (((A → B) → (A → C)) → (A → (B → C))) | TH1 * 5,4 |
| 7. | ((A → B) → (A → C)) → (A → (A → (B → C))) | ТО-3 * 6 |
| 8. | (A → (A → (B → C))) → (A → (B → C)) | TH13 |
| 9. | ((A → B) → (A → C)) → (A → (B → C)) | TH1 * 7,8. |
Теорема TH15 является обратной аксиомой ТО-2.
Теорема ( TH16 ) - (¬A → ¬B) → (B → A)
| # | wff | причина |
|---|---|---|
| 1. | (¬A → ¬B) → (¬¬B → ¬¬A) | ФРГ-1 |
| 2. | ¬¬B → ((¬A → ¬B) → ¬¬A) | ТО-3 * 1 |
| 3. | B → ¬¬B | ФРГ-3 |
| 4. | В → ((¬A → ¬B) → ¬¬A) | TH1 * 3,2 |
| 5. | (¬A → ¬B) → (B → ¬¬A) | ТО-3 * 4 |
| 6. | ¬¬A → А | ФРГ-2 |
| 7. | (¬¬A → A) → (B → (¬¬A → A)) | ТО-1 |
| 8. | Б → (¬¬A → А) | МП 6,7 |
| 9. | (B → (¬¬A → A)) → ((B → ¬¬A) → (B → A)) | ТО-2 |
| 10. | (B → ¬¬A) → (B → A) | MP 8,9 |
| 11. | (¬A → ¬B) → (B → A) | TH1 * 5,10. |
Теорема ( TH17 ) - (¬A → B) → (¬B → A)
| # | wff | причина |
|---|---|---|
| 1. | (¬A → ¬¬B) → (¬B → A) | TH16, с B: = ¬B |
| 2. | B → ¬¬B | ФРГ-3 |
| 3. | (B → ¬¬B) → (¬A → (B → ¬¬B)) | ТО-1 |
| 4. | ¬A → (B → ¬¬B) | MP 2,3 |
| 5. | (¬A → (B → ¬¬B)) → ((¬A → B) → (¬A → ¬¬B)) | ТО-2 |
| 6. | (¬A → B) → (¬A → ¬¬B) | MP 4,5 |
| 7. | (¬A → B) → (¬B → A) | TH1 * 6,1. |
Сравните TH17 с теоремой TH5.
Теорема ( TH18 ) - ((A → B) → B) → (¬A → B)
| # | wff | причина |
|---|---|---|
| 1. | (A → B) → (¬B → (A → B)) | ТО-1 |
| 2. | (¬B → ¬A) → (A → B) | TH16 |
| 3. | (¬B → ¬A) → (¬B → (A → B)) | TH1 * 2,1 |
| 4. | ((¬B → ¬A) → (¬B → (A → B))) → (¬B → (¬A → (A → B))) | TH15 |
| 5. | ¬B → (¬A → (A → B)) | MP 3,4 |
| 6. | (¬A → (A → B)) → (¬ (A → B) → A) | TH17 |
| 7. | ¬B → (¬ (A → B) → A) | TH1 * 5,6 |
| 8. | (¬B → (¬ (A → B) → A)) → ((¬B → ¬ (A → B)) → (¬B → A)) | ТО-2 |
| 9. | (¬B → ¬ (A → B)) → (¬B → A) | MP 7,8 |
| 10. | ((A → B) → B) → (¬B → ¬ (A → B)) | ФРГ-1 |
| 11. | ((A → B) → B) → (¬B → A) | TH1 * 10,9 |
| 12. | (¬B → A) → (¬A → B) | TH17 |
| 13. | ((A → B) → B) → (¬A → B) | TH1 * 11,12. |
Теорема ( TH19 ) - (A → C) → ((B → C) → (((A → B) → B) → C))
| # | wff | причина |
|---|---|---|
| 1. | ¬A → (¬B → ¬ (¬A → ¬¬B)) | TH10 |
| 2. | B → ¬¬B | ФРГ-3 |
| 3. | (B → ¬¬B) → (¬A → (B → ¬¬B)) | ТО-1 |
| 4. | ¬A → (B → ¬¬B) | MP 2,3 |
| 5. | (¬A → (B → ¬¬B)) → ((¬A → B) → (¬A → ¬¬B)) | ТО-2 |
| 6. | (¬A → B) → (¬A → ¬¬B) | MP 4,5 |
| 7. | ¬ (¬A → ¬¬B) → ¬ (¬A → B) | ФРГ-1 * 6 |
| 8. | ¬A → (¬B → ¬ (¬A → B)) | TH14 * 1,7 |
| 9. | ((A → B) → B) → (¬A → B) | TH18 |
| 10. | ¬ (¬A → B) → ¬ ((A → B) → B) | ФРГ-1 * 9 |
| 11. | ¬A → (¬B → ¬ ((A → B) → B)) | TH14 * 8,10 |
| 12. | ¬C → (¬A → (¬B → ¬ ((A → B) → B))) | ТО-1 * 11 |
| 13. | (¬C → ¬A) → (¬C → (¬B → ¬ ((A → B) → B))) | ТО-2 * 12 |
| 14. | (¬C → (¬B → ¬ ((A → B) → B))) → ((¬C → ¬B) → (¬C → ¬ ((A → B) → B))) | ТО-2 |
| 15. | (¬C → ¬A) → ((¬C → ¬B) → (¬C → ¬ ((A → B) → B))) | TH1 * 13,14 |
| 16. | (A → C) → (¬C → ¬A) | ФРГ-1 |
| 17. | (A → C) → ((→ C → ¬B) → (¬C → ¬ ((A → B) → B))) | TH1 * 16,15 |
| 18. | (¬C → ¬ ((A → B) → B)) → (((A → B) → B) → C) | TH16 |
| 19. | (A → C) → ((¬C → ¬B) → (((A → B) → B) → C)) | TH14 * 17,18 |
| 20. | (B → C) → (¬C → ¬B) | ФРГ-1 |
| 21. | ((B → C) → (¬C → ¬B)) → (((¬C → ¬B) → (((A → B) → B) → C)) → ((B → C) → (((A → B) → B) → C))) |
TH1 |
| 22. | ((¬C → ¬B) → (((A → B) → B) → C)) → ((B → C) → (((A → B) → B) → C)) | MP 20,21 |
| 23. | (A → C) → ((B → C) → (((A → B) → B) → C)) | TH1 * 19,22. |
Примечание: A → ((A → B) → B) (TH8), B → ((A → B) → B) (TH9) и (A → C) → ((B → C) → (((A → B) → B) → C)) (TH19), поэтому ((A → B) → B) ведет себя так же, как A∨B. (Сравните с аксиомами OR-1, OR-2 и OR-3.)
Теорема ( TH20 ) - (А → ¬A) → ¬A
| # | wff | причина |
|---|---|---|
| 1. | (A → A) → ((A → ¬A) → ¬A) | TH11 |
| 2. | А → А | TH7 |
| 3. | (А → ¬A) → ¬A | МП 2,1. |
TH20 соответствует аксиоме NOT-3 стандартного ПК, называемой " tertium non datur ".
Теорема ( TH21 ) - А → (¬A → В)
| # | wff | причина |
|---|---|---|
| 1. | А → (¬A → ¬¬B) | TH2, где B: = ~ B |
| 2. | ¬¬B → B | ФРГ-2 |
| 3. | А → (¬A → В) | TH14 * 1,2. |
TH21 соответствует аксиоме NOT-2 стандартного ПК, называемой " ex contraissione quodlibet ".
Все аксиомы стандартного ПК были взяты из ПК Фреге после того, как
Правило ( 1 доллар ) - 2 доллара
A∧B: = ¬ (A → ¬B) и A∨B: = (A → B) → B. Эти выражения не уникальны, например, A∨B также можно было определить как (B → A) → A, ¬A → B или ¬B → A. Однако обратите внимание, что определение A∨B: = (A → B) → B не содержит отрицаний. С другой стороны, A∧B нельзя определить только с точки зрения импликации без использования отрицания.
В некотором смысле выражения A∧B и A∨B можно рассматривать как «черные ящики». Внутри эти черные ящики содержат формулы, состоящие только из импликации и отрицания. Черные ящики могут содержать что угодно, если они подключены к аксиомам от AND-1 до AND-3 и OR-1 до OR-3 стандартного ПК, эти аксиомы остаются верными. Эти аксиомы предоставляют полные синтаксические определения операторов конъюнкции и дизъюнкции .
Следующий набор теорем будет направлен на поиск оставшихся четырех аксиом ПК Фреге в «пространстве теорем» стандартного ПК, показывая, что теория ПК Фреге содержится в теории стандартного ПК.
Теорема ( ST1 ) - А → А
| # | wff | причина |
|---|---|---|
| 1. | (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) | ТО-2 |
| 2. | А → ((А → А) → А) | ТО-1 |
| 3. | (А → (А → А)) → (А → А) | MP 2,1 |
| 4. | А → (А → А) | ТО-1 |
| 5. | А → А | МП 4,3. |
Теорема ( ST2 ) - А → ¬¬A
| # | wff | причина |
|---|---|---|
| 1. | А | гипотеза |
| 2. | А → (¬A → А) | ТО-1 |
| 3. | ¬A → А | МП 1,2 |
| 4. | ¬A → ¬A | ST1 |
| 5. | (¬A → A) → ((¬A → ¬A) → ¬¬A) | НЕ-1 |
| 6. | (¬A → ¬A) → ¬¬A | MP 3,5 |
| 7. | ¬¬A | MP 4,6 |
| 8. | А ⊢ ¬¬A | резюме 1-7 |
| 9. | А → ¬¬A | ДТ 8. |
ST2 - аксиома FRG-3 ПК Фреге.
Теорема ( ST3 ) - B∨C → (¬C → B)
| # | wff | причина |
|---|---|---|
| 1. | С → (¬C → В) | НЕ-2 |
| 2. | B → (¬C → B) | ТО-1 |
| 3. | (B → (¬C → B)) → ((C → (¬C → B)) → ((B ∨ C) → (¬C → B))) | ИЛИ-3 |
| 4. | (C → (¬C → B)) → ((B ∨ C) → (¬C → B)) | MP 2,3 |
| 5. | B∨C → (¬C → B) | МП 1,4. |
Теорема ( ST4 ) - ¬¬A → А
| # | wff | причина |
|---|---|---|
| 1. | A∨¬A | НЕ-3 |
| 2. | (A∨¬A) → (¬¬A → A) | ST3 |
| 3. | ¬¬A → А | МП 1,2. |
ST4 - аксиома FRG-2 ПК Фреге.
Докажите ST5: (A → (B → C)) → (B → (A → C))
| # | wff | причина |
|---|---|---|
| 1. | А → (В → С) | гипотеза |
| 2. | B | гипотеза |
| 3. | А | гипотеза |
| 4. | B → C | MP 3,1 |
| 5. | C | МП 2,4 |
| 6. | А → (В → С), В, А ⊢ С | резюме 1-5 |
| 7. | А → (В → С), В ⊢ А → С | DT 6 |
| 8. | A → (B → C) ⊢ B → (A → C) | DT 7 |
| 9. | (A → (B → C)) → (B → (A → C)) | ДТ 8. |
ST5 - это аксиома THEN-3 ПК Фреге.
Теорема ( ST6 ) - (A → B) → (¬B → ¬A)
| # | wff | причина |
|---|---|---|
| 1. | А → Б | гипотеза |
| 2. | ¬B | гипотеза |
| 3. | ¬B → (A → ¬B) | ТО-1 |
| 4. | А → ¬B | MP 2,3 |
| 5. | (A → B) → ((A → ¬B) → ¬A) | НЕ-1 |
| 6. | (А → ¬B) → ¬A | MP 1,5 |
| 7. | ¬A | MP 4,6 |
| 8. | А → В, ¬B ⊢ ¬A | резюме 1-7 |
| 9. | А → В ⊢ ¬B → ¬A | DT 8 |
| 10. | (A → B) → (¬B → ¬A) | DT 9. |
ST6 - аксиома FRG-1 ПК Фреге.
Каждую из аксиом Фреге можно вывести из стандартных аксиом, и каждую из стандартных аксиом можно вывести из аксиом Фреге. Это означает, что два набора аксиом взаимозависимы, и в одном наборе нет аксиомы, независимой от другого набора. Следовательно, эти два набора аксиом порождают одну и ту же теорию: ПК Фреге эквивалентен стандартному ПК.
(Ведь если теории должны быть разными, то одна из них должна содержать теоремы, не содержащиеся в другой теории. Эти теоремы могут быть выведены из набора аксиом их собственной теории: но, как было показано, весь этот набор аксиом может быть получен из другой набор аксиом теории, что означает, что данные теоремы могут быть фактически получены исключительно из набора аксиом другой теории, так что данные теоремы также принадлежат другой теории.Противоречие: таким образом, два набора аксиом охватывают одно и то же пространство теорем. : Любая теорема, полученная из стандартных аксиом, может быть выведена из аксиом Фреге, и наоборот, сначала доказывая как теоремы аксиомы другой теории, как показано выше, а затем используя эти теоремы как леммы для вывода желаемой теоремы.)
Смотрите также
Рекомендации
- Басс, Сэмюэл (1998). «Введение в теорию доказательств» (PDF) . Справочник по теории доказательств . Эльзевир. С. 1–78. ISBN 0-444-89840-9 . CS1 maint: обескураженный параметр ( ссылка )
- Детловс, Вилнис; Подниекс, Карлис (24 мая 2017 г.). «Аксиомы логики: минимальная система, конструктивная система и классическая система». Введение в математическую логику (PDF) . Латвийский университет . С. 29–30.