Здравствуйте

Разгребая старый макаронный С-код, стал думать как бы составить все логические уравнения (условия) для строк внутри функции с целью упрощения. В конце концов стал учить калкулюс, и читая википедию возник такой вопрос:

Вот тут даются схемы аксиом и далее пример доказательства A → A.
Вопрос: разве, изменив соответствующим образом использование схем аксиом в п. 1 и 2 — не получается, что таким же образом можно доказать A → B, и вообще, А → <что угодно> ? Где ошибка?

PS: В первом шаге считать ψ = B, χ = Z → A и т.д.

Здравствуйте, dilettante, Вы писали:


D>Вот тут даются схемы аксиом и далее пример доказательства A → A.
D>Вопрос: разве, изменив соответствующим образом использование схем аксиом в п. 1 и 2 — не получается, что таким же образом можно доказать A → B, и вообще, А → <что угодно> ? Где ошибка?

D>PS: В первом шаге считать ψ = B, χ = Z → A и т.д.

выкладки сделай, тогда увидишь, где ошибка (ну или мы ткнём).

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, dilettante, Вы писали:

D>>PS: В первом шаге считать ψ = B, χ = Z → A и т.д.

D>выкладки сделай, тогда увидишь, где ошибка (ну или мы ткнём).

Да, вчера ночью не заметил — а сейчас сделал ещё раз и увидел ошибку, спасибо

Вообще адская вещь, как подходить к доказательству даже чего-то совсем простого — например (Α∧B→C) → (A→B→C) — совершенно не понятно.

Здравствуйте, dilettante, Вы писали:

D>Вообще адская вещь, как подходить к доказательству даже чего-то совсем простого — например (Α∧B→C) → (A→B→C) — совершенно не понятно.

Откройте для себя секвенциальное исчисление, там свойство подформульности сильно упрощает автоматизацию доказательства.

D>Вообще адская вещь, как подходить к доказательству даже чего-то совсем простого — например (Α∧B→C) → (A→B→C) — совершенно не понятно.

это исчисление полно, и вывод утверждений в нем это не более глубокая вешь чем разложение формул в ДНФ.

Здравствуйте, dilettante, Вы писали:

D>Вообще адская вещь, как подходить к доказательству даже чего-то совсем простого — например (Α∧B→C) → (A→B→C) — совершенно не понятно.

Сначала избавляешься от ненужных стрелок: A->B == !A | B
А потом как в арифметике начальной школы(только булева арифметика малость отличается), раскрываешь скобочки и убеждаешься что оно==true
Такие штуковины наверное известны? !(A&B)==!A | !B ; ...

(A&B -> C) -> (A->B->C)
!( !(A&B) | C) | (!A | (!B | C))
( A & B & !C) | !(A & B & !C)
X | !X == true

Здравствуйте, Silver_S, Вы писали:

S_S>(A&B -> C) -> (A->B->C)
S_S>!( !(A&B) | C) | (!A | (!B | C))
S_S>( A & B & !C) | !(A & B & !C)
S_S>X | !X == true

Классицист детектед, интуиционисты негодуют.

Доказываем через изоморфизм Карри-Говарда:

curry :: ((a, b) -> c) -> a -> b -> c
curry f x y  =  f (x, y)

Здравствуйте, deniok, Вы писали:

D>Здравствуйте, Silver_S, Вы писали:

S_S>>(A&B -> C) -> (A->B->C)
S_S>>!( !(A&B) | C) | (!A | (!B | C))
S_S>>( A & B & !C) | !(A & B & !C)
S_S>>X | !X == true

D>Классицист детектед, интуиционисты негодуют.

D>Доказываем через изоморфизм Карри-Говарда:
D>

D>curry :: ((a, b) -> c) -> a -> b -> c
D>curry f x y  =  f (x, y)
D>

тут доказательство в смысле "скомпилируется программа или нет"?

You will always get what you always got
  If you always do  what you always did

Здравствуйте, jazzer, Вы писали:

J>Здравствуйте, deniok, Вы писали:

D>>Здравствуйте, Silver_S, Вы писали:

S_S>>>(A&B -> C) -> (A->B->C)
S_S>>>!( !(A&B) | C) | (!A | (!B | C))
S_S>>>( A & B & !C) | !(A & B & !C)
S_S>>>X | !X == true

D>>Классицист детектед, интуиционисты негодуют.

D>>Доказываем через изоморфизм Карри-Говарда:
D>>

D>>curry :: ((a, b) -> c) -> a -> b -> c
D>>curry f x y  =  f (x, y)
D>>

J>тут доказательство в смысле "скомпилируется программа или нет"?

Да, в смысле, что если мы можем написать валидную функцию с таким типом, то этот тип — теорема логики. Правда, пара (эквивалент И) введена ad hoc, честнее было бы конечно всё делать не в Хаскелле, а в System F. Но у Хаскелла внутреннее представление — это фактически System F (с расширениями, конечно).

Здравствуйте, dilettante, Вы писали:

D>... как подходить к доказательству даже чего-то совсем простого — например (Α∧B→C) → (A→B→C) — совершенно не понятно.
Если писать движок, претендующий на высокую интеллектуальность. То проблема будет не столько в том, как доказать какую-то громоздкую конструкцию, а как найти наиболее простой способ из огромного множества других вариантов.
Если не использовать навороченые теоремы, то в этом примере наиболее простой способ, все-же, самый дубовый. Подстановкой значения A.
(A&B -> C) -> (A->B->C)
Вместо A подставляем true, остается: (B -> C) -> (B->C) == true
Подставляем false: (false -> C) -> (false->(B->C)), из него true->true==true