فرامنطق استدلال در فرازبان درباره تعبیر و نحو در زبان‌های صوری (مانند LC) و دستگاه‌های صوری مانند (دستگاه CND) است. بنابراین، ما اینجا و در فرازبان به بیان احکام درباره دستگاه‌های استنتاجی (دستگاه CND و دستگاه CND+Cp) خواهیم پرداخت. این احکام
(احکام درباره دستگاه‌های استنتاجی) فراقضیه نامیده
می‌شوند. به‌عبارت‌دیگر، یک فراقضیه حکم یا خاصیتی درباره یک دستگاه استنتاجی معین است که در فرامنطق به فرازبان بیان و اثبات می‌‌گردد. در منطق، تفکیک بین قضیه و فراقضیه بسیار مهم است. اولی یک فرمول خوش-ساخت است که در دستگاه استنتاجی دست آوردنی است و دومی خاصیت اثبات‌شده‌ای درباره دستگاه استنتاجی در فرازبان است.
• دو رکن فرامنطق، ازجمله،
عبارتند از (فرا)قضیه رسانش (Soundness) و (فرا)قضیه تمامیت (یا ناتمامیت) (Completeness / Incompleteness)
درباره دستگاه‌های صوری.
در ادامه، رسانش و تمامیت دستگاه‌های CND و CND+Cp
را خواهیم دید و می‌بینیم که فراقضیه‌های رسانش و تمامیت در این دستگاه‌ها وارون (به‌عبارت‌دیگر، شرط لازم و کافی) هم هستند.
گرچه طولانی ولی به‌وسیله جداول ارزش می‌توان آزمود و دید که همه قواعد استنتاج در CND استلزام منطقی هستند و بنابراین رسا هستند. پس در حالت (۱) هر مدل مقدمات، مدل نتیجه نیز خواهد بود. در حالت (۲) که نتیجه یکی از مقدمات است آنگاه هر مدل مجموعه مقدمات آن استنتاج به اقوی دلیل مدل این مقدمه نیز است. بنابراین دستگاه استوار است.
(د.۲) تمامیت دستگاه: CND
فراقضیه تمامیت وارون فراقضیه رسانش است. پس، گوییم دستگاه CND تمام است اگرهر استلزام منطقی، استنتاج باشد، به عبارت دیگر، هر استنتاج معنایی یک استنتاج معتبر نحوی باشد. نیز به گونه دیگر، آنچه نتیجه منطقی است، نتیجه نحوی است.
اثبات تمامیت [یا ناتمامیت] دستگاه‌های استنتاجی دارای روندی
کمی گسترده تا بسیار طولانی است. اثبات
تمامیت برای دستگاه CND را می‌توانید در ارجاعی کتاب در فصل ۱۰ قسمت ۷ بیابید.
همان‌طور که دیدیم، در دستگاه CND+Cpرسانش و تمامیت شرط لازم و کافی یکدیگرند. بنابراین در این دستگاه، فراقضیه‌های رسانش و تمامیت را می‌توان با صورت‌بندی
— فرمول α قضیه است، اگر و فقط اگر توتولوژی باشد
— بیان کرد.
بنابراین داریم:
⊩CND ⇔ ⊢CND
⊩CND+Cp ⇔ ⊢CND+Cp
به‌عبارت‌دیگر، هر دستگاه صوری گزاره‌ای همچون سازواره‌های ماشینی سازگاری هستند که می‌توانند همه صور معتبر و فقط صور معتبر آن دستگاه را تولید کنند. قضیه تمامیت برای زبان صوری گزاره‌ای همان چیزی است که لایبنیتس در پی آن بود ولی برای زبانی جهان‌شمول.
گوتفرید ویلهم لایبنیتس - Gottfried Wilhelm Leibniz
... هرگاه چالش به پا خاست، نیاز به جدال بین فیلسوفان نیست مگر بین دو حسابدار. کافیست آن‌ها قلم‌هایشان را در دست گیرند و پشت حسابگرهای خود بنشینند (و اگر شاهدی خواستند نیز بیاورند) و به یک دیگر گویند: اکنون بگذاریم حسابگر حساب کند.
1- Ronald Chrisley (Editor); "Artificial Intelligence: Critical Concepts in Cognitive Science 1st Edition", Routledge; 1 edition (January 16, 2001). p. 14.
2- De arte characteristica ad perficiendas scientias ratione nitentes in C. I. Gerhardt (ed.), Die philosophischen Schriften von Gottfried Wilhelm Leibniz (7 vols. 1875–1890) VII 125.
گوتفرید ویلهم لایبنیتس (Gottfried Wilhelm Leibniz م۱۶۴۶-۱۷۱۶) فیلسوف، منطق دان و ریاضیدان بزرگ آلمانی، یکی از دو بنیان‌گذار دانش حساب دیفرانسیل و انتگرال و آغازگر در تدوین اندیشه دستگاه صوری (Lingua characteristica/ زبان نوعی/صوری و Calculus ratiocinator / حساب استدلال) است. آنچه او می‌خواست ماشین برهان بود تا فیلسوفان هنگام اختلاف بدان رجوع کنند. خواست وی در زمانه وی دست نیافتی، زیرا نه منطق جدید و نه تکنیک مقتضی موجود بود. راسل و وایتهد (در پی کتاب مفهوم نگاریفرگه) در تألیف اثر مشهور و بسیار تأثیرگذار اصول ریاضی به دنبال چنین دستگاهی برای ریاضیات بودند. سرانجام گودل "یک‌شبِ ره صد ساله پیموده" با دو قضیه ناتمامیت خود به میدانگاه آمد. خواست لایبنیتس نه دقیقاً آنچه وی می‌خواست هنوز، گرچه به‌تقریب، نامیسر نیست و هم‌اکنون، در بعضی دامنه‌های از پیش معین، میسر و آماده است.
بریده‌ای از "کتاب تاریخ فلسفه غرب"، برتراند راسل، ترجمه نجف دریابندری است (جلد ۲- صفحه ۴۵۰).
(د.۴) صدق منطقی
گیریم α۱, α۲,. . ., αn فرمول‌های یک دستگاه استنتاجی باشند، به قسمی که داشته باشیم:
α۱⊢α۲ α۲⊢α۳
. . .
αn-۱⊢αn.
اکنون با کار زدن رسانش و تمامیت به‌آسانی می‌توان دید که، اگر دستگاه استنتاجی موردنظر رسا باشد آنگاه هر مدل α۱ مدل αn نیز خواهد بود. به عیارت دیگر، در هر تعبیر که α۱ درست باشد αn هم درست است [به‌عبارت‌دیگر، دارای صدق منطقی است]. ازاین‌جهت گفته می‌شود در دستگاه‌های استنتاجی رسا، رابطه ⊢رسانای صدق منطقی است.
(د.۵) سازگاری دستگاه CND
برای هر تعبیر دلخواه I اگر (~α)I=درست، آنگاه (α)I=نادرست. پس چنین نیست که در CND داشته باشیم: ~α⊩α.ازاینجا و بنا بر رسانش و تمامیت نیز چنین نخواهد بود که در~α⊢α :CND. پس دستگاه CNDسازگار است.
همان‌طور که در بند ۱ نظریه سورها می‌توان دید، چنین نیست که همه استدلالها تابع-ارزش باشند. افزودن واژگان "متغیر انفرادی"، "ثابت‌های انفرادی"، "حروف محمولی"، "سور عمومی"، و "سور وجودی" به واژگان بنیادی زبان صوری گزاره‌ای و نیز تعداد محدود قاعده استنتاج بیشتر دستگاه حساب محمولات مرتبه اول با توان بیان بسیار بیشتر را پدید می‌آورد. کورت گودل (۱۹۳۰) و بعد دیگران نشان دادند در هر حساب محمولات مرتبه اولقضیه تمامیت برقرار است، یعنی:
قضایای هر حساب محمولات مرتبه اول دقیقاً فرمول‌های منطقاً معتبر آن هستند.
به‌عبارت‌دیگر،
هر دستگاه صوری مرتبه اول همچون سازواره سازگاری است که می‌تواند تحت هر تعبیر همه‌ی عبارات درست و فقط درست را تولید کنند.
(د.۲.۶) ناتمامیت در منطق محمولات
در زبان محمولات مرتبه اول دامنه گیرایش سور فقط می‌تواند متغیرهای انفرادی باشد. این محدودیت باعث می‌شود نتوان همه عبارات ریاضیات حتی حساب مقدماتی (و زبان طبیعی)، برای مثال اصل استقرای ریاضی و نیز خوش-ترتیبی را بیان کرد. زبانی که دارای این توان توان گویایی است، زبان صوری محمولات مرتبه دوم (دستگاه صوری مرتبه دوم) نامیده می‌شود. در محمولات مرتبه دوم دامنه گیرایش سور می‌تواند حروف محمولی (نیز حروف تابعی) باشد. برای مثال گیریم P یک حرف محمولی تک موضعی (یعنی یک خاصیت) باشد. فرمول:
(x)(P)[P(x)∨~P(x)]
یک فرمول مرتبه دوم منطقاً معتبر است که می‌گوید: برای x دلخواه و هر خاصیت P دلخواه؛ x خاصیت P را دارد یا ندارد [هر شیئی هر خاصیتی را دارد یا آن را ندارد - هر شیئی خاصیتی دارد یا ندارد.]
قضیه تمامیت به اینجا نرسیده خود تمام می‌شود، چراکه کورت گودل با دو قضیه ناتمامیت که در زیر به آن‌ها اشاره‌شده به میدان می‌آید.
قضیه اول ناتمامیت:
سازواره ماشینی [Machinery] سازگاری که بتواند همه گزاره‌های درست و فقط درست حساب را تولید کند وجود ندارد.
قضیه دوم ناتمامیت:
سازواره ماشینی [Machinery]سازگاری (در حساب) که بتواند سازگاری خود را ثابت کند وجود ندارد.
۵. منطق و فرامنطق 
;)
