منطق پویا (منطق وجهی): تفاوت میان نسخه‌ها

محتوای حذف‌شده محتوای افزوده‌شده
بدون خلاصۀ ویرایش
بدون خلاصۀ ویرایش
برچسب‌ها: متن دارای ویکی‌متن نامتناظر ویرایشگر دیداری
خط ۲۹:
A6. <math>p \land [a*](p \to [a]p) \to [a*]p\,\!</math>
 
* اصل A1 این قول خالی را می‌دهد که موقعی که '''BLOCK''' تمام می‌شود، <math> p </math> برقرار است، حتی اگر <math> p </math> گزاره ی '''false''' باشد. از این رو '''BLOCK''' وجود عمل «ابدیت قابل دست یافتن نیست» را انتزاعی می‌کند.
* اصل A2 می‌گوید که '''NOP''' به صورت تابع همانی روی گزاره‌ها عمل می‌کند، یعنی این عملگر <math> p </math> را به خودش تبدیل می‌کند.
 
* اصل A3 می‌گوید اگر انجام یکی از <math> {\displaystyle a\,\!} </math> یا <math> {\displaystyle b\,\!} </math> باید سبب وقوع <math> p </math> شود، آنوقت <math> {\displaystyle a\,\!} </math> باید سبب وقوع <math> p </math> شود و به صورت مشابه برای <math> {\displaystyle b\,\!} </math> و بالعکس.
اصل A2 می‌گوید که '''NOP''' به صورت تابع همانی روی گزاره‌ها عمل می‌کند، یعنی این عملگر <math> p </math> را به خودش تبدیل می‌کند.
* اصل A4 می‌گوید اگر انجام <math> {\displaystyle a\,\!} </math> و سپس انجام <math> {\displaystyle b\,\!} </math> باید سبب وقوع <math> p </math> شود، آنوقت <math> {\displaystyle a\,\!} </math> باید سبب وقوع وضعیتی شود که در آن <math> {\displaystyle b\,\!} </math> باید سبب وقوع <math> p </math> شود.
 
* A5 یک نتیجه آشکار از اعمال A2، A3 و A4 به معادله <math> {\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!} </math> از [[:en:Kleene_algebra|جبر کلینی]] است.
اصل A3 می‌گوید اگر انجام یکی از <math> {\displaystyle a\,\!} </math> یا <math> {\displaystyle b\,\!} </math> باید سبب وقوع <math> p </math> شود، آنوقت <math> {\displaystyle a\,\!} </math> باید سبب وقوع <math> p </math> شود و به صورت مشابه برای <math> {\displaystyle b\,\!} </math> و بالعکس.
* A6 ادعا می‌کند که اگر <math> p </math> هم‌اکنون برقرار باشد، و مهم نباشد که ما چند بار <math> {\displaystyle a\,\!} </math> را انجام داده‌ایم، آنوقت صحت <math> p </math> بعد از آن اجرا مستلزم صحت آن بعد از یک اجرای اضافی <math> {\displaystyle a\,\!} </math> است، در این صورت <math> p </math> باید صحیح بماند بدون توجه به اینکه ما چند بار <math> {\displaystyle a\,\!} </math> را اجرا کرده‌ایم. A6 به عنوان [[استقرای ریاضی]] شناخته می‌شود، که در آن عمل '''n := n+1''' از افزایش '''n''' توسط عمل اختیاری <math> {\displaystyle a\,\!} </math> تعمیم یافته است.<ref name=":0" />
 
اصل A4 می‌گوید اگر انجام <math> {\displaystyle a\,\!} </math> و سپس انجام <math> {\displaystyle b\,\!} </math> باید سبب وقوع <math> p </math> شود، آنوقت <math> {\displaystyle a\,\!} </math> باید سبب وقوع وضعیتی شود که در آن <math> {\displaystyle b\,\!} </math> باید سبب وقوع <math> p </math> شود.
 
A5 یک نتیجه آشکار از اعمال A2، A3 و A4 به معادله <math> {\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!} </math> از [[:en:Kleene_algebra|جبر کلینی]] است.
 
A6 ادعا می‌کند که اگر <math> p </math> هم‌اکنون برقرار باشد، و مهم نباشد که ما چند بار <math> {\displaystyle a\,\!} </math> را انجام داده‌ایم، آنوقت صحت <math> p </math> بعد از آن اجرا مستلزم صحت آن بعد از یک اجرای اضافی <math> {\displaystyle a\,\!} </math> است، در این صورت <math> p </math> باید صحیح بماند بدون توجه به اینکه ما چند بار <math> {\displaystyle a\,\!} </math> را اجرا کرده‌ایم. A6 به عنوان [[استقرای ریاضی]] شناخته می‌شود، که در آن عمل '''n := n+1''' از افزایش '''n''' توسط عمل اختیاری <math> {\displaystyle a\,\!} </math> تعمیم یافته است.<ref name=":0" />
<br />{{منطق-خرد}}