عمق وجهی

در منطق موجهات،  عمق وجهی یک فرمول، عمیقترین تودرتویی  است که عمیق‌ترین تودرتو از عملگرهای وجهی (معمولاً $◻$ و $◊$) است. فرمولهای وجهی بدون عملگر وجهی، دارای عمق وجهی صفر هستند.

تعریف

عمق وجهی را می‌توان به شرح زیر تعریف شده کرد. فرض کنید$MD(\varphi )$ یک تابع باشد که عمق یک فرمول وجهی $\varphi$ را محاسبه می‌کند:

$MD(p)=0$، که $p$ یک فرمول اتمی است.

$MD(\mathrm{\top })=0$

$MD(\mathrm{\perp })=0$

$MD(\mathrm{\neg }\phi )=MD(\phi )$

$MD(\phi \wedge \psi )=max(MD(\phi ),MD(\psi ))$

$MD(\phi \vee \psi )=max(MD(\phi ),MD(\psi ))$

$MD(\phi \to \psi )=max(MD(\phi ),MD(\psi ))$

$MD(◻\phi )=1+MD(\phi )$

$MD(◊\phi )=1+MD(\phi )$

مثال

محاسبه زیر عمق وجهی $◻(◻p\to p)$ را بدست می‌دهد:

$MD(◻(◻p\to p))=$

$1+MD(◻p\to p)=$

$1+max(MD(◻p),MD(p))=$

$1+max(1+MD(p),0)=$

$1+max(1+0,0)=$

$1+1=:2$