The set of PrAl+valid in a finite structure is undecidable

We consider a probabilistic logic of programs. In it is proved that the set of formulas of the logic PrAL, valid in a finite structure, is decidable with respect to the diagram of the structure. We add to the language LP of PrAL a sign S and a functor lg. Next we justify that the set of formulas of extended logic, valid in a finite at least 2-element structure (for LP+) is undecidable.

Rozważamy probabilistyczną logikę algorytmiczną. W pracy znajduje się uzasadnienie, że zbiór formuł logiki PrAL, prawdziwych w skończonej strukturze, jest rozstrzygalny ze względu na diagram struktury. Dodajemy do języka LP logiki PrAL znak S i funktor lg. Następnie uzasadniamy, ze zbiór formuł rozszerzonej logiki, prawdziwych w skończonej co najmniej 2-elementowej strukturze (dla L P+), nie jest już rozstrzygalny.