Building toward a research identity at the intersection of mathematical logic, formal verification, and the theory of mind.
Formal specification of a deployed conversational AI agent as ⟨S, A, P, π, R, M⟩. Hybrid policy architecture combining rule-based reasoning and learned components. Ethical constraint formalism. Memory model grounded in cognitive science. Built and deployed in production at EngineCX.
Formalizing operational constraints of a deployed conversational agent in Standard Deontic Logic (SDL). Three theorems: (1) consistency of constraint set Γ via Kripke model construction, (2) completeness w.r.t. harm set H — every harmful action has F(a) derivable from Γ, (3) safe constraint updates form a lattice under set inclusion. Extends BRAIN with formal proofs.
The questions that keep me up at night — and the fields that are trying to answer them.
First-order logic, completeness and incompleteness theorems, proof theory, model theory. Working through Enderton systematically with Dr. Oliart.
Standard Deontic Logic, dynamic epistemic logic, Kripke semantics for normative reasoning. What agents know, believe, and ought to do — formalized.
Computability, complexity classes, the Church-Turing thesis. The diagonal argument as the skeleton of Cantor, Gödel, and Turing simultaneously.
Provably correct systems. Ethical constraints enforced by construction, not by policy. The research question: can machines be kind — and can we prove it?
Qubits as unit vectors in ℂ², Born rule, quantum gates as unitary linear maps. The mathematical physics of the next computational paradigm.
ZFC axioms, ordinals, cardinals, the Axiom of Choice. Building mathematics from ∅ upward — the universe where all of mathematics lives.
My SWE degree does not teach mathematical logic or proof theory. So I built my own curriculum — public, rigorous, ongoing. One proof written in full every week, no exceptions. Five tracks running in parallel.
Enderton. Currently §2.4.
Blackburn, van Ditmarsch.
Enderton — Elements of Set Theory.
Marker. EF games, types, QE.
Troelstra & Schwichtenberg.