Second Order Logic: WS1S and HOL

This lecture covers the concepts of Second Order Logic (SOL), Weak Monadic Second Order Logic, and Weak Monadic Second Order Logic of 1 Successor. It explains the syntax and semantics of WS1S formulas, decision procedures, atomic and composite formulas, and the embedding function translating WS1S formulae into HOL formulae. The lecture also discusses the combination of WS1S and MONA with HOL and Isabelle, illustrating how to express problems in HOL and automatically solve subproblems in WS1S. The presentation concludes with the oracle usage, correctness, and theorems related to WS1S and HOL.