# Alexander V. Gheorghiu

> Personal academic website of Dr Alexander V. Gheorghiu — Lecturer in the Programming Principles, Logic and Verification (PPLV) group, Department of Computer Science, University College London (previously a New Frontiers Fellow at the University of Southampton). Research centres on proof-theoretic semantics, philosophy of logic, and the formal foundations of AI reasoning. Graham Hoare Prize 2025 (Institute of Mathematics and its Applications).

Alexander Gheorghiu is a logician whose work studies the formal foundations of reasoning — how meaning arises from inference, how proofs structure thought, and what these foundations reveal about artificial intelligence. His central claim: the gap between statistical prediction and genuine reasoning is formally precise, not merely philosophical.

## Main pages

- [Home](https://alexandergheorghiu.com/): Overview of research, publications, and public engagement.
- [About](https://alexandergheorghiu.com/about.html): Academic biography, positions, and background.
- [Research](https://alexandergheorghiu.com/research.html): Research programme in proof-theoretic semantics and logic.
- [Publications](https://alexandergheorghiu.com/publications.html): Full list of journal articles, book chapters, and conference papers.
- [Writing & Essays](https://alexandergheorghiu.com/writing.html): Public-facing essays and talks, including pieces in the Times Literary Supplement, The Conversation, and Mathematics Today.
- [Contact](https://alexandergheorghiu.com/contact.html): Contact details and PhD supervision enquiries.

## Explainer pages

- [What Is Proof-Theoretic Semantics?](https://alexandergheorghiu.com/proof-theoretic-semantics.html): An accessible introduction to the research programme.
- [How Does Logic Relate to AI?](https://alexandergheorghiu.com/logic-and-ai.html): The relationship between formal reasoning and artificial intelligence.
- [What Is Base-Extension Semantics?](https://alexandergheorghiu.com/base-extension-semantics.html): How logical validity is defined against bases (sets of atomic inference rules) rather than models, drawing on Gheorghiu's research on first-order, linear, bunched, and arithmetical logics.
- [What Is Inferentialism?](https://alexandergheorghiu.com/inferentialism.html): The view that meaning is constituted by inferential role rather than reference, and its formal development in proof-theoretic semantics.
- [What Does a Logician Do?](https://alexandergheorghiu.com/what-is-a-logician.html): An explanation of mathematical logic as a discipline.
- [Glossary of Proof-Theoretic Semantics & Logic](https://alexandergheorghiu.com/glossary.html): Plain-language definitions of ~20 core concepts (base-extension semantics, harmony, inferentialism, natural deduction, normalisation, soundness, completeness, and more), each linked to the relevant explainer and research paper.

## Publications

Peer-reviewed articles and conference papers, each with a full HTML reading page. Index: https://alexandergheorghiu.com/publications.html

- [Defining Logical Systems via Algebraic Constraints on Proofs](https://alexandergheorghiu.com/publications/defining-logical-systems.html): Defines logical systems through algebraic constraints on proof structures, providing a general framework for proof-theoretic characterization.
- [Definite Formulae, Negation-as-Failure, and the Base-extension Semantics of Intuitionistic Propositional Logic](https://alexandergheorghiu.com/publications/definite-formulae-negation-as-failure.html): Studies the role of definite formulae and negation-as-failure in the base-extension semantics for intuitionistic propositional logic.
- [Focused Proof-search in the Logic of Bunched Implications](https://alexandergheorghiu.com/publications/focused-proof-search-bi.html): Develops focused proof-search for the logic of bunched implications, providing a decision procedure via focused sequent calculus.
- [From Basic Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic](https://alexandergheorghiu.com/publications/from-basic-pts-to-base-extension.html): Connects basic proof-theoretic validity in the sense of Dummett and Prawitz to base-extension semantics for intuitionistic propositional logic.
- [On an Inferential Semantics for Intuitionistic Sentential Logic](https://alexandergheorghiu.com/publications/inferential-semantics-intuitionistic.html): Relates Sandqvist's base-extension semantics for intuitionistic logic to Mints' resolution method, deriving soundness and completeness as corollaries.
- [Inferentialist Resource Semantics](https://alexandergheorghiu.com/publications/inferentialist-resource-semantics.html): Develops an inferentialist approach to resource semantics, connecting proof-theoretic semantics with resource-sensitive reasoning.
- [On the Logical Content of Knowledge Bases](https://alexandergheorghiu.com/publications/logical-content-knowledge-bases.html): Logic derived from the structure of knowledge: starting from a pre-logical notion of a knowledge base, logical constants are defined intrinsically and extrinsically, recovering classical, intuitionistic, and intermediate logics.
- [A Proof-theoretic Foundation for Mathematics](https://alexandergheorghiu.com/publications/proof-theoretic-foundation-mathematics.html): An extended abstract arguing that base-extension semantics for classical logic furnishes a technically grounded reading of Dummett's response to Gödel's incompleteness theorems.
- [Proof-theoretic Semantics for the Logic of Bunched Implications](https://alexandergheorghiu.com/publications/pts-bunched-implications.html): Base-extension semantics for the logic of bunched implications (BI), combining B-eS for intuitionistic propositional logic and intuitionistic multiplicative linear logic.
- [Proof-theoretic Semantics for First-order Logic](https://alexandergheorghiu.com/publications/pts-first-order-logic.html): An elementary, constructive, and native proof of soundness and completeness for the base-extension semantics of classical and first-order intuitionistic logic.
- [Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)](https://alexandergheorghiu.com/publications/pts-imll-tableaux.html): Extended abstract presenting base-extension semantics for intuitionistic multiplicative linear logic at TABLEAUX 2023.
- [Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic](https://alexandergheorghiu.com/publications/pts-imll.html): Base-extension semantics for intuitionistic multiplicative linear logic (IMLL), proving soundness and completeness.
- [Reductive Logic, Coalgebra, and Proof-search](https://alexandergheorghiu.com/publications/reductive-logic-coalgebra.html): Develops the connections between reductive logic, coalgebra, and proof-search, contributing to the Festschrift for Samson Abramsky.
- [Semantic Foundations of Reductive Reasoning](https://alexandergheorghiu.com/publications/semantic-foundations-reductive-reasoning.html): Develops the semantic foundations of reductive reasoning in the proof-theoretic semantics framework.
- [Semantical Analysis of the Logic of Bunched Implications](https://alexandergheorghiu.com/publications/semantical-analysis-bi.html): Provides a semantical analysis of the logic of bunched implications using resource semantics and algebraic methods.
- [A Survey of Proof-theoretic Semantics](https://alexandergheorghiu.com/publications/survey-proof-theoretic-semantics.html): A concise survey of proof-theoretic semantics: from Gentzen and Prawitz's semantics of proofs to Sandqvist's base-extension semantics and its recent development for modal, substructural, and first-order logics.
- [A System for Evaluating the Admissibility of Rules for Intuitionistic Propositional Logic](https://alexandergheorghiu.com/publications/system-evaluating-admissibility.html): Presents a proof-theoretic system for evaluating admissibility of rules for intuitionistic propositional logic.
- [Truth, Support, and Arithmetic](https://alexandergheorghiu.com/publications/truth-support-arithmetic.html): A mathematically precise alternative reading of Gödel's second incompleteness theorem: the gap lies not between provability and truth, but between derivability and proof-theoretic semantic consequence within a single arithmetical theory.

## Essays and public writing

Public-facing essays and reviews, including pieces in the Times Literary Supplement, The Conversation, and Mathematics Today. Index: https://alexandergheorghiu.com/writing.html

- [A world in which AI feels pain](https://alexandergheorghiu.com/writing/a-world-in-which-ai-feels-pain.html): Saul Kripke's Naming and Necessity, half a century on — and what his possible worlds mean for whether an artificial mind could feel pain.
- [By inference: An alternative account of logic](https://alexandergheorghiu.com/writing/by-inference-alternative-account-of-logic.html): A review of Ulf Hlobil and Robert Brandom's Reasons for Logic, Logic for Reasons, and why the foundations of logic matter for how we build and trust intelligent systems.
- [High School Algebra and the Limits of AI](https://alexandergheorghiu.com/writing/high-school-algebra-limits-of-ai.html): From Tarski's high-school identities to Gödel's incompleteness theorems, and what they reveal about what AI genuinely cannot do.
- [The Mathematics of Double-checking Programs](https://alexandergheorghiu.com/writing/mathematics-of-double-checking-programs.html): How formal verification — from Rice's theorem to Hoare and Separation Logic — underpins reliable software and AI.
- [Researchers have invented a new system of logic that could boost critical thinking and AI](https://alexandergheorghiu.com/writing/new-system-of-logic-critical-thinking-ai.html): A new logical framework — inferentialism — with implications for AI reasoning and critical thinking.

## Workshops

- [AI Workshops for Leadership Teams](https://workshops.alexandergheorghiu.com/): Half-day workshops for boards and strategy teams on evaluating AI claims and making sound decisions under uncertainty. Separate subdomain.

## Research themes

1. **Meaning and Inference** — Proof-theoretic semantics and inferential approaches to meaning across classical, intuitionistic, and substructural logics.
2. **Logic and Intelligent Systems** — Formal tools for making the structure of reasoning in AI systems legible, accountable, and open to rigorous scrutiny.
3. **Proof Theory and Computation** — The mathematical structure of proofs and their applications in computation, distributed systems, and automated reasoning.
4. **Foundations of Mathematics** — Philosophical and logical underpinnings of mathematical knowledge and formal systems.
5. **Formal Models of Norms and Governance** — Logical methods for representing policies and institutional structures, including AI governance.

## Affiliations and identifiers

- University College London (current — Lecturer, PPLV group, Department of Computer Science): https://profiles.ucl.ac.uk/73204-alexander-v-gheorghiu
- University of Southampton (previous — New Frontiers Fellow): https://www.southampton.ac.uk/people/668bl9/doctor-alexander-gheorghiu
- ORCID: https://orcid.org/0000-0002-7144-6910
- Google Scholar: https://scholar.google.co.uk/citations?user=NuymnkMAAAAJ&hl=en
- PhilPeople: https://philpeople.org/profiles/alexander-v-gheorghiu
- Wikidata: https://www.wikidata.org/wiki/Q139736899
- DBLP: https://dblp.org/pid/276/6726