Subintuitionistic logics and their modal companions: a nested approach

Area of Science:

• Logic
• Proof Theory
• Modal Logic

Background:

• Subintuitionistic logics are weaker fragments of intuitionistic logic.
• Modal logics extend classical or intuitionistic logic with modal operators.
• Nested calculi offer a structured framework for logical systems.

Purpose of the Study:

• To introduce novel nested calculi for subintuitionistic systems.
• To develop nested calculi for modal logics within the S4 modal cube.
• To provide a purely syntactic proof of the Gödel-McKinsey-Tarski embedding.

Main Methods:

• Development of specialized nested calculi.
• Application of proof-theoretic techniques.
• Analysis of modal operator rules in nested systems.

Main Results:

• A purely syntactic proof of the Gödel-McKinsey-Tarski embedding is established.
• The embedding preserves derivation structure and height.
• A conservativity result for classical logic over a weak subintuitionistic system is obtained.

Conclusions:

• The introduced nested calculi provide a powerful tool for studying subintuitionistic and modal logics.
• The syntactic proof offers new insights into the Gödel-McKinsey-Tarski embedding.
• The conservativity result highlights the relationship between classical and subintuitionistic logic.