Mathematical Logic Seminar Abstracts Spring 2011

We review Petr Hajek's 2002 paper "Monadic Fuzzy Predicate Logics" starting with the syntax and semantics of Lukasiewicz, Godel, product, and basic fuzzy logics. We then consider, for monadic fragments of these logics, the set of tautologies (TAUT), satisfiable formulas (SAT), finite model tautologies (fTAUT), and finite model satisfiable formulas (fSAT). Particular results include: the sets TAUT=fTAUT and SAT=fSAT in monadic Lukasiewicz logic are recursive, fSAT is recursive in Godel logic, and fSAT is recursive in monadic product logic.

We will review the paper of the title, which explains how to formalize a certain forcing argument in RCA_0. The paper uses this to give an effective proof that WKL_0 is conservative over RCA_0 with only a polynomial increase in proof length.

The system M1 of modal mu-calculus has been introduced by G.Jaeger and T.Studer and proved to be sound and complete for a suitable Kripke semantics and admit a cut-free formulation using Buchholz's Omega-rule. We show that simpler rules based on the equivalence between P and the disjunction V_k A^k(false) for the fixpoint P\iff A(P) are also sound and complete and admit cut-elimination. Even simpler proof (using an idea due to W. Pohlers) shows that complete cut-elimination for derivations of arbitrary sequents is possible in the Omega-calculus for ID1.

The modal mu-calculus may be a serious candidate, not just for describing computation, but also for other tasks that modal logics have been used for, such as abstract analysis of provability. I will give a brief tour of some recent results in this area: (a) connections between the mu-calculus and Goedel-Loeb provability logic, (b) extending modal correspondence theory to mu-calculus.

References: J. van Benthem, 2005, 'Minimal Predicates, Fixed-Points, and Definability, Journal of Symbolic Logic 70:3, 696-712. J. van Benthem, 2006, 'Modal Frame Correspondences and Fixed-Points', Studia Logica 83:1, 133 - 155. J. van Benthem, N. Bezhanishvili & I. Hodkinson, in progress, 'Sahlqvist Correspondence for Modal Mu-Calculus', ILLC Amsterdam & IC London.

Smorynski's 1973 "Elementary Intuitionistic Theories" provides a survey of decidability and undecidability results in the intuitionistic setting. I will present on the paper's major negative results, including the undecidability of the predicate calculus on a single monadic predicate (originally due to Maslov, Mints, and Orevkov, with a semantic proof by Gabbay) and Lifshits's results on the undecidability of the intuitionistic theories of equality and normal equality.

Takeuti and Titani refer to I-valued logic (where I is the closed real interval [0,1]) as intuitionistic fuzzy logic (IF) and I-valued set theory as intuitionistic fuzzy set theory (ZF_{IF}). In their paper (Intuitionistic Fuzzy Logic and Intuitionistic Fuzzy Set Theory, JSL 49, 3, 1984, 851-866) they:
1. axiomatize the intuitionistic fuzzy logic IF,
2. prove consistency and strong completeness of IF

Then in the second section they
3. present the intuitionistic fuzzy set theory ZF_{IF} and develop a calculus for it
4. present a sheaf model of ZF_{IF}, $V^I$
5. show that the classical forms of Rolle's theorem, the mean value theorem, and Taylor's theorem hold in their model.

They also discuss Powell's innermodel, but we aim to present simply 1 to 5.

This is a review of Yu. Gurevich, Monadic Second-Order Theories (in: Model-theoretic logics, 1985, edited by J. Barwise, S. Feferman). Monadic Theory of Finite Chains, Monadic Theory of omega, Monadic Theory of the Binary Tree, Monadic Theory of Countable Ordinals, Undecidability.