Eksport (logika) - Exportation (logic)
Eksport jest ważną regułą zastępowania w logice zdań . Zasada pozwala stwierdzenia warunkowe o spojówek wyznaczników zastępuje oświadczenia o warunkowe następniki i vice versa w dowodów logicznych . Zasadą jest, że:
Gdzie „ ” jest symbolem metalicznym reprezentującym „można go zastąpić w dowodzie”.
Notacja formalna
Wywozu reguła może być napisany w Sequent notacji:
gdzie jest metalogiki symbol oznacza, że jest składniowym równoważne z w pewnym układ logiczny ;
lub w formie reguły :
- ,
gdzie regułą jest, że gdziekolwiek instancja " " pojawia się w wierszu dowodu, może być zastąpiona przez " " i vice versa;
lub jako stwierdzenie tautologiczno -funkcjonalnej prawdziwości lub twierdzenia logiki zdań:
gdzie , , i są zdaniami wyrażonymi w jakimś systemie logicznym .
Język naturalny
Wartości prawdy
W dowolnym momencie, jeśli P→Q jest prawdziwe, można je zastąpić P→(P∧Q).
Jednym z możliwych przypadków dla P→Q jest to, że P jest prawdziwe, a Q jest prawdziwe; zatem P∧Q jest również prawdziwe, a P→(P∧Q) jest prawdziwe.
Inny możliwy przypadek ustawia P jako fałszywe, a Q jako prawdziwe. Zatem P∧Q jest fałszywe, a P→(P∧Q) jest fałszywe; fałsz → fałsz jest prawdą.
Ostatni przypadek ma miejsce, gdy zarówno P, jak i Q są fałszywe. Zatem P∧Q jest fałszywe, a P→(P∧Q) jest prawdziwe.
Przykład
Pada deszcz i świeci słońce, co oznacza, że jest tęcza.
Tak więc, jeśli pada deszcz, słońce świeci, oznacza to, że jest tęcza.
Jeśli mój samochód jest włączony, kiedy przełączam bieg na D, samochód zaczyna jechać. Jeśli mój samochód jest włączony i przestawiłem bieg na D, samochód musi ruszyć.
Dowód
Poniższy dowód używa Implikacji Materialnej , podwójnej negacji , Prawa De Morgana , negacji instrukcji warunkowej, własności asocjacyjnej koniunkcji, negacji innej instrukcji warunkowej i jeszcze raz podwójnej negacji, aby uzyskać wynik.
Propozycja | Pochodzenie |
---|---|
Dany | |
Implikacje materialne | |
Implikacje materialne | |
Łączność | |
Prawo de Morgana | |
Implikacje materialne |
Związek z funkcjami
Eksport jest powiązany z Currying za pośrednictwem korespondencji Curry–Howard .