Tłumaczenie z podwójną negacją

W teorii dowodu , dyscyplina logiki matematycznej , tłumaczenie podwójnej negacji , czasami nazywane tłumaczeniem negatywnym , jest ogólnym podejściem do osadzania logiki klasycznej w logice intuicjonistycznej , zwykle poprzez tłumaczenie formuł na formuły, które są klasycznie równoważne, ale intuicjonistycznie równoważne. Szczególne przypadki tłumaczenia podwójnej negacji obejmują tłumaczenie Glivenki dla logiki zdań oraz tłumaczenie Gödla-Gentzena i tłumaczenie Kurody dla logiki pierwszego rzędu .

Logika zdaniowa

Najłatwiejsze do opisania tłumaczenie z podwójną negacją pochodzi z twierdzenia Glivenki , udowodnionego przez Walerego Glivenkę w 1929 roku. Odwzorowuje ono każdą klasyczną formułę φ na jej podwójną negację ¬¬φ.

Twierdzenie Glivenko stwierdza:

Jeśli φ jest formułą zdaniową, to φ jest klasyczną tautologią wtedy i tylko wtedy, gdy ¬¬φ jest tautologią intuicjonistyczną.

Twierdzenie Glivenki implikuje bardziej ogólne stwierdzenie:

Jeśli T jest zbiorem formuł zdaniowych, a φ jest formułą zdaniową, to T ⊢ φ w logice klasycznej wtedy i tylko wtedy, gdy T ⊢ ¬¬φ w logice intuicjonistycznej.

W szczególności zestaw formuł zdaniowych jest intuicjonistycznie spójny wtedy i tylko wtedy, gdy jest klasycznie spełnialny.

Logika pierwszego rzędu

Tłumaczenie Gödla – Gentzena (nazwane na cześć Kurta Gödla i Gerharda Gentzena ) wiąże z każdą formułą φ w języku pierwszego rzędu inną formułę φ ^N , która jest zdefiniowana indukcyjnie:

Jeśli φ jest atomowe, to φ ^N to ¬¬φ
(φ ∧ θ) ^N jest φ ^N ∧ θ ^N
(φ ∨ θ) ^N wynosi ¬(¬φ ^N ∧ ¬θ ^N )
(φ → θ) ^N jest φ ^N → θ ^N
(¬φ) ^N to ¬φ ^N
(∀ x φ) ^N wynosi ∀ x φ ^N
(∃ x φ) ^N wynosi ¬∀ x ¬φ ^N

To tłumaczenie ma tę właściwość, że φ ^N jest klasycznie równoważne φ. Podstawowe twierdzenie o słuszności (Avigad i Feferman 1998, s. 342; Buss 1998, s. 66) stwierdza:

Jeśli T jest zbiorem aksjomatów ^, a φ jest formułą, to T dowodzi φ za pomocą logiki klasycznej wtedy i tylko wtedy, gdy TN dowodzi φ ^N za pomocą logiki intuicjonistycznej.

Tutaj T ^N składa się z translacji podwójnie negujących formuł w T .

Zdanie φ nie może implikować jego negatywnego tłumaczenia φ ^N w intuicjonistycznej logice pierwszego rzędu. Troelstra i van Dalen (1988, rozdz. 2, rozdz. 3) podają opis (ze względu na Leivanta) formuł, które implikują ich tłumaczenie Gödla – Gentzena.

Warianty

Istnieje kilka alternatywnych definicji przekładu negatywnego. Wszystkie są w sposób możliwy do udowodnienia równoważne w logice intuicjonistycznej, ale mogą być łatwiejsze do zastosowania w określonych kontekstach.

Jedną z możliwości jest zmiana klauzul dotyczących dysjunkcji i kwantyfikatora egzystencjalnego na

(φ ∨ θ) ^N jest ¬¬(φ ^N ∨ θ ^N )
(∃ x φ) ^N wynosi ¬¬∃ x φ ^N

Wtedy tłumaczenie można zwięźle opisać jako: przedrostek ¬¬ do każdego wzoru atomowego, dysjunkcji i kwantyfikatora egzystencjalnego.

Inną możliwością (znaną jako tłumaczenie Kurody ) jest skonstruowanie φ ^N z φ przez wstawienie ¬¬ przed całym wzorem i po każdym uniwersalnym kwantyfikatorze . Zauważ, że sprowadza się to do prostej translacji ¬¬φ, jeśli φ jest zdaniowe.

