Searcharxiv⌕ Search

arXiv subjects

Alexander V. Gheorghiu

Publications and source records attributed to Alexander V. Gheorghiu.

At least 19 recordsLinked to original sources
arXiv2026

Classical Logic as Intuitionistic Logic with Duality

The field of proof-theoretic semantics (P-tS) offers an alternative approach to meaning in logic that is based on inference and argument (rather than truth in a model). It has been successfully developed for various logics; in particular, Sandqvist has developed such semantics for both classical and intuitionistic logic. In the case of classical logic, P-tS provides a conception of consequence that avoids an a priori commitment to the principle of bivalence, addressing what Dummett identified as a significant foundational challenge in logic. In this paper, we propose an alternative P-tS for classical logic, which essentially extends the P-tS for intuitionistic logic by operating over literals rather than atomic propositions. Importantly, literals are atomic and not defined by negation but are related by a primitive duality encoded inferentially at the atomic level. This semantics illustrates the perspective that classical logic can be understood as intuitionistic logic supplemented by a principle of duality, offering fresh insights into the relationship between these two systems.

math.LO↗
arXiv2026

Inferentialist Game Semantics (Extended Abstract)

Game semantics is an elegant approach to the formal semantics of reasoning and computation that grounds model-theoretic concepts of truth and validity in game-theoretic concepts that emphasize the dynamic and interactive aspects of logical reasoning. In Hyland-Ong games, plays are traces of interactions between a player and an environment and such games provide a naturally appealing semantics for computation that is derived from proof-search in logical systems. Such a semantics can be seen as providing an intensional theory of meaning for systems of logic in terms of (the computation of) proofs. In logic, an intensional theory of meaning for systems of logic is offered by proof-theoretic semantics; in particular, by base-extension semantics (B-eS), in which the model-theoretic interpretation of atomic propositions in a satisfaction relation is replaced by a validity relation which uses provability in `bases' of atomic rules. We establish a fully abstract correlation between B-eS and Hyland-Ong game semantics, employing techniques similar to those used by Sandqvist to give a sound and complete B-eS for intuitionistic propositional logic. We illustrate our semantics through the example of 4x4 Sudoku.

math.LO↗
arXiv2026

Support is Search

Sandqvist's base-extension semantics for intuitionistic propositional logic defines a support relation parametrised by atomic bases, with validity identified as support in every base. Sandqvist's completeness theorem answers the global question: which formulae are valid? This paper addresses the local question: given a fixed base, what does support in that base correspond to? We show that support in a fixed base coincides with proof-search in a second-order hereditary Harrop logic program, via an encoding of formulae as logic-programming goals. This encoding proceeds by reading the semantic clauses in continuation-passing style, revealing that the universal quantifiers over base extensions and atoms appearing in those clauses are not domain-ranging quantifiers over a completed totality, but eigenvariables governed by a standard freshness discipline. Base-extension semantics thereby admits a fully constructive and computationally transparent interpretation: support is proof-search. The result complements Sandqvist's global theorem with a local correspondence, vindicates the anti-realist foundations of the framework on its own terms, and opens the way for implementing the semantics in modelling tasks.

cs.LO↗
arXiv2026

In Defence of the Material Conditional

The material conditional has long been charged with paradox. Defined truth-functionally, it renders true any conditional whose antecedent is false or consequent true -- hence, seemingly absurd statements such as `If unicorns exist, then $2+2=4$'. This has been taken as proof that the connective cannot capture the meaning of ordinary if-then sentences, which appear to imply a causal or evidential link. I argue, by contrast, that the paradoxes arise from a confusion of what it expresses caused by cognitive biases. The material conditional properly belongs to the class of indicative, not subjunctive, conditionals -- those that register patterns of co-variation rather than counterfactual dependence. When understood as a formal device marking entailment under a background theory, it faithfully represents a mode of reasoning essential to science itself: correlation without causation. The faults ascribed to it, therefore, are not flaws in meaning or standard use, but as misapplication and misreading.

math.LO↗
arXiv2026

Verification of Robust Properties for Access Control Policies

Existing methods for verifying access control policies require the policy to be complete and fully determined before verification can proceed, but in practice policies are developed iteratively, composed from independently maintained components, and extended as organisational structures evolve. We introduce robust property verification: the problem of determining what a policy's structure commits it to regardless of how pending decisions are resolved and regardless of subsequent extension. We define a support judgment $\Vdash_{P}ϕ$ stating that policy $P$ has robust property $ϕ$, with connectives for implication, conjunction, disjunction, and negation, prove that it is compositional (verified properties persist under policy extension by a monotonicity theorem), and show that despite quantifying universally over all possible policy extensions the judgment reduces to proof search in a second-order logic programming language. Soundness and completeness of this reduction are established, yielding a finitary and executable verification procedure for robust security properties.

cs.CR↗
arXiv2026

On the Concept of Arithmetic Conseqeunce

Gödel's second incompleteness theorem is standardly understood as showing that no sufficiently strong, consistent theory of arithmetic can prove its own consistency, a result typically interpreted against a model-theoretic background in which arithmetical language is evaluated with respect to an independently given structure of natural numbers. This paper develops an alternative perspective grounded in proof-theoretic semantics. We distinguish between derivability and a semantic notion of consequence given by support, defined compositionally in terms of the inferential roles fixed by a theory. For suitable arithmetical theories A formulated in a finite signature (such as Robinson's Q and Peano Arithmetic), these two notions can diverge in a principled way: although A does not prove its own consistency, it nevertheless supports its formalized consistency statement, and more generally supports sentences not derivable within it. This does not conflict with Gödel's incompleteness theorem, but instead reframes incompleteness as a divergence between two internally determined notions of consequence associated with a single theory, rather than as a gap between syntactic provability and truth in a mind-independent structure. The result clarifies the relationship between reflection, consistency, and inferentialist approaches to meaning, and shows how substantial semantic determinacy may arise from the inferential structure of arithmetic itself.

