🚀 go-pugleaf

On Jul 19, 12:26 pm, Wlodzimierz Holsztynski <sennaj...@gmail.com>
wrote:

> Duże litery  X X' X'' ... Y Y' ... Z ... są meta-symbolami
> oznaczającymi zdania teorii rachunku zdań.

Wprowadźmy też schematy zdaniowe, które
synktaktycznie są dokładnie jak zdania,
z jednym wyjątkiem: zamiast małych liter
dopuszcza się i małe i duże litery. Na przykład

    (X \/ Y)        (x /\ X)

są dwoma schematami zdaniowymi. Schematy
zdaniowe będę oznacazał przez  SA  SA' ... SZ SZ' ...

> Reguły dowodzenia są napisami postaci
>
>     X ... Y |-> Z
>
> gdzie po lewej mamy skończony ciąg
> (meta-symboli) zdań teorii, a po prawerj
> jeden meta-symbol zdania Z; z tym, że zamiast
> X Y Z itp mamy bardziej skomplikowane wyrażenia
> typu  (X \/ Y), itp., na przykład:
>
>     X Y |-> (X /\ Y)
>     X |-> (X \/ Y)
>
> itp.

Przykłady dobrze podałem. Natomiast
ogólnie należy mówić o schematach, czyli tak:

Reguły dowodzenia są napisami postaci

     SX ... SY  |->  SZ

> Gdy ciąg po lewej jest pusty, to reguła dowodzenia
> podaje aksjomat  Z, na przykład.
>
>     |->  (Z \/ (~ Z))
>
> może ewentualnie służyć za aksjomat;
> albo
>
>     |->  (Z <=> Z)

Znowu przykłady aksjomatów podałem dobrze,
ale ogólnie należy mówić o schematach,
mamy schematy aksjomatów:

    |-> SZ

> Każdy aksjomat jest z definicji twierdzeniem
> (rachunku zdań), a raczej schematem twierdzeń,
> [...], twierdzenia są to zdania otrzymane
> po prawej stronie reguł dowodzenia, gdy
> po lewej występują tylko twierdzenia (w
> szczególności nic); i tylko takie zdania.
>
> Czyli iterujemy reguły dowodzenia.
> Twierdzenia są wynikami skonczonych iteracji.

Wprowadźmy także twierdzenia relatywne i pośrednie
reguły dowodzenia. Niech Set  bedzie pewnym (dowolnym)
zbiorem schematów zdaniowych. Zdanie lub schemat
zdaniowy SZ jest twierdzeniem względnym, względem Set,
gdy dodanie schematów z Set do aksjomatów pozwala SZ
udowodnić:

  gdy SZ pojawi się po prawej stronie regułu dowodzenia
  po skończonej liczbie stosowania reguł dowodzenia
  do schematów które są aksjomatami lub należą do Set
  lub są twierdzeniami relatywnymi.

Na przykład, jeżeli mamy regułę  SA |-> SZ   to  SZ
jest twierdzeniem relatywny względem zbioru  Set := {SA},
jak i względem każdego  Set zawierającego zbiór {SA}.

Gdy SZ jest twierdzeniem relatywnym, względem
(jakiegoś dowolnego) Set, to piszemy to jako
pośrednią regułę dowodzenia:

    Set |--> SZ

(zamiast krótkiego oznaczenia  |->  mamy dłuższe |-->).

Pośrednie reguły dowodzenia prowadzą od twierdzeń
do twierdzeń: gdy po lewej stronie kolejnych pośrednich
reguł dowodzenia występują wyłącznie twierdzenia, to
także po prawej stronie mamy same twierdzenia (a nie
ogólne-relatywne). Zatem pośrednie reguły dowodzenia
można stosować tak samo jak zwykłe - zawsze otrzyma się
poprawny wynik. Jest to bardzo wygodne narzędzie.

Podam ogólny niby-przykład. Gdy mamy reguły:

    SA  SB  |->  SY
    SC  SY  |->  SZ

to otrzymujemy pośrednią regułę:

    SA  SB  SC    |-->    SZ

którą możemy stosować jako skrót w następnych dowodach
(zamiast wciąż powoływać się na dwie podane reguly).

Pozdrawiam,

    Włodek

On Jul 19, 2:53 pm, "Wlodzimierz Holsztynski (Wlod)"
<sennaj...@gmail.com> wrote:

> Wprowadźmy także twierdzenia relatywne i pośrednie
> reguły dowodzenia.
> [...]
> Gdy SZ jest twierdzeniem relatywnym, względem
> (jakiegoś dowolnego) Set, to piszemy to jako
> pośrednią regułę dowodzenia:
>
>     Set |--> SZ
>
> (zamiast krótkiego oznaczenia  |->  mamy dłuższe |-->).

Skoro użyłem nazwy "posrednia", to niech
tak będzie. Wolę jednak synonim "skomponowana",
i odtąd raczej będę go używał, i zwrotu:

  skomponowana reguła dowodzenia.

Trochę przydługie słowo, ale można je
omijać, gdy sam znak  |-->  pokazuje, że chodzi
o komponowanie.

Pozdrawiam,

    Włodek

On Jul 19, 2:53 pm, "Wlodzimierz Holsztynski (Wlod)"
<sennaj...@gmail.com> wrote:

> Gdy SZ jest twierdzeniem relatywnym, względem
> (jakiegoś dowolnego) Set, to piszemy to jako
> pośrednią regułę dowodzenia:
>
>     Set |--> SZ
>
> (zamiast krótkiego oznaczenia  |->  mamy dłuższe |-->).

Już wspomniałem, że wolę nazwę
reguła skomponowana.

W szczególności twierdzenia to nic innego
niż konkluzje skomponowanych reguł
dowodzenia ze zbioru pustego.

Aksjomaty są konkluzjami reguł ze
zbioru pustego, a twierdzenia są
konkluzjami reguł skomponowanych,
też stosowanych do zbioru pustego.

*******************

Mója lista regul (i aksjomatów) z pewnością
będzie nieminimalna, a nawet chyba daleka
od minimalności (co potem bedzie można
wygładzić). Nie martwmy się tym. Moim celem
jest wyłożenie elementarnej teorii zdań, łącznie
z twierdzeniem o tautologiach i twierdzeniach,
bez tak zwanego "machania rękami" (ani nogami :-).

Nieminimalność wręcz ułatwia początkowe,
szybkie zrozumienie tematu, minimalność zaś
je może opóźniać.

Pozdrawiam,

    Włodek