Możliwe jest również zdefiniowanie φ ^N przez dodanie przedrostka ¬¬ przed każdą podformułą φ, tak jak zrobił to Kołmogorow . Takie tłumaczenie jest logicznym odpowiednikiem tłumaczenia funkcjonalnych języków programowania w stylu call-by-name z przekazywaniem kontynuacji na wzór korespondencji Curry-Howarda między dowodami a programami.

Wyniki

Tłumaczenie z podwójną negacją zostało użyte przez Gödla (1933) do zbadania związku między klasycznymi i intuicjonistycznymi teoriami liczb naturalnych („arytmetyka”). Otrzymuje następujący wynik:

Jeśli formuła φ jest dowodliwa z aksjomatów arytmetyki Peano , to φ ^N jest dowodliwa z aksjomatów arytmetyki Heytinga .

Wynik ten pokazuje, że jeśli arytmetyka Heytinga jest spójna, to spójna jest również arytmetyka Peano. Dzieje się tak, ponieważ sprzeczna formuła θ ∧ ¬θ jest interpretowana jako θ ^N ∧ ¬θ ^N , co nadal jest sprzeczne. Co więcej, dowód związku jest całkowicie konstruktywny, dając możliwość przekształcenia dowodu θ ∧ ¬θ w arytmetyce Peano w dowód θ ^N ∧ ¬θ ^N w arytmetyce Heytinga. (Łącząc translację podwójnej negacji z translacją Friedmana , można faktycznie udowodnić, że arytmetyka Peano jest ⁰ Π ₂ - konserwatywna w stosunku do arytmetyki Heytinga.)

Zdaniowe odwzorowanie φ na ¬¬φ nie rozciąga się na dźwiękową translację logiki pierwszego rzędu, ponieważ tak zwane przesunięcie podwójnej negacji

∀ x ¬¬φ( x ) → ¬¬∀ x φ( x )

nie jest twierdzeniem intuicjonistycznej logiki predykatów. To wyjaśnia, dlaczego φ ^N musi być definiowane w bardziej skomplikowany sposób w przypadku pierwszego rzędu.

Zobacz też

Interpretacja dialektyki

J. Avigad i S. Feferman (1998), „Interpretacja funkcjonalna Gödla („Dialectica”)”, Handbook of Proof Theory , wyd. S. Buss, Elsevier. ISBN 0-444-89840-9
S. Buss (1998), „Wprowadzenie do teorii dowodu”, Handbook of Proof Theory , S. Buss, red., Elsevier. ISBN 0-444-89840-9
G. Gentzen (1936), „Die Widerspruchfreiheit der reinen Zahlentheorie”, Mathematische Annalen , t. 112, s. 493–565 (niemiecki). Przedrukowany w tłumaczeniu na język angielski jako „Konsystencja arytmetyki” w Zbiorze dokumentów Gerharda Gentzena , ME Szabo, wyd.
V. Glivenko (1929), Sur quelques points de la logique de M. Brouwer , Bull. soc. Matematyka Belg. 15, 183-188
K. Gödel (1933), „Zur intuitionistischen Arithmetik und Zahlentheorie”, Ergebnisse eines mathematischen Kolloquiums , t. 4, s. 34–38 (niemiecki). Przedrukowany w tłumaczeniu na język angielski jako „O intuicjonistycznej arytmetyce i teorii liczb” w The Undecidable , M. Davis, red., s. 75–81.
AN Kołmogorow (1925), „O principe tertium non datur” (rosyjski). Przedrukowany w tłumaczeniu na język angielski jako „Na zasadzie wyłączonego środka” w From Frege to Gödel , van Heijenoort, red., s. 414–447.
AS Troelstra (1977), „Aspekty konstruktywnej matematyki”, Handbook of Mathematical Logic , J. Barwise , red., Holandia Północna. ISBN 0-7204-2285-X
AS Troelstra i D. van Dalen (1988), Konstruktywizm w matematyce. Wprowadzenie , tomy 121, 123 Studiów z logiki i podstaw matematyki , Holandia Północna.

Linki zewnętrzne

„ Logika intuicjonistyczna ”, Stanford Encyclopedia of Philosophy.