math.LO↗
arXiv2026

Classical Logic without Bivalance

Sandqvis's semantics for classical logic without bivalence resolves the question of an anti-realist account of classical reasoning after Dummett. This paper applies the framework to the essential questions of metamathematics. The system intuitively handles $ω$-incompleteness, makes induction meaning-constitutive, and yields an elementary consistency proof for Peano Arithmetic using only ordinary induction on the natural numbers, with no appeal to transfinite ordinals or recognition-transcendent truth.

math.LO↗
arXiv2025

Proof-theoretic Semantics for Second-order Logic

We develop a proof-theoretic semantics (P-tS) for second-order logic (S-oL), providing an inferentialist alternative to both full and Henkin model-theoretic interpretations. Our approach is grounded in base-extension semantics (B-eS), a framework in which meaning is determined by inferential roles relative to atomic systems -- collections of rules that encode an agent's pre-logical inferential commitments. We show how both classical and intuitionistic versions of S-oL emerge from this set-up by varying the class of atomic systems. These systems yield modular soundness and completeness results for corresponding Hilbert-style calculi, which we prove equivalent to Henkin's account of S-oL. In doing so, we reframe second-order quantification as systematic substitution rather than set-theoretic commitment, thereby offering a philosophically lightweight yet expressive semantics for higher-order logic. This work contributes to the broader programme of grounding logical meaning in use rather than reference and offers a new lens on the foundations of logic and mathematics.

math.LO↗
arXiv2025

Proof-theoretic Semantics for First-order Logic

Sandqvist gave a proof-theoretic semantics (P-tS) for classical logic (CL) that explicates the meaning of the connectives without assuming bivalance. Later, he gave a semantics for intuitionistic propositional logic (IPL). While soundness in both cases is proved through standard techniques, the proof completeness for CL is complex and somewhat obscure, but clear and simple for IPL. Makinson gave a simplified proof of completeness for classical propositional logic (CPL) by directly relating the the P-tS to the logic's extant truth-functional semantics. In this paper, we give an elementary, constructive, and native -- in the sense that it does not presuppose the model-theoretic interpretation of classical logic -- proof of completeness the P-tS of CL using the techniques applies for IPL. Simultaneously, we give a proof of soundness and completeness for first-order intuitionistic logic (IL).

math.LO↗
arXiv2025

Semantic Foundations of Reductive Reasoning

The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual 'reductive' perspective: collections of sufficient premisses are generated from putative conclusions. We call this paradigm, 'reductive logic'. This expression of logic encompass as diverse reasoning activities as proving a formula in a formal system to seeking to meet a friend before noon on Saturday. This paper is a semantical analysis of reductive logic. In particular, we provide mathematical foundations for representing and reasoning about 'reduction operators'. Heuristically, reduction operators may be thought of as `backwards' inference rules. In this paper, we address their mathematical representation, how they are used in the context of reductive reasoning, and, crucially, what makes them 'valid'.

cs.LO↗
arXiv2025

On an Inferential Semantics for Intuitionistic Sentential Logic

Sandqvist's base-extension semantics (B-eS) for intuitionistic sentential logic grounds meaning relative to bases (rather than, say, models), which are arbitrary sets of permitted inferences over sentences. While his soundness proof is standard, his completeness proof, is quite unusual. It closely parallels a method introduced much earlier by Mints, who developed a resolution-based approach to intuitionistic logic using a systematic translation of formulas into sentential counterparts. In this short note, we highlight the connection between these two approaches and show that the soundness and completeness of B-eS follow directly from Mints' theorem. While the result is modest, it reinforces the relevance of proof-search to proof-theoretic semantics and suggests that resolution methods have a deeper conceptual role in constructive reasoning than is often acknowledged.

math.LO↗
arXiv2024

Inferentialist Resource Semantics

In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how inferentialism -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components.

cs.LO↗
arXiv2024

Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)

This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist's B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for IMLL, in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.

cs.LO↗
arXiv2024

Proof-theoretic Semantics for the Logic of Bunched Implications

The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist's B-eS for IPL, deferring an analysis of proof-theoretic validity, in the sense of Dummett and Prawitz, to another occasion. Essential to BI's formulation in proof-theoretic terms is the concept of a `bunch' of hypotheses that is familiar from relevance logic. Bunches amount to trees whose internal vertices are labelled with either the IMLL context-former or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the `resource interpretation' of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the `number-of-uses' reading of the propositions of linear logic as resources. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling.

cs.LO↗
arXiv2024

From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic

Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on 'proof' (as opposed to 'truth'). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of logical constants. This paper demonstrates that the B-eS for intuitionistic propositional logic (IPL) encapsulates the declarative content of a version of P-tV based on the elimination rules. This explicates how the B-eS for IPL works, and shows the completeness of this version of P-tV.

cs.LO↗
arXiv2024

A Note on an Inferentialist Approach to Resource Semantics

A central concept within informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how 'inferentialism' -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components.

cs.LO↗
arXiv2023

Defining Logical Systems via Algebraic Constraints on Proofs

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; for example, one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of reduction is to obtain a tool for uniform and modular treatment of proof theory and provide a bridge between semantics logics and their proof theory. The article discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. The results include the following: a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and, a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.

cs.LO↗