Monday, 22 December 2008, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B126
Abstract: A logical formula F(X,P) is treated here as an equation to be satisfied by solution X0(P) for unknown predicate symbols X (with parametric predicate symbols P). We find general solution for monadic predicate logic with equality. Elimination of quantifiers provides necessary and sufficient solvability conditions of the form ∨i≤ m Ri(P) with Ri(P) = ∧s Qi,sx Ps(x). Here s ranges over all possible states P1σ1(x)∧...∧ Pnσn(x) and Qi,s is ∃=is or ∃≥ is. The general solution consists of the components X0i(P), i≤ m, such that Ri(P) → F(X0i(P),P) (*) is valid. X0i(P) contains ε-terms for ∃-quantifiers in Ki. This solves a parameterization problem stated by J. McCarthy (see this page).
The components are glued together in a standard way: X0:= (R1∧ X01)∨(R2∧ &neg; R1∧ X02)∨ ... ∨ (Rm∧∧i < m&neg; Ri∧ X0m) . X0 is a solution: ∨i Ri → F(X0,P), since Ri→ (X0 ↔ X0i) and (*) holds.
X0 is a general solution: for every state s and i ≤ m there is a substitution σi for the predicates occurring in X0 but not in P (arbitrary constants) that turns X0 into X0i in state Ps provided Ri holds. This implies ∨i Ri→ ∨i (σi( X0)↔ X0i) since ∨s Ps is valid.
(Joint work with Tomohiro Hoshi.)