arXiv subjects

Sergei Artemov

Publications and source records attributed to Sergei Artemov.

8 recordsLinked to original sources

arXiv2025

Non-Compact Proofs

Non-compact proofs are a class of reasoning that is used in mathematics but overlooked in the analysis of (un)provability of consistency. We focus on proofs of arithmetical statements (*) "for any natural number n, F(n)." A proof of (*) is called compact if all proofs of F(n)'s for n=0,1,2,... fit into some finitely axiomatized fragment of Peano Arithmetic PA. An example of non-compact reasoning is given by the standard proof of Mostowski's 1952 reflexivity theorem: PA proves the consistency of its finite fragments. It turns out that Gödel's second incompleteness theorem prohibits compact proofs and does not rule out non-compact proofs of PA-consistency formalizable in PA. This explains how the recent proof of PA-consistency in PA works. It essentially formalizes in PA the explicit version of Mostowski's proof, which is not in the scope of Gödel's theorem.

math.LO↗

arXiv2025

Consistency formula is strictly stronger in PA than PA-consistency

In this note, we show that, despite the widespread assumption, the consistency formula for Peano Arithmetic PA, Con(PA), "for all x, x is not a code of a derivation of (0=1)," is not equivalent in PA to the consistency of PA. Specifically, we demonstrate that "PA is consistent" is provably in PA equivalent to the series ConS(PA) of arithmetical sentences "n is not a code of a derivation of (0=1)" for n=0,1,2,.... Since Con(PA) is strictly stronger in PA than ConS(PA), the unprovability of Con(PA) in PA does not yield the unprovability of PA-consistency.

math.LO↗

arXiv2024

Serial Properties, Selector Proofs, and the Provability of Consistency

For Hilbert, the consistency of a formal theory T is an infinite series of statements "D is free of contradictions" for each derivation D and a consistency proof is i) an operation that, given D, yields a proof that D is free of contradictions, and ii) a proof that (i) works for all inputs D. Hilbert's two-stage approach to proving consistency naturally generalizes to the notion of a finite proof of a series of sentences in a given theory. Such proofs, which we call selector proofs, have already been tacitly employed in mathematics. Selector proofs of consistency, including Hilbert's epsilon substitution method, do not aim at deriving the Gödelian consistency formula Con(T) and are thus not precluded by Gödel's second incompleteness theorem. We give a selector proof of consistency of Peano Arithmetic PA and formalize this proof in PA.

math.LO↗

arXiv2022

Towards Syntactic Epistemic Logic

Traditionally, Epistemic Logic represents epistemic scenarios using a single model. This, however, covers only complete descriptions that specify truth values of all assertions. Indeed, many -- and perhaps most -- epistemic descriptions are not complete. Syntactic Epistemic Logic, SEL, suggests viewing an epistemic situation as a set of syntactic conditions rather than as a model. This allows us to naturally capture incomplete descriptions; we discuss a case study in which our proposal is successful. In Epistemic Game Theory, this closes the conceptual and technical gap, identified by R. Aumann, between the syntactic character of game-descriptions and semantic representations of games.

cs.LO↗

arXiv2020

The Provability of Consistency

We offer a mathematical proof of consistency for Peano Arithmetic PA formalizable in PA. This result is compatible with Goedel's Second Incompleteness Theorem since our consistency proof does not rely on the representation of consistency as a specific arithmetical formula. Our findings show that formal theories can finitely formalize proofs of certain properties presented as schemes without reducing the presentation of those properties to a single formula. We outline a theory of proving schemes in PA.

math.LO↗

arXiv2017

Epistemic Modeling with Justifications

Existing logical models do not fairly represent epistemic situations with fallible justifications, e.g., Russell's Prime Minister example, though such scenarios have long been at the center of epistemic studies. We introduce justification epistemic models, JEM, which can handle such scenarios. JEM makes justifications prime objects and draws a distinction between accepted and knowledge-producing justifications; belief and knowledge become derived notions. Furthermore, Kripke models can be viewed as special cases of JEMs with additional assumptions of evidence insensitivity and common knowledge of the model. We argue that JEM can be applied to a range of epistemic scenarios in CS, AI, Game Theory, etc.

cs.LO↗

arXiv2016

Knowing the Model

Epistemic modal logic normally views an epistemic situation as a Kripke model. We consider a more basic approach: to view an epistemic situation as a set W of possible states/worlds -- maximal consistent sets of propositions -- with conventional accessibility relations determined by W. We find that in many epistemic situations, W is not a Kripke model: a necessary and sufficient condition for W to be a Kripke model is the so-called `fully explanatory property' - a propositional form of common knowledge of the model - which has been a hidden (and overlooked) assumption in epistemic modal logic. We sketch a theory that describes epistemic models in their generality. We argue for conceptual and practical value of new models, specifically for representing partial knowledge, asymmetric knowledge, and awareness.

math.LO↗

arXiv2016

Intuitionistic Epistemic Logic

We outline an intuitionistic view of knowledge which maintains the original Brou\-wer-Heyting-Kolmogorov semantics for intuitionism and is consistent with the well-known approach that intuitionistic knowledge be regarded as the result of verification. We argue that on this view co-reflection $A \rightarrow {\bf{K}} A$ is valid and the factivity of knowledge holds in the form ${\bf{K}} A \rightarrow \neg\neg A$ `known propositions cannot be false'. We show that the traditional form of factivity ${\bf{K}} A \rightarrow A$ is a distinctly classical principle which, like {\it tertium non datur} $A\vee\neg A$, does not hold intuitionistically, but, along with the whole of classical epistemic logic, is intuitionistically valid in its double negation form $\neg\neg({\bf{K}} A\rightarrow A)$. Within the intuitionistic epistemic framework the knowability paradox is resolved in a constructive manner. We argue that this paradox is the result of an unwarranted classical reading of constructive principles and as such does not have the consequences for constructive foundations traditionally attributed it.

math.LO↗