Showing 1–4 of 4 results for author: Artemov, S

Serial Properties, Selector Proofs, and the Provability of Consistency

Authors: Sergei Artemov

Abstract: 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… ▽ More 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. △ Less

Submitted 18 March, 2024; originally announced March 2024.

MSC Class: 03A05; 03B30; 03F03; 03F07; 03F30; 03F40 ACM Class: F.3.0; F.4.0; F.4.1; I.2.0; I.2.3

The Provability of Consistency

Authors: Sergei Artemov

Abstract: 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 reduci… ▽ More 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. △ Less

Submitted 22 June, 2020; v1 submitted 19 February, 2019; originally announced February 2019.

Comments: A compact exposition of the main result and a brief foundational discussion

MSC Class: 03F03; 03F25; 03F30; 03F40; 03F50

Knowing the Model

Authors: Sergei Artemov

Abstract: 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… ▽ More 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. △ Less

Submitted 16 October, 2016; originally announced October 2016.

Comments: 20 pages, 12 figures

MSC Class: 03A05; 03B42; 03B45; 03B70 ACM Class: I.2.4; F.4.1

Intuitionistic Epistemic Logic

Authors: Sergei Artemov, Tudor Protopopescu

Abstract: 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… ▽ More 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. △ Less

Submitted 16 January, 2016; v1 submitted 6 June, 2014; originally announced June 2014.

Comments: 40 pages. Pre-print of version to appear in the Review of Symbolic Logic

MSC Class: 03B20; 03B42

Journal ref: The Review of Symbolic Logic 9 (2016) 266